BB(6) hunt
Machines / W5-3

1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC

W5-3local proof 24Claimed by someone elseBell eats counterbbchallenge ↗Explorer

How we proved it never halts

The counter never exceeds twice the word's length

The tape holds a binary counter on the right, written 11 for a 1 and 00 for a 0, lowest digit first, and on its left a word of 10 pairs with one flaw, an extra cell called the defect. Each trip of the head into the word and back adds 1 to the counter, and every second trip moves the defect two pairs further from the counter. Once the defect has walked off the far end, the next trip reaches the blank left edge, where a sweep shifts the whole word by one cell, eats the counter's lowest digits and plants a fresh defect. So the word grows with every eat.

The key fact is a size bound at each eat: the counter's value is at most twice the number of pairs in the word. The eats fall into five cases by the counter's last binary digits. In the hardest, the eat misaligns the low digits and briefly creates a second defect, which later cancels the first; that works out only if the word is long enough, and the bound supplies exactly that.

Why that settles it: each case is a chain of exact moves from one eat to a later one, where the bound holds again. The missing table entry (state F reading 0) could only come up if the left-edge sweep met two 0 cells in a row, but that sweep only crosses the word 10 10 … 10 1, which has none. The blank tape reaches an eat inside the bound at step 165, so the machine never halts.

The Rocq proof uses busycoq's binary-counter library, proves every move as an exact run and every case as a chain of them, checks the bound's closure by arithmetic, and runs the opening directly.

#24local proof number
530lines of Rocq
3 sto compile
6/6automatic checks
space-time diagram, first 10,000 steps from blank
The first 10,000 steps from a blank tape. Time runs down; white is 1.
About this picture

The standard picture (bbchallenge.org's Default view): each row is the whole tape at one step, time runs downward, and the head's path draws the pattern.

bbchallenge-defaultStart blankRows steps 0 → 10,000, top to bottomWindow cells −200..199, left to rightColors 1 0 or unvisited

Claimed by someone else

We proved this machine locally, but our proof was still unsubmitted when we found it already covered upstream.

Submit completed proofs early. A local proof does not secure an upstream claim.

Upstream proof ↗ · Recorded timeline

What the timing evidence establishes

This describes upstream credit, not who first discovered the mathematics. The records do not establish adoption of our proof, first public push time, or whether an earlier submission would have secured credit.

Overview

In one sentence

A phase defect walks a 1010 word one pair per count; at the far end it eats 1-3 low digits of a binary counter.

Submitted mechanism Counter and budget word. The tape is a word (10)^p with one *defect* cell, then the counter BinInc [1;1] N on the right. Each count is a round trip into the word and back: it adds 1 to N, and every second count moves the defect two pairs further from the counter. (submission/README.md, Mechanism)

Upstream
The blank-start machine never halts: BECv10.v.TM15 ↗. We also have a local proof. This upstream addition is separate from our merged submissions; adoption credit is not established. Recorded commit time: 2026-10-13T13:42:06Z. First public push time is not established.
Rocq proof
check_kill PASS · first Oct 13 03:09
530 lines · 20 KB .v · compile 3.4 s · coqchk pass · 0 axioms · PASS Oct 13 03:09
· the .v file
Automatic review
6 of 6 checks passtemplate: verify/BECv5.v Module TM1 (adapted from) · details in Proof →
Class
Bell eats counterours: Bell eats counter (sheet) · ours adds: a phase defect walks a 1010 budget word away from a binary counter (digits 11/00); at the far end the counter's low digits are eaten · high confidence
On the list
not on BB6_holdouts_663.txt (line 134 of the previous list) · historical 740 line 134
eqv ×1sim 1e15

Mechanism

What to check here: the pictures show the mechanism that the rule table describes.

How it works: 3 notes
  • Tape between counts: M(a,X,b,N) = 0^inf 10^a X 10^b 011 B> 0 D(N) 11 0^inf. D(N) 11 is N in binary, low digit first, 1 = 11, 0 = 00 (the final 11 is the leading 1). X is a one-cell phase defect (an extra 1 or 0) in the 1010 word.
  • Each count adds 1 to N and moves the defect left (X=1 -> X=0 in place, X=0 -> X=1 two pairs left). When it falls off the far end (word 10^p, no defect: E(p,N)) a C/F sweep runs the whole word into the counter and eats its low end: N odd -> (N+1)/2, N = 0 mod 4 -> N/4, N = 2 mod 8 -> (N+6)/8, N = 6 mod 8 -> a two-defect transient ending in a quick second eat. The word gains 2 to 7+t pairs.
  • Eat to eat: p' = p+1+e+[p odd], N' = f(N)+p'+[p even] (e = 1,2,3 digits eaten); 6 mod 8: N = (2m+1)2^(t+3)-2 -> E(p+7+t, m+2^t+t+1), N = 16m+6 -> E(p+7, m+5). This equals the direct run at all 2,091 eats to 1e11 steps. Invariant p >= 20, 1 <= N <= 2p is kept by every branch (algebra; exhaustive for p <= 2000) and holds from E(21, 6) at step 3,097. No branch halts (the only halt, F0, needs a C/F sweep, and all 514 sweeps to 1e9 are eats), so the pseudo-random order of eat types needs no prediction: not a cryptid. Siblings: none.

Figures for Checkpoint A

Fig 1 · bbchallenge default viewviewer ↗

The site's view. The grey 1010 word grows to the left; the counter's 11/00 digits sit at its right edge.

bbchallenge default view
bbchallenge-defaultStart blankRows 10,000 steps squeezed into 500 px rowsWindow cells -200..199, 1 px = 1 cellColors 1 0 or never visited head after a right/left move
Rows: 1 px row = 20 steps; the site blends steps 20y+9 and 20y+10
Fig 2 · Phase view, one row per countQ1

One row per count. Follow the cream/navy border left, row by row, to the reset at the left edge.

Phase view, one row per count
customStart blankRows one per count configuration MWindow cells -73..99, 1 px = 0.5 cellsColors opposite parity head (state B) blank outside the written word
Rows: (B reading the 0 left of the counter digits): counts 1..700, steps 31..117,683 (not evenly spaced), 2 px per row · Window: each cell drawn 2 px wide · Colors: cream = cell value equals position parity; the cream/navy border inside the word is the defect, and the checkered strip at the right is the counter
Fig 3 · N/p at each eat, by typeQ3

One dot per eat. Check every dot against the black line; the band near 0 is the quick second eats.

N/p at each eat, by type
customStart blankRows x = eats 1..2,091 of the blank runWindow x = eat indexColors N odd N 0 mod 4 N 2 mod 8 N 6 mod 8 line: N/p of 2 (invariant bound) N/p of 1
Rows: (steps 31..99,939,266,761), 3 eats per px column, in order; abstract model, equal to the direct run at every one of these eats · Window: 1 px = 3 eats; y = N/p from 0 (bottom) to 2.4 (top), 1 px = 0.01 · Colors: dashed; a dot's colour is the type of the eat taken from that state
More figures (2)Fig 4–5: One eat, every step · One budget cycle, every 16 steps
Fig 4 · One eat, every stepQ2

Follow orange/magenta (B/E) left to the edge, then blue/cyan (C/F) right across the word into the counter.

One eat, every step
bbchallenge-exploreStart constructed: 0∞ (10)8 011 B> 0 111100 11 0∞Rows every step, steps 0..66Window cells -22..8, 1 px = 0.125 cellsColors 0 1
Rows: from the eat configuration E(8, 11) to the next count configuration M(10, 1, 0, 6) · Window: 8 px per cell · Colors: head cell coloured by state: A red, B orange, C blue, D green, E magenta, F cyan
Fig 5 · One budget cycle, every 16 steps

Default colours, mid-run. Look for the faint diagonal seam (the defect) and the eats at the top and bottom.

One budget cycle, every 16 steps
bbchallenge-defaultStart mid-run: step 30,900Rows every 16 stepsWindow cells -43..69, 1 px = 0.5 cellsColors 1 0 or never visited head after a right/left move
Rows: steps 30,900..39,700 (551 rows; eats at steps 31,017 and 39,071)
Rules (9/9 validated)exact tape rewrites the proof will formalize, each re-checked by simulation
rulefrom ⟶ tocasesstepschecked
INC1
0∞ (10)a 1 (10)b 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)a 0 (10)b 011 B> 0 D(N+1) 11 0∞
a >= 0, b >= 0, N >= 1—✓319/319
INC0
0∞ (10)a 0 (10)b 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)a-2 1 (10)b+2 011 B> 0 D(N+1) 11 0∞
a >= 2; a = 1 is INCL; a = 0 is E(b, N)—✓276/276
INCL
0∞ 10 0 (10)b 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)b+2 011 B> 0 D(N+1) 11 0∞
defect falls off the far end; the word grows one pair—✓601/601
EAT1
0∞ (10)p 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)p+2 1 011 B> 0 D((N+1)/2) 11 0∞
N odd—✓292/292
EAT2
0∞ (10)p 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)p+2 111 011 B> 0 D(N/4) 11 0∞
N = 0 mod 4; next count gives 0^inf 10^(p+2) 1 10 011 B> 0 D(N/4+1) 11 0^inf (137/137)—✓137/137
EAT3
0∞ (10)p 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)p+4 1 011 B> 0 D((N+6)/8) 11 0∞
N = 2 mod 8—✓111/111
EAT4
0∞ (10)p 011 B> 0 D(N) 11 0∞
⟶ 0∞ (10)p+7-2^t 0 (10)2^t-1 12t+1 011 B> 0 D(m+1) 11 0∞
N = (2m+1)2^(t+3)-2, t >= 1, p+7 >= 2^t; t = 0 (N = 16m+6): 0^inf 10^(p+5) 1 10 1 011 B> 0 D(m+1) 11 0^inf—✓300/300
E2E (eat to eat)
E(p, N) = 0∞ (10)p 011 B> 0 D(N) 11 0∞
⟶ E(p', N'): p' = p+1+e+[p odd], N' = f(N)+p'+[p even]; 6 mod 8: E(p+7+t, m+2t+t+1), or E(p+7, m+5) if t = 0
e,f = 1,(N+1)/2 (N odd); 2,N/4 (0 mod 4); 3,(N+6)/8 (2 mod 8). 6 mod 8 needs p+7 >= 2^t (sharp: tested p = 2^t-16..2^t+3 for t = 2..7, fails exactly below it). 855/855 random instances inside the precondition (1 more, p=50 with t=6, is outside it); plus all 2,091 blank-run eats to 1e11 steps—✓855/855
R1 (hub view)
0∞ (10)a+2^(k-1) X (10)b 12k A> 0∞
⟶ 0∞ (10)a X (10)b+2^(k-1) 12k+2 A> 0∞
X in {1,0}, k >= 2, b >= 1: 2^(k-1) counts with no eat (counter overflow view)—✓200/200
Compressed historythe tape as 0∞ (10)p 011 B> 0 D(N) 11 0∞ at 40 moments: where the rules are read off
0∞ (10)p 011 B> 0 D(N) 11 0∞
steppN
3101
16524
45157
905812
1,6951115
2,7251422
3,097216
3,521285
7,3513034
12,1213440
17,5993748
23,8714153
31,0174471
8,899,889316366
51,650,94358566
151,908,3918621,293
341,226,4791,14698
688,305,6251,4002,505
1,174,692,2651,6642,627
1,810,659,7751,9522,938
2,643,272,1132,2642,653
3,886,992,7172,5224,839
5,367,305,7472,7743,383
7,068,639,7493,0504,827
9,103,740,7553,3124,971
11,588,017,1113,5674,856
14,480,475,2773,8326,307
17,569,657,4234,1035,946
21,470,553,4034,3314,380
25,524,842,8674,6196,452
29,787,116,7314,936274
34,846,961,2275,2317,328
41,082,713,7295,48210,133
47,342,989,4495,75811,284
54,754,780,2216,0187,393
61,934,244,6236,31010,745
70,409,297,5036,56211,918
79,694,337,8296,82610,290
89,464,421,2977,09212,458
99,939,266,7617,367197
plast 7,367
7,3670311e11log xstep 31: p = 0step 165: p = 2step 451: p = 5step 905: p = 8step 1695: p = 11step 2725: p = 14step 3097: p = 21step 3521: p = 28step 7351: p = 30step 12121: p = 34step 17599: p = 37step 23871: p = 41step 31017: p = 44step 8899889: p = 316step 51650943: p = 585step 151908391: p = 862step 341226479: p = 1146step 688305625: p = 1400step 1174692265: p = 1664step 1810659775: p = 1952step 2643272113: p = 2264step 3886992717: p = 2522step 5367305747: p = 2774step 7068639749: p = 3050step 9103740755: p = 3312step 11588017111: p = 3567step 14480475277: p = 3832step 17569657423: p = 4103step 21470553403: p = 4331step 25524842867: p = 4619step 29787116731: p = 4936step 34846961227: p = 5231step 41082713729: p = 5482step 47342989449: p = 5758step 54754780221: p = 6018step 61934244623: p = 6310step 70409297503: p = 6562step 79694337829: p = 6826step 89464421297: p = 7092step 99939266761: p = 7367
Nlast 197
12,4581311e11log xstep 31: N = 1step 165: N = 4step 451: N = 7step 905: N = 12step 1695: N = 15step 2725: N = 22step 3097: N = 6step 3521: N = 5step 7351: N = 34step 12121: N = 40step 17599: N = 48step 23871: N = 53step 31017: N = 71step 8899889: N = 366step 51650943: N = 66step 151908391: N = 1293step 341226479: N = 98step 688305625: N = 2505step 1174692265: N = 2627step 1810659775: N = 2938step 2643272113: N = 2653step 3886992717: N = 4839step 5367305747: N = 3383step 7068639749: N = 4827step 9103740755: N = 4971step 11588017111: N = 4856step 14480475277: N = 6307step 17569657423: N = 5946step 21470553403: N = 4380step 25524842867: N = 6452step 29787116731: N = 274step 34846961227: N = 7328step 41082713729: N = 10133step 47342989449: N = 11284step 54754780221: N = 7393step 61934244623: N = 10745step 70409297503: N = 11918step 79694337829: N = 10290step 89464421297: N = 12458step 99939266761: N = 197
Template comparisonBECv5.v TM1: partly applies · the nearest solved proof, what carries over, and the transitions that differ
01
A1RB1RA
B1LC1LE
C1RF1LD
D1RE0LD
E0LB0RA
F---0RC
file
BECv5.v:30
module
TM1
machine
1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB (11 transitions apart)
diff
different table (no busycoq hand proof within 3 transitions; the distance-3 tables are decider proofs in Indv2.v and RWL_mod_v3.v)
note
Same architecture as BECv5 TM1 (and our W4-2): a binary counter BinInc plus a budget word with a one-cell phase defect (TM1's R n m = 1 (10)^(1+n) 0 (10)^m), one budget pair per count (RIncs), an eat that removes low counter digits (ROv), BigStep and progress_nonhalt_cond with a linear invariant (TM1: a <= 1+b; here N <= 2p). Different: the defect walks AWAY from the counter and the eat happens at the far blank end via a C/F sweep over the whole word; the eat removes 1, 2 or 3 digits by N mod 8, plus a two-defect transient for N = 6 mod 8. Our counter D(N) 11 0^inf is BinInc [1;1] N on the right (RBinInc_spec).
Proof strategy & riskshow the formal proof will go · 3 risks to watch

S(p,N) := E(p,N). Prove INC1/INC0/INCL (E/B sweep, defect fix, A sweep, RBinInc_spec), the C/F sweep, EAT1-3 and EAT4 plus its transient, then BigStep E -> E. Close with progress_nonhalt_cond, P := p >= 20 /\ 1 <= N <= 2p, after multistep_nonhalt to E(21, 6) at step 3,097.

  • ▲The N = 6 mod 8 transient (a 1^(2t+1) block becomes a second defect that walks 2^t+t pairs and cancels the first) is validated end to end but its inner steps are not yet stated as exact lemmas; it is the largest piece of Rocq work.
  • ▲No busycoq file has a defect that walks away from the counter with an eat at the far blank end, so most lemmas are new; expect a W4-2-sized effort (2-3 Rocq stages).
  • ▲Edge cases must be exact: the defect at a = 0 or 1, a leading blank when p+7 = 2^t, and the [p odd] / [p even] terms in every eat.
Stats & provenance1011 steps simulated · 14,769 cells · the status in full · files
simulated
1011 steps
tape
14,769 cells · 7,386 nonzeros
growth
span 14,769 cells at 1e11 (6,815 at 1e10), about 3.2 steps^(1/3); word 2p with p = 7,367 pairs at the last eat before 1e11; counter N <= 2p; abstract model run for 2,000,000 eats (p = 7,056,392): N/p < 2 throughout, and 6 mod 8 slack p - 2^t >= 80 after eat 20
status now
check_kill PASS, independently re-verified (status.json, 2026-10-13)
observer's note
Mechanism closed: all 2,091 eats from blank to 1e11 steps follow the validated eat-to-eat model, and a simple linear invariant (N <= 2p) is kept by every branch. Next: proof.md, then Rocq from BECv5 TM1's architecture.
files
observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v

Proof & checks

6/6 automatic checks pass

Kill 24 · Bell eats counter · the kill file 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v: 530 lines, 53 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/BECv5.v Module TM1 · 6% of our lines identical
1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).
Machine
1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC
vs holdout list
✓ byte-exact: the .v literal (L32) == 2026-10-07_778.txt line 141 (41 bytes, via tools/holdouts.py)
Theorem
✓ Lemma nonhalt: ~halts tm c0. L480
check_kill
✓ PASS · 17/17 checks pass · compile 3.39 s · coqchk pass (1.0 s) · assumptions: 0 (closed) · 2026-10-13 10:09:16 UTC · submission/check_kill.txt
Checked .v
sha256 75932a97949d61ba…
✓1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v75932a97949d61ba… = checked
✓submission/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v75932a97949d61ba… = checked
Status
✓Killed: never halts updated 2026-10-13
✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity
All 17 check_kill checks with their one-line results
✓args6x2 machine, framework module Individual62, mode nonhalt
✓input20609 bytes, 530 lines, 577 sentences
✓frameworkHEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓framework_build17 needed framework .vo files present and fresh, with native code no older than the .vo
✓forbiddennone of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓structure6 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓tm_textline 32: TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC" == <tm> (41 bytes)
✓theorem_textline 480: nonhalt : ~halts tm c0
✓coqcoqc 8.20.1 ([local working file]
✓nameshalts, c0, TM_from_str resolved inside Individual62
✓compilecompiled in 3.4s with all appended checks
✓tm_rocqBB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC" by eq_refl (in-file and isolated)
✓theorem_rocqnonhalt : ~ halts (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC") c0 with absolute names (in-file and isolated)
✓isolationonly stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓assumptions0 assumption(s), all in the baseline
✓coqchkcoqchk -norec BB6Kill.Candidate ok (1.0s); its context summary lists nothing of the file's own
✓integrityinput sha256 and framework HEAD/cleanliness identical before and after
2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).
adapted from verify/BECv5.v Module TM1 · detected from 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v line 4
6%of our lines identical to the template
1changed lines
411added lines (ours only)
119template lines dropped
1 / 1 / 51items identical / adapted / new
What the package README says it reused and changed (submission/README.md line 18, Template and what changed), quoted:

Adapted from busycoq's verify/BECv5.v, Module TM1, architecture only: a BinInc counter, a budget word with a one-cell defect, one budget pair per count, an eat of low digits, BigStep lemmas and progress_nonhalt_cond with a linear invariant. Changes: the counter is on the right (RBinInc_spec); the defect walks away from it; the eat is at the far blank edge after a sweep over the whole word; it removes 1–3 digits by N mod 8; and N ≡ 6 (mod 8) adds the misaligned counter Q and a two-defect transient. The file has 530 lines, every lemma top level.

Fig P1 · Reuse of the template, line by line and by name

Top two bars: non-blank lines after the TM string is replaced by <TM> and whitespace is collapsed. Bottom bar: our Definitions/Lemmas/… by name.

ours 436 lines
6% identical · 1 changed · 411 added
template 144 lines
17% kept verbatim · 119 not in ours
our items 53
1 identical · 1 adapted · 51 new · 11 template-only
identicalchanged / adaptedours only (new)template only
Template part: lines 1–29 (shared header, before the first Module) + 31–165 (body of Module TM1; the Module/End lines left out). Ours: lines 23–530 (header comment 1–22 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.

Template-only names: highbit, LC0, R, tm', LInc0, LIncs, LIncs', RIncs, ROv, S, BigStep

Side-by-side diff: template (144 lines) vs ours (436 lines), 531 lines differ; runs of identical lines and long template-only runs folded
identicalequal once each TM string is <TM>changedours onlytemplate only
templateours
1From BusyCoq Require Import Individual62.24From BusyCoq Require Import Individual62.
2Require Import ZifyNat Lia.25Require Import ZifyNat Lia.
3Require Import ZArith.26Require Import ZArith.
4Require Import String.27Require Import String.
5From BusyCoq Require Import BinaryCounter_v2.28From BusyCoq Require Import BinaryCounter_v2.
6From BusyCoq Require Import Longitudinal.
8Open Scope list.30Open Scope list.
10Ltac flia := repeat (lia||f_equal).
12Lemma highbit x:
⋯ 14 template-only lines (template 13–26), not in ours
27 cbn; lia.
28Qed.
32Definition tm := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB").32Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").
34Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).34Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
35Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).35Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
37Notation "l <| r" :=
37(** C(n): n in binary, lowest digit first, 1 = 11, 0 = 00, leading 1 last.
38 (l <{{A}} [] *> r) (at level 30).
38 HF l r: E reads the last cell of l, followed by 1 0 1 1 and the right side r. *)
40Notation "l |> r" :=
39Definition C n := BinInc [1;1] n.
41 (l <* [] {{B}}> r) (at level 30).
40Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.
43Definition LC0 n := BinInc <[0;1] n.
42(** ** Low-level rules *)
44Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0.
44(* right part of every count: A over (11)^n, CARRY, TS *)
46Notation hL := (A,[]).
46Lemma RIncG l r n:
47Notation hR := (B,[]).
47 l <* [1;1;0;1] {{A}}> [1;1]^^n *> [0;0] *> r -->+
48Notation hLR := [(hL,hR)].
48 l <{{E}} [1;0;1;1] *> [0;0]^^n *> [1;1] *> r.
49Notation hRL := [(hR,hL)].
49Proof. es. Qed.
51Definition tm' := flip tm.
51(* the counter increment on C *)
53Lemma LInc0 r n:52Lemma RInc n l:
54 LC0 n <| r -->*
53 l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
55 LC0 (1+n) |> r.
56Proof.54Proof.
57 unfold LC0.
55 unfold C, HF. apply RBinInc_spec. intros. apply RIncG.
58 er.
59 eapply evstep_trans.
60 1: apply progress_evstep.
61 1: apply LBinInc_spec with (qL:=[]) (qR:=[]); es.
62 er.
63Qed.56Qed.
65Lemma LIncs n:
58(* left parts: INC1 (EB, X1, AS), INC0 (EB, X0, AS), INC011 (F011, A01, AS) *)
66 sideRLs tm' (hLR^^n) (LC0 0) (LC0 n).
59Lemma L1 u b r:
60 HF (u <* [1] <* [0;1]^^b) r -->+ u <* [0] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
61Proof. unfold HF. es. Qed.
63Lemma L0 u b r:
64 HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ u <* [0;1;0;1] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
65Proof. unfold HF. es. Qed.
67Lemma L011 u r:
68 HF (u <* [0;0;1;1;0;1]) r -->+ u <* [0;1;1;0;1;0] <* [1;1;0;1] {{A}}> r.
69Proof. unfold HF. es. Qed.
71(* EAT: EB, then the C/F sweep EAT0 over the whole word, then CS *)
72Lemma LEat b r:
73 HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
74Proof. unfold HF. es. Qed.
76(* Y rules: the right part after an eat *)
77Lemma Y1C v n:
78 v <* [0;1;1] {{A}}> C (n*2+1) -->+ HF (v <* [1]) (C (1+n)).
67Proof.79Proof.
68 induction n.
80 unfold C. rewrite BinInc_mul2add1. fold (C n).
69 - esx.
81 eapply progress_trans. 2: apply RInc.
70 - replace (S n) with (n+1) by lia.
82 unfold C. es.
71 rewrite lpow_add.
72 eapply sideRLs_trans.
⋯ 4 template-only lines (template 73–76), not in ours
77 rw_Bin.
78 esx.
79Qed.83Qed.
81Lemma LIncs' n:
85Lemma Y2C v n:
82 sideRLs tm' (hLR^^(n*2)) (LC0 n <* [0]) (LC0 0).
86 v <* [0;1;1] {{A}}> C (n*4) -->+ HF (v <* [1;1;1]) (C n).
83Proof.87Proof.
84 unfold LC0.
88 unfold C. replace (n*4) with (n*2*2) by lia. rewrite !BinInc_mul2.
85 induction n using lt_wf_ind.
89 unfold HF. es.
86 divmod2_cases n.
87 - destruct (Nat.eqb_spec n' 0).
⋯ 16 template-only lines (template 88–103), not in ours
104 replace ((n'*2+1)*2) with (n'*2*2+2) by lia.
105 apply segRLs_addmul''; esx.
106Qed.90Qed.
108Lemma RIncs n m:
92Lemma Y3 v s r:
109 sideRLs tm (hRL^^n) (R n m) (R 0 (n+m)).
93 v <* [0;1;1] {{A}}> [0;0] *> [1;1] *> [1;1]^^s *> [0;0] *> r -->+
94 HF (v <* [1;1]) ([0;0]^^s *> [0] *> [1;1] *> r).
95Proof. unfold HF. es. Qed.
97Lemma Y4 v m:
98 v <* [0;1;1] {{A}}> [1;1;0] *> [1;1] *> C m -->+ HF (v <* [1;0;1;1]) (C (1+m)).
110Proof.99Proof.
111 gen m.
100 eapply progress_trans. 2: apply RInc.
112 induction n; intros.
113 - esx.
⋯ 10 template-only lines (template 114–124), not in ours
125 unfold LC0,R.
126 rw_Bin.
127 es.101 es.
128Qed.102Qed.
130Definition S '(a,b) := LC0 a <| R 0 b.
104Lemma Y1Q v r:
132Lemma BigStep k i m:
105 v <* [0;1;1] {{A}}> [1;1] *> [0;0] *> r -->+ HF (v <* [1]) ([1;1] *> r).
133 k*2<=(1+i+m) ->
106Proof. unfold HF. es. Qed.
134 S ((k*2+1)*2^i-1,m) -->+
108(* right part of OVF: the overflow of Q_j(2^j-1, 2m+1) *)
135 S (1+i+m-k*2,1+i+m).
109Lemma ROvf l j m:
110 l <* [1;1;0;1] {{A}}> [1;1]^^j *> [0;1;1] *> C m -->+
111 HF (l <* [0;1] <* [1;1]^^j <* [1]) (C (1+m)).
136Proof.112Proof.
137 unfold S.
113 eapply progress_trans. 2: apply RInc.
138 intros.
114 es.
139 follow10 ROv.
115Qed.
140 replace (1+i+m) with (k*2+(1+i+m-k*2)) by lia.
117(** ** Generic counting *)
141 epose proof (sideRLs_concat_1L (RIncs _ 0)) as I1.
119Definition Inc r r' := forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'.
142 follow I1.
121Lemma IncC n: Inc (C n) (C (1+n)).
143 - rewrite lpow_add.
122Proof. intros l. apply RInc. Qed.
144 eapply sideRLs_trans.
124Lemma Inc00 r: Inc ([0;0] *> r) ([1;1] *> r).
145 + apply LIncs'.
125Proof. intros l. apply (RIncG l r 0). Qed.
146 + apply LIncs.
127Lemma pt3 c1 c2 c2' c3: c1 -->+ c2 -> c2 = c2' -> c2' -->+ c3 -> c1 -->+ c3.
147 - unfold to_DH_config.
128Proof. intros H1 -> H2. eapply progress_trans; eauto. Qed.
148 finish.
130Lemma pt_pre c1 c1' c2: c1 = c1' -> c1' -->+ c2 -> c1 -->+ c2.
131Proof. intros -> H1. exact H1. Qed.
133Lemma pt_eq c1 c2 c3: c1 -->+ c2 -> c2 = c3 -> c1 -->+ c3.
134Proof. intros H1 ->. exact H1. Qed.
136Lemma HF_eq l l' r r': l = l' -> r = r' -> HF l r = HF l' r'.
137Proof. intros -> ->. reflexivity. Qed.
139Lemma Cnt1 u b r r': Inc r r' ->
140 HF (u <* [1] <* [0;1]^^b) r -->+ HF (u <* [0] <* [0;1]^^b) r'.
141Proof. intros I. eapply progress_trans. 1: apply L1. apply I. Qed.
143Lemma Cnt0 u b r r': Inc r r' ->
144 HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ HF (u <* [0;1;0;1] <* [0;1]^^b) r'.
145Proof. intros I. eapply progress_trans. 1: apply L0. apply I. Qed.
147Lemma Cnt011 u r r': Inc r r' ->
148 HF (u <* [0;0;1;1;0;1]) r -->+ HF (u <* [0;1;1;0;1;0]) r'.
149Proof. intros I. eapply progress_trans. 1: apply L011. apply I. Qed.
151(** ** The misaligned counter Q_k(x,y) = D_k(x) 0 C(y) *)
153Fixpoint Dk (k x : nat) : list Sym :=
154 match k with
155 | O => []
156 | S k' => (if Nat.odd x then [1;1] else [0;0]) ++ Dk k' (Nat.div2 x)
157 end.
159Definition Q k x y := Dk k x *> [0] *> C y.
161Lemma Dk_even k a: Dk (S k) (2*a) = [0;0] ++ Dk k a.
162Proof.
163 cbn [Dk]. rewrite Nat.div2_double.
164 replace (Nat.odd (2*a)) with false. 1: reflexivity.
165 rewrite <-Nat.negb_even, Nat.even_mul. reflexivity.
166Qed.
168Lemma Dk_odd k a: Dk (S k) (2*a+1) = [1;1] ++ Dk k a.
169Proof.
170 replace (2*a+1) with (S (2*a)) by lia.
171 cbn [Dk]. rewrite Nat.div2_succ_double.
172 replace (Nat.odd (S (2*a))) with true. 1: reflexivity.
173 rewrite Nat.odd_succ, Nat.even_mul. reflexivity.
174Qed.
176Lemma Dk_0 k: Dk k 0 = [0;0]^^k.
177Proof. induction k as [|k IH]. 1: reflexivity. cbn. rewrite IH. reflexivity. Qed.
179Lemma Dk_1 k: Dk (S k) 1 = [1;1] ++ [0;0]^^k.
180Proof. cbn [Dk]. cbn. rewrite Dk_0. reflexivity. Qed.
182Lemma Dk_full k: Dk k (2^k-1) = [1;1]^^k.
183Proof.
184 induction k as [|k IH]. 1: reflexivity.
185 replace (2^(S k)-1) with (2*(2^k-1)+1).
186 2: { rewrite Nat.pow_succ_r'. pose proof (Nat.pow_nonzero 2 k). lia. }
187 rewrite Dk_odd, IH. reflexivity.
188Qed.
190Lemma Dk_inc k: forall x, S x < 2^k -> exists t rest,
191 Dk k x = [1;1]^^t ++ [0;0] ++ rest /\ Dk k (S x) = [0;0]^^t ++ [1;1] ++ rest.
192Proof.
193 induction k as [|k IH]; intros x Hx.
194 1: cbn in Hx; lia.
195 rewrite Nat.pow_succ_r' in Hx.
196 destruct (Nat.Even_or_Odd x) as [[a ->]|[a ->]].
197 - exists O, (Dk k a). rewrite Dk_even.
198 replace (S (2*a)) with (2*a+1) by lia. rewrite Dk_odd. split; reflexivity.
199 - destruct (IH a) as [t [rest [E1 E2]]]. 1: lia.
200 exists (S t), rest. rewrite Dk_odd.
201 replace (S (2*a+1)) with (2*(S a)) by lia. rewrite Dk_even.
202 rewrite E1, E2. split; reflexivity.
203Qed.
205Lemma IncQ k x y: S x < 2^k -> Inc (Q k x y) (Q k (S x) y).
206Proof.
207 intros Hx l. unfold Q.
208 destruct (Dk_inc k x Hx) as [t [rest [E1 E2]]].
209 rewrite E1, E2, !Str_app_assoc. apply RIncG.
210Qed.
212(** ** Walks *)
214Lemma lp2 (b:nat) (X:side): [0;1]^^b *> [0;1;0;1] *> X = [0;1]^^(S (S b)) *> X.
215Proof.
216 change ([0;1;0;1] *> X) with ([0;1] *> [0;1] *> X).
217 rewrite !lpow_shift'. reflexivity.
218Qed.
220Lemma lp1 (b:nat) (X:side): [0;1]^^b *> [0;1] *> X = [0;1]^^(S b) *> X.
221Proof. rewrite lpow_shift'. reflexivity. Qed.
223(* W2: G(u (10)^2 1 (10)^b, r1) -> G(u 1 (10)^(b+2), r3), counts INC1, INC0 *)
224Lemma W2 u b r1 r2 r3: Inc r1 r2 -> Inc r2 r3 ->
225 HF (u <* [0;1;0;1] <* [1] <* [0;1]^^b) r1 -->+ HF (u <* [1] <* [0;1]^^(S (S b))) r3.
226Proof.
227 intros I1 I2.
228 eapply progress_trans. 1: apply (Cnt1 (u <* [0;1;0;1]) b r1 r2 I1).
229 eapply pt_eq. 1: apply (Cnt0 (u <* [1]) b r2 r3 I2).
230 apply HF_eq. 2: reflexivity.
231 apply lp2.
232Qed.
234(* W(a,b): G((10)^a 1 (10)^b, C n) -> E(a+b+[a odd], n+a+1), a+1 counts *)
235Lemma Wk a: forall b n,
236 HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
237 HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).
238Proof.
239 induction a as [a IH] using lt_wf_ind. intros b n.
240 destruct a as [|[|a]].
241 - eapply pt_eq. 1: apply (Cnt1 0inf b (C n) _ (IncC n)).
242 apply HF_eq. 2: f_equal; lia.
243 cbn [Nat.add Nat.modulo]. rewrite Nat.add_0_r.
244 cbn [Str_app]. rewrite <-const_unfold. reflexivity.
245 - eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]) b (C n) _ (IncC n)).
246 eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
247 instantiate (1:= 0inf <* [0;0;1;0] <* [0;1]^^b).
248 cbn [Str_app]. rewrite <-const_unfold. reflexivity. }
249 eapply pt_eq. 1: apply (Cnt0 0inf b (C (1+n)) _ (IncC (1+n))).
250 apply HF_eq. 2: f_equal; lia.
251 rewrite lp2. f_equal. f_equal.
252 pose proof (Nat.mod_upper_bound (S (S b)) 2).
253 cbn. lia.
254 - eapply progress_trans.
255 1: apply (W2 (0inf <* [0;1]^^a) b (C n) (C (1+n)) (C (1+(1+n))) (IncC n) (IncC (1+n))).
256 eapply pt_eq. 1: apply (IH a ltac:(lia) (S (S b)) (1+(1+n))).
257 apply HF_eq. 2: f_equal; lia.
258 f_equal. f_equal. lia.
259Qed.
261(* W2 iterated on Q: phase (d) of M5 *)
262Lemma W2Q t y i: forall u b x, x + 2*i < 2^t ->
263 HF (u <* [0;1;0;1]^^i <* [1] <* [0;1]^^b) (Q t x y) -->*
264 HF (u <* [1] <* [0;1]^^(b+2*i)) (Q t (x+2*i) y).
265Proof.
266 induction i as [|i IH]; intros u b x Hx.
267 - apply evstep_refl'. apply HF_eq. 2: f_equal; lia.
268 rewrite Nat.add_0_r. reflexivity.
269 - apply progress_evstep.
270 eapply progress_evstep_trans.
271 1: apply (W2 (u <* [0;1;0;1]^^i) b _ _ _ (IncQ t x y ltac:(lia)) (IncQ t (S x) y ltac:(lia))).
272 eapply evstep_trans. 1: apply (IH u (S (S b)) (S (S x)) ltac:(lia)).
273 apply evstep_refl'. apply HF_eq; lia_refl.
274Qed.
276(* B(s): G(u 1^(2s+1) (10)^j, C n) -> G(u 0 (10)^(s+j), C(n+s+1)), s+1 counts INC1 *)
277Lemma Bk s: forall j u n,
278 HF (u <* [1;1]^^s <* [1] <* [0;1]^^j) (C n) -->+
279 HF (u <* [0] <* [0;1]^^(s+j)) (C (n+s+1)).
280Proof.
281 induction s as [|s IH]; intros j u n.
282 - eapply pt_eq. 1: apply (Cnt1 u j (C n) _ (IncC n)).
283 apply HF_eq. 1: reflexivity. f_equal; lia.
284 - eapply progress_trans. 1: apply (Cnt1 (u <* [1;1]^^s <* [1;1]) j (C n) _ (IncC n)).
285 eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
286 instantiate (1:= u <* [1;1]^^s <* [1] <* [0;1]^^(S j)).
287 apply lp1. }
288 eapply pt_eq. 1: apply (IH (S j) u (1+n)).
289 apply HF_eq; lia_refl.
290Qed.
292(* W0(c,d): G(u 0 (10)^(2c+1) 0 (10)^d, C n) -> G(u (10)^(2c+2+d), C(n+2c+1)) *)
293Lemma W0k c: forall d u n,
294 HF (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [0] <* [0;1]^^d) (C n) -->+
295 HF (u <* [0;1]^^(2*c+2+d)) (C (n+2*c+1)).
296Proof.
297 induction c as [|c IH]; intros d u n.
298 - eapply pt_eq. 1: apply (Cnt0 u d (C n) _ (IncC n)).
299 apply HF_eq. 2: f_equal; lia.
300 rewrite lp2. reflexivity.
301 - eapply progress_trans.
302 1: apply (Cnt0 (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1]) d (C n) _ (IncC n)).
303 eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
304 instantiate (1:= u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1] <* [0;1]^^(S (S d))).
305 apply lp2. }
306 eapply progress_trans.
307 1: apply (Cnt1 (u <* [0] <* [0;1] <* [0;1;0;1]^^c) (S (S d)) _ _ (IncC (1+n))).
308 eapply pt_eq. 1: apply (IH (S (S d)) u (1+(1+n))).
309 apply HF_eq; lia_refl.
310Qed.
313(** ** Eat configurations and the macro rules M1-M5 *)
315Definition EC p N := HF (0inf <* [0;1]^^p) (C N).
317Lemma C_split m i: C (((m*2+1)*2^i-1)*2) = [0;0] *> [1;1]^^i *> [0;0] *> C m.
318Proof. unfold C. rewrite BinInc_mul2, BinInc_mulpow2sub1. reflexivity. Qed.
320Lemma C_odd n: C (n*2+1) = [1;1] *> C n.
321Proof. unfold C. rewrite BinInc_mul2add1. reflexivity. Qed.
323Lemma lp4 i (X:side): [0;1;0;1]^^i *> X = [0;1]^^(2*i) *> X.
324Proof.
325 induction i as [|i IH]. 1: reflexivity.
326 replace (2*S i) with (S (S (2*i))) by lia.
327 cbn [lpow]. rewrite Str_app_assoc, IH. reflexivity.
328Qed.
330(* M1: N odd *)
331Lemma BS1 p n: EC p (n*2+1) -->+ EC (p+2+p mod 2) (n+p+4).
332Proof.
333 unfold EC.
334 eapply progress_trans. 1: apply LEat.
335 eapply progress_trans. 1: apply Y1C.
336 eapply pt_eq. 1: apply (Wk (p+2) 0 (1+n)).
337 apply HF_eq. 2: f_equal; lia.
338 f_equal. f_equal.
339 pose proof (Nat.mod_upper_bound p 2). pose proof (Nat.mod_upper_bound (p+2) 2).
340 pose proof (Nat.div_mod p 2). pose proof (Nat.div_mod (p+2) 2). lia.
341Qed.
343(* M2: N = 0 mod 4 *)
344Lemma BS2 p n: EC p (n*4) -->+ EC (p+3+p mod 2) (n+p+4).
345Proof.
346 unfold EC.
347 eapply progress_trans. 1: apply LEat.
348 eapply progress_trans. 1: apply Y2C.
349 eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1;1]) 0 (C n) _ (IncC n)).
350 eapply pt_eq. 1: apply (Wk (p+2) 1 (1+n)).
351 apply HF_eq. 2: f_equal; lia.
352 f_equal. f_equal. lia.
353Qed.
355(* M3: N = 2 mod 8 *)
356Lemma BS3 p m: EC p (((m*2+1)*2^1-1)*2) -->+ EC (p+4+p mod 2) (m+p+6).
357Proof.
358 unfold EC.
359 eapply progress_trans. 1: apply LEat.
360 rewrite C_split.
361 eapply progress_trans. 1: apply (Y3 _ 0 (C m)).
362 eapply progress_trans. 1: apply (L1 (0inf <* [0;1]^^(p+2) <* [1]) 0).
363 eapply progress_trans. 1: apply (ROvf _ 0 m).
364 eapply pt_eq. 1: apply (Wk (S (S (p+2))) 0 (1+m)).
365 apply HF_eq. 2: f_equal; lia.
366 f_equal. f_equal. lia.
367Qed.
369(* M4: N = 6 mod 16 *)
370Lemma BS4 p m: EC p (((m*2+1)*2^2-1)*2) -->+ EC (p+7) (m+5).
371Proof.
372 unfold EC.
373 eapply progress_trans. 1: apply LEat.
374 rewrite C_split.
375 eapply progress_trans. 1: apply (Y3 _ 1 (C m)).
376 eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;1;1] *> C m))).
377 eapply progress_trans. 1: apply (LEat (S (p+2))).
378 eapply progress_trans. 1: apply Y4.
379 eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(S (p+2)+2) <* [0;1;1]) 0 _ _ (IncC _)).
380 eapply progress_trans. 1: apply (Cnt011 (0inf <* [0;1]^^(p+2+2)) _ _ (IncC _)).
381 eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2+2) <* [0;1;0]) 1 _ _ (IncC _)).
382 eapply pt_eq. 1: apply (Cnt0 (0inf <* [0;1]^^(p+2+2)) 1 _ _ (IncC _)).
383 apply HF_eq. 2: f_equal; lia.
384 replace (p+7) with (S (S (S (p+2+2)))) by lia. reflexivity.
385Qed.
387(* M5: N = (2m+1) 2^(t+4) - 2 with t' = t+1 >= 1, precondition 2^t' <= p+7 *)
388Lemma BS5 p m t: 2^(S t) <= p+7 ->
389 EC p (((m*2+1)*2^(S (S (S t)))-1)*2) -->+ EC (p+8+t) (m+2^(S t)+t+2).
390Proof.
391 intros Hp.
392 pose proof (Nat.pow_nonzero 2 t ltac:(lia)) as HT.
393 rewrite Nat.pow_succ_r' in Hp.
394 unfold EC.
395 (* (a) *)
396 eapply progress_trans. 1: apply LEat.
397 rewrite C_split.
398 eapply progress_trans. 1: apply (Y3 _ (S (S t)) (C m)).
399 (* (b) *)
400 eapply progress_trans.
401 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;0]^^(S t) *> [0] *> [1;1] *> C m))).
402 (* (c) *)
403 eapply progress_trans. 1: apply (LEat (S (p+2))).
404 eapply pt3. 1: apply (Y1Q _ ([0;0]^^t *> [0] *> [1;1] *> C m)).
405 1: { instantiate (1 := HF (0inf <* [0;1]^^(S (p+2)+2) <* [1]) (Q (S t) 1 (m*2+1))).
406 apply HF_eq. 1: reflexivity. unfold Q. rewrite Dk_1, C_odd, !Str_app_assoc. reflexivity. }
407 (* (d) *)
408 set (i := 2^t-1).
409 eapply evstep_progress_trans.
410 1: { eapply evstep_trans. 2: apply (W2Q (S t) (m*2+1) i (0inf <* [0;1]^^(p+7-2*2^t)) 0 1).
411 2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
412 apply evstep_refl'. apply HF_eq. 2: reflexivity.
413 rewrite lp4, lpow_add'. cbn [Str_app lpow]. unfold i. lia_refl. }
414 (* (e) *)
415 eapply progress_trans. 1: apply L1.
416 replace (Q (S t) (1+2*i) (m*2+1)) with ([1;1]^^(S t) *> [0;1;1] *> C m).
417 2: { unfold Q. replace (1+2*i) with (2^(S t)-1).
418 2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
419 rewrite Dk_full, C_odd. reflexivity. }
420 eapply progress_trans. 1: apply ROvf.
421 (* (f) *)
422 eapply progress_trans. 1: apply (Bk (S t) 0 _ (1+m)).
423 (* (g) *)
424 eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
425 instantiate (1 := 0inf <* [0;1]^^(p+7-2*2^t) <* [0] <* [0;1] <* [0;1;0;1]^^i <* [0] <* [0;1]^^(S t+0)).
426 rewrite lp4. f_equal. f_equal. cbn [Nat.add]. rewrite lpow_shift'. reflexivity. }
427 eapply pt_eq. 1: apply W0k.
428 apply HF_eq.
429 - rewrite lpow_add'. f_equal. f_equal. unfold i. lia.
430 - f_equal. unfold i. rewrite Nat.pow_succ_r'. lia.
431Qed.
433(** ** Start: 171 steps from the blank tape to E(2,4) (after TS) *)
435Lemma init: c0 -->* EC 2 4.
436Proof.
437 unfold EC, HF.
438 replace (C 4) with ([0;0;0;0;1;1] *> 0inf) by reflexivity.
439 change ([0;1]^^2) with [0;1;0;1].
440 solve_init.
441Qed.
443(** ** Invariant J(p,N): 1 <= N <= 2p *)
445Local Open Scope nat_scope.
447Lemma step_J p N: 1 <= N <= 2*p ->
448 exists p' N', EC p N -->+ EC p' N' /\ 1 <= N' <= 2*p'.
449Proof.
450 intros HJ.
451 destruct (Nat.Even_or_Odd N) as [[K ->]|[n ->]].
452 - destruct (Nat.Even_or_Odd K) as [[n ->]|[K' ->]].
453 + exists (p+3+p mod 2), (n+p+4). split.
454 * replace (2*(2*n)) with (n*4) by lia. apply BS2.
455 * lia.
456 + lowbitS_cases K'.
457 pose proof (Nat.pow_nonzero 2 i ltac:(lia)) as HT.
458 destruct i as [|[|i]].
459 * exists (p+4+p mod 2), (x+p+6). split.
460 -- replace (2*(2*((x*2+1)*2^0-1)+1)) with (((x*2+1)*2^1-1)*2) by (cbn; lia).
461 apply BS3.
462 -- cbn in HJ. lia.
463 * exists (p+7), (x+5). split.
464 -- replace (2*(2*((x*2+1)*2^1-1)+1)) with (((x*2+1)*2^2-1)*2) by (cbn; lia).
465 apply BS4.
466 -- cbn in HJ. lia.
467 * rewrite !Nat.pow_succ_r' in HJ.
468 set (T := 2^i) in *.
469 assert (x <= x*T) by nia.
470 exists (p+8+i), (x+2^(S i)+i+2). split.
471 -- replace (2*(2*((x*2+1)*2^(S (S i))-1)+1)) with (((x*2+1)*2^(S (S (S i)))-1)*2).
472 2: { rewrite !Nat.pow_succ_r'. fold T. lia. }
473 apply BS5. rewrite Nat.pow_succ_r'. fold T. lia.
474 -- rewrite Nat.pow_succ_r'. fold T. lia.
475 - exists (p+2+p mod 2), (n+p+4). split.
476 + replace (2*n+1) with (n*2+1) by lia. apply BS1.
477 + lia.
149Qed.478Qed.
151Lemma nonhalt: ~halts tm c0.480Lemma nonhalt: ~halts tm c0.
152Proof.481Proof.
153 eapply multistep_nonhalt with (c':=S (6,6)).
482 eapply multistep_nonhalt. 1: apply init.
154 1: unfold S; esx.
483 change (EC 2 4) with ((fun x : nat*nat => let (p,N) := x in EC p N) (2,4)).
155 eapply progress_nonhalt_cond with (P:=fun '(a,b) => a<=1+b).
484 apply progress_nonhalt_cond with (P := fun x : nat*nat => let (p,N) := x in 1 <= N <= 2*p).
156 2: lia.
485 - intros [p N] HJ. destruct (step_J p N HJ) as [p' [N' [H1 H2]]].
157 intros [a b] HP.
486 exists (p',N'). split; assumption.
158 lowbitS_cases a.
159 eexists (_,_).
160 split.
161 - apply BigStep.
162 zify_le_mul_r; lia.
163 - lia.487 - lia.
164Qed.488Qed.
490(*
4911RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC (only F0 is undefined; only C0 enters F)
493counter C(0) = 0^inf, C(2n) = 0 0 C(n), C(2n+1) = 1 1 C(n) (= BinInc [1;1] n)
494 D_k(x) = the k digits of x < 2^k, lowest first; Q_k(x, y) = D_k(x) 0 C(y)
495configs G(w, R) = 0^inf w 0 1 1 B> 0 R (count configuration: w a word, R a right half-tape)
496 E(p, N) = G((10)^p, C(N)) (eat configuration; EC p N is E(p,N) after TS)
497 Y(v, R) = 0^inf v 1 1 0 A> R
498 R = (11)^k 0 0 R' has R+ = (00)^k 1 1 R'
500count rules, for every word u and every R = (11)^k 0 0 R'
501INC1 G(u 1 (10)^b, R) -> G(u 0 (10)^b, R+)
502INC0 G(u 0 1 0 0 (10)^b, R) -> G(u 1 0 1 0 (10)^b, R+)
503INC011 G(u 1 0 1 1 0 0 (10)^b, R) -> G(u 0 1 0 1 1 0 (10)^b, R+)
504OVF G(u 1 (10)^b, Q_j(2^j-1, 2m+1)) -> G(u 0 (10)^(b+1) 1^(2j+1), C(m+1))
506eat rules
507EAT G(0^inf (10)^b, R) -> Y((10)^(b+2), R)
508Y1 Y(v, (11)^s 0 0 R') -> G(v 1, (00)^(s-1) 1 1 R') s >= 1
509Y2 Y(v, 0 0 0 0 R') -> G(v 1 1 1, R')
510Y3 Y(v, 0 0 1 1 (11)^s 0 0 R') -> G(v 1 1, 0^(2s+1) 1 1 R') s >= 0
511Y4 Y(v, 1 1 0 1 1 (11)^i 0 0 R') -> G(v 1 1 0 1, (00)^i 1 1 R')
513walks
514W(a,b) G((10)^a 1 (10)^b, C(n)) -> E(a+b+[a odd], n+a+1) a+1 counts INC1, INC0, INC1, ...
515W2 G(u (10)^2 1 (10)^b, R) -> G(u 1 (10)^(b+2), R++) INC1, INC0
516W0 G(u 0 (10)^(2c+1) 0 (10)^d, R) -> G(u (10)^(2c+2+d), R+^(2c+1)) INC0, INC1, ..., INC0
517B(t) G(u 1^(2t+1), R) -> G(u 0 (10)^t, R+^(t+1)) t+1 times INC1
519eat to eat E(p, N) -> E(p', N')
520M1 N odd EAT,Y1; W(p+2,0) p+2+[p odd], (N+1)/2 + p + 3
521M2 N = 0 (mod 4) EAT,Y2; INC1; W(p+2,1) p+3+[p odd], N/4 + p + 4
522M3 N = 8m+2 EAT,Y3(0); OVF(0,0); W(p+4,0) p+4+[p odd], m + p + 6
523M4 N = 16m+6 EAT,Y3(1); INC1; EAT,Y4; INC1; INC011; INC1; INC0 p+7, m + 5
524M5 N = (2m+1)2^(t+3)-2, t >= 1, p+7 >= 2^t
525 EAT,Y3(t+1); INC1; EAT,Y1(1); W2^(2^(t-1)-1);
526 OVF(2^t-2, t); B(t); W0(2^(t-1)-1, t) p+7+t, m + 2^t + t + 1
528invariant J(p, N): 1 <= N <= 2p. J(p, N) -> exactly one of M1..M5 applies, and J(p', N')
529start c0 -->(165) E(2, 4), so c0 -->(171) EC 2 4; J(2, 4) holds
530*)
3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

53 items in 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v (530 lines): 46 Lemma, 6 Definition, 1 Fixpoint. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.

#kindnamestatement (no proof body)linevs template
1Definitiontm
Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").
L32identicalexcept the TM string
2DefinitionC
Definition C n := BinInc [1;1] n.
L39new
3DefinitionHF
Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.
L40new
4LemmaRIncG
Lemma RIncG l r n:
l <* [1;1;0;1] {{A}}> [1;1]^^n *> [0;0] *> r -->+
l <{{E}} [1;0;1;1] *> [0;0]^^n *> [1;1] *> r.
L46new
5LemmaRInc
Lemma RInc n l:
l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
L52new
6LemmaL1
Lemma L1 u b r:
HF (u <* [1] <* [0;1]^^b) r -->+ u <* [0] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
L59new
7LemmaL0
Lemma L0 u b r:
HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ u <* [0;1;0;1] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
L63new
8LemmaL011
Lemma L011 u r:
HF (u <* [0;0;1;1;0;1]) r -->+ u <* [0;1;1;0;1;0] <* [1;1;0;1] {{A}}> r.
L67new
9LemmaLEat
Lemma LEat b r:
HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
L72new
10LemmaY1C
Lemma Y1C v n:
v <* [0;1;1] {{A}}> C (n*2+1) -->+ HF (v <* [1]) (C (1+n)).
L77new
11LemmaY2C
Lemma Y2C v n:
v <* [0;1;1] {{A}}> C (n*4) -->+ HF (v <* [1;1;1]) (C n).
L85new
12LemmaY3
Lemma Y3 v s r:
v <* [0;1;1] {{A}}> [0;0] *> [1;1] *> [1;1]^^s *> [0;0] *> r -->+
HF (v <* [1;1]) ([0;0]^^s *> [0] *> [1;1] *> r).
L92new
13LemmaY4
Lemma Y4 v m:
v <* [0;1;1] {{A}}> [1;1;0] *> [1;1] *> C m -->+ HF (v <* [1;0;1;1]) (C (1+m)).
L97new
14LemmaY1Q
Lemma Y1Q v r:
v <* [0;1;1] {{A}}> [1;1] *> [0;0] *> r -->+ HF (v <* [1]) ([1;1] *> r).
L104new
15LemmaROvf
Lemma ROvf l j m:
l <* [1;1;0;1] {{A}}> [1;1]^^j *> [0;1;1] *> C m -->+
HF (l <* [0;1] <* [1;1]^^j <* [1]) (C (1+m)).
L109new
16DefinitionInc
Definition Inc r r' := forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'.
L119new
17LemmaIncC
Lemma IncC n: Inc (C n) (C (1+n)).
L121new
18LemmaInc00
Lemma Inc00 r: Inc ([0;0] *> r) ([1;1] *> r).
L124new
19Lemmapt3
Lemma pt3 c1 c2 c2' c3: c1 -->+ c2 -> c2 = c2' -> c2' -->+ c3 -> c1 -->+ c3.
L127new
20Lemmapt_pre
Lemma pt_pre c1 c1' c2: c1 = c1' -> c1' -->+ c2 -> c1 -->+ c2.
L130new
21Lemmapt_eq
Lemma pt_eq c1 c2 c3: c1 -->+ c2 -> c2 = c3 -> c1 -->+ c3.
L133new
22LemmaHF_eq
Lemma HF_eq l l' r r': l = l' -> r = r' -> HF l r = HF l' r'.
L136new
23LemmaCnt1
Lemma Cnt1 u b r r': Inc r r' ->
HF (u <* [1] <* [0;1]^^b) r -->+ HF (u <* [0] <* [0;1]^^b) r'.
L139new
24LemmaCnt0
Lemma Cnt0 u b r r': Inc r r' ->
HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ HF (u <* [0;1;0;1] <* [0;1]^^b) r'.
L143new
25LemmaCnt011
Lemma Cnt011 u r r': Inc r r' ->
HF (u <* [0;0;1;1;0;1]) r -->+ HF (u <* [0;1;1;0;1;0]) r'.
L147new
26FixpointDk
Fixpoint Dk (k x : nat) : list Sym :=
match k with
| O => []
| S k' => (if Nat.odd x then [1;1] else [0;0]) ++ Dk k' (Nat.div2 x)
end.
L153new
27DefinitionQ
Definition Q k x y := Dk k x *> [0] *> C y.
L159new
28LemmaDk_even
Lemma Dk_even k a: Dk (S k) (2*a) = [0;0] ++ Dk k a.
L161new
29LemmaDk_odd
Lemma Dk_odd k a: Dk (S k) (2*a+1) = [1;1] ++ Dk k a.
L168new
30LemmaDk_0
Lemma Dk_0 k: Dk k 0 = [0;0]^^k.
L176new
31LemmaDk_1
Lemma Dk_1 k: Dk (S k) 1 = [1;1] ++ [0;0]^^k.
L179new
32LemmaDk_full
Lemma Dk_full k: Dk k (2^k-1) = [1;1]^^k.
L182new
33LemmaDk_inc
Lemma Dk_inc k: forall x, S x < 2^k -> exists t rest,
Dk k x = [1;1]^^t ++ [0;0] ++ rest /\ Dk k (S x) = [0;0]^^t ++ [1;1] ++ rest.
L190new
34LemmaIncQ
Lemma IncQ k x y: S x < 2^k -> Inc (Q k x y) (Q k (S x) y).
L205new
35Lemmalp2
Lemma lp2 (b:nat) (X:side): [0;1]^^b *> [0;1;0;1] *> X = [0;1]^^(S (S b)) *> X.
L214new
36Lemmalp1
Lemma lp1 (b:nat) (X:side): [0;1]^^b *> [0;1] *> X = [0;1]^^(S b) *> X.
L220new
37LemmaW2
Lemma W2 u b r1 r2 r3: Inc r1 r2 -> Inc r2 r3 ->
HF (u <* [0;1;0;1] <* [1] <* [0;1]^^b) r1 -->+ HF (u <* [1] <* [0;1]^^(S (S b))) r3.
L224new
38LemmaWk
Lemma Wk a: forall b n,
HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).
L235new
39LemmaW2Q
Lemma W2Q t y i: forall u b x, x + 2*i < 2^t ->
HF (u <* [0;1;0;1]^^i <* [1] <* [0;1]^^b) (Q t x y) -->*
HF (u <* [1] <* [0;1]^^(b+2*i)) (Q t (x+2*i) y).
L262new
40LemmaBk
Lemma Bk s: forall j u n,
HF (u <* [1;1]^^s <* [1] <* [0;1]^^j) (C n) -->+
HF (u <* [0] <* [0;1]^^(s+j)) (C (n+s+1)).
L277new
41LemmaW0k
Lemma W0k c: forall d u n,
HF (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [0] <* [0;1]^^d) (C n) -->+
HF (u <* [0;1]^^(2*c+2+d)) (C (n+2*c+1)).
L293new
42DefinitionEC
Definition EC p N := HF (0inf <* [0;1]^^p) (C N).
L315new
43LemmaC_split
Lemma C_split m i: C (((m*2+1)*2^i-1)*2) = [0;0] *> [1;1]^^i *> [0;0] *> C m.
L317new
44LemmaC_odd
Lemma C_odd n: C (n*2+1) = [1;1] *> C n.
L320new
45Lemmalp4
Lemma lp4 i (X:side): [0;1;0;1]^^i *> X = [0;1]^^(2*i) *> X.
L323new
46LemmaBS1
Lemma BS1 p n: EC p (n*2+1) -->+ EC (p+2+p mod 2) (n+p+4).
L331new
47LemmaBS2
Lemma BS2 p n: EC p (n*4) -->+ EC (p+3+p mod 2) (n+p+4).
L344new
48LemmaBS3
Lemma BS3 p m: EC p (((m*2+1)*2^1-1)*2) -->+ EC (p+4+p mod 2) (m+p+6).
L356new
49LemmaBS4
Lemma BS4 p m: EC p (((m*2+1)*2^2-1)*2) -->+ EC (p+7) (m+5).
L370new
50LemmaBS5
Lemma BS5 p m t: 2^(S t) <= p+7 ->
EC p (((m*2+1)*2^(S (S (S t)))-1)*2) -->+ EC (p+8+t) (m+2^(S t)+t+2).
L388new
51Lemmainit
Lemma init: c0 -->* EC 2 4.
L435new
52Lemmastep_J
Lemma step_J p N: 1 <= N <= 2*p ->
exists p' N', EC p N -->+ EC p' N' /\ 1 <= N' <= 2*p'.
L447new
53Lemmanonhalt
Lemma nonhalt: ~halts tm c0.
L480adapted
4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.
submission/proof.md line 58: 1. Rule table (busycoq comment-block style)
1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC          (only F0 is undefined; only C0 enters F)

counter    C(0) = 0^inf,  C(2n) = 0 0 C(n),  C(2n+1) = 1 1 C(n)        = BinInc [1;1] n
           t1(n) = number of trailing 1 bits of n
           D_k(x) = the k digits of x < 2^k, lowest first;   Q_k(x, y) = D_k(x) 0 C(y)
configs    G(w, R) = 0^inf w 0 1 1 B> 0 R          (count configuration: w a word, R a right half-tape)
           E(p, N) = G((10)^p, C(N)),  N >= 1       (eat configuration)
           Y(v, R) = 0^inf v 1 1 0 A> R
           R = (11)^k 0 0 R'  has  R+ = (00)^k 1 1 R'
           C(n)+ = C(n+1)  (k = t1(n));   Q_j(x, y)+ = Q_j(x+1, y) if x+1 < 2^j  (k = t1(x))

count rules, for every word u and every R = (11)^k 0 0 R'                               steps
INC1    G(u 1 (10)^b, R)              -> G(u 0 (10)^b, R+)                              6b + 4k + 24
INC0    G(u 0 1 0 0 (10)^b, R)        -> G(u 1 0 1 0 (10)^b, R+)                        6b + 4k + 32
INC011  G(u 1 0 1 1 0 0 (10)^b, R)    -> G(u 0 1 0 1 1 0 (10)^b, R+)                    6b + 4k + 40
OVF     G(u 1 (10)^b, Q_j(2^j-1, 2m+1)) -> G(u 0 (10)^(b+1) 1^(2j+1), C(m+1))           6b + 2j + 4 t1(m) + 29

eat rules, for every u, v, R'
EAT     G(u 0 0 0 (10)^b, R)          -> Y(u (10)^(b+2), R)            (any R)          4b + 17
Y1      Y(v, (11)^s 0 0 R')           -> G(v 1, (00)^(s-1) 1 1 R')     s >= 1           4s + 9
Y2      Y(v, 0 0 0 0 R')              -> G(v 1 1 1, R')                                 7
Y3      Y(v, 0 0 1 1 (11)^s 0 0 R')   -> G(v 1 1, 0^(2s+1) 1 1 R')     s >= 0           4s + 20
Y4      Y(v, 1 1 0 1 1 (11)^i 0 0 R') -> G(v 1 1 0 1, (00)^i 1 1 R')                    4i + 18

walks, for every u
W(a,b)  G((10)^a 1 (10)^b, C(n))      -> E(a+b+[a odd], n+a+1)          a+1 counts INC1, INC0, INC1, ...
W2      G(u (10)^2 1 (10)^b, R)       -> G(u 1 (10)^(b+2), R++)          INC1, INC0
W0      G(u 0 (10)^(2c+1) 0 (10)^d, R) -> G(u (10)^(2c+2+d), R+^(2c+1))  INC0, INC1, ..., INC0
B(t)    G(u 1^(2t+1), R)              -> G(u 0 (10)^t, R+^(t+1))         t+1 times INC1

eat to eat                                                                  E(p, N) -> E(p', N')
M1  N odd                EAT,Y1; W(p+2,0)                                   p+2+[p odd],  (N+1)/2 + p + 3
M2  N = 0 (mod 4)        EAT,Y2; INC1; W(p+2,1)                             p+3+[p odd],  N/4 + p + 4
M3  N = 8m+2             EAT,Y3(0); OVF(0,0); W(p+4,0)                      p+4+[p odd],  m + p + 6
M4  N = 16m+6            EAT,Y3(1); INC1; EAT,Y4; INC1; INC011; INC1; INC0  p+7,          m + 5
M5  N = (2m+1)2^(t+3)-2, t >= 1, p+7 >= 2^t
                         EAT,Y3(t+1); INC1; EAT,Y1(1); W2^(2^(t-1)-1);
                         OVF(2^t-2, t); B(t); W0(2^(t-1)-1, t)              p+7+t,        m + 2^t + t + 1

invariant J(p, N):  1 <= N <= 2p.   J(p, N) -> exactly one of M1..M5 applies, and J(p', N')
start      c0 -->(7) G(1, C(0)) -->(24, INC1) E(0,1) -->(134, M1) E(2,4)   (step 165),  J(2,4)
           (.v form, §8: EC 2 4 = E(2,4) after TS, at step 171)
5FamilyCheck: related machines are killed together or have a reason to be left open.

1 machines, 1 killed, 0 not. Family links: status.json parent, same transition table with another start (tools/dashboard.py), targeting.md follow-on rows, ledger "= twin" notes. A machine string named in a .v header / proof.md / notes.md is listed but does not make a family.

whomachinestatusrelation to this kill
W5-3 kill 241RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC✓Killed: never haltsthis kill
Named in a file but not linked (not counted as family)
W6-31RB1LC_1LA1RF_0RD1RD_0RA0LE_1LA0LE_0RC---⚠Cryptid candidatenamed in W6-3's notes.md · mechanism
W6-51RB0LB_0LC0RE_1LA1LD_0LB1LD_1RA0RF_1RA---⚠Cryptid candidatenamed in W6-5's notes.md · mechanism
6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.
  • ✓
    Machine string exact
    the .v literal == holdout list line 141 byte for byte
  • ✓
    Statement is ~halts tm c0
    parsed from the .v and confirmed by check_kill (theorem_text, theorem_rocq)
  • ✓
    No axioms beyond baseline
    0 assumption(s); tools/assumptions_baseline.txt allows only functional_extensionality_dep
  • ✓
    coqchk finished (optional)
    coqchk pass in 1.0 s
  • ✓
    .v hash matches the checked hash
    .v = checked sha256 75932a97949d…; submission/ copy = checked sha256 75932a97949d…
  • ✓
    No repo-local paths in the .v
    comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
  • ✓
    Public write-up is clean
    tools/writeup_lint.py on submission/proof.md: 0 error(s)
  • ○
    proof.md reviewed by Dennis (Checkpoint B)
    no Checkpoint B note from Dennis found
    • notes.md L80: - proof.md: complete informal proof (Checkpoint B pending). 16 exact low-level rules; count rules INC1/INC0/INC011/OVF; eat rules EAT + Y1..Y4; walk lemmas W, W2, W0, B; macro rules M1..M5 with closed form; invariant J:
    • notes.md L96: - Not done: Discord post and upstream PR (Dennis's call). Checkpoint B notes: none on file at packaging time.
    • proof.md L562: - **Checkpoint B (Dennis).** Pending (non-blocking).
    • proof.md L590: - Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
    • proof.md L598: - Public text: §9 has no file paths or script names; the observe-notes cross-references, "ground rule 6", the W4-2 mention, Checkpoint B and the file list moved to a working-copy appendix. Everything above the appendix l
    • proof.md L601: - Status: CHECKPOINT_B. No fatal or major gap remains. Still open: Dennis's Checkpoint B notes (non-blocking) and formalization (§8).
  • ○
    Family posted together?
    no other kill in the family

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.0 s from the files linked above; nothing in this review is hand-written except the box “How we proved it never halts” (above), which quotes how_proved.md. Re-run: python3 -B tools/killreview.py 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC

Files

machines/<tm>/: 12 entries · raw notes, status, scripts, images

namesizechanged
notes.md ↓12 KB2026-10-13 03:13
proof.md ↓41 KB2026-10-13 02:46
how_proved.md ↓1.6 KB2026-10-14 10:51
status.json ↓1.4 KB2026-10-13 03:13
observe.json ↓14 KB2026-10-13 01:30
1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v ↓20 KB2026-10-13 03:05
img/6 items2026-10-13 01:21
rocq/8 items2026-10-13 03:06
scripts/39 items2026-10-13 01:26
submission/5 items2026-10-14 09:18
work/15 items2026-10-13 02:00
check_proof.py ↓43 KB2026-10-13 02:42
status.json in full
{
 "tm": "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "label": "W5-3",
 "confidence": "high",
 "template": "verify/BECv5.v Module TM1 (architecture only: BinInc counter + defect budget + ROv-style eat + progress_nonhalt_cond)",
 "family_note": "No siblings: canon from all 6 starts against the 740 and 778 lists finds only this machine; singleton group in 2026-10-07_eqv_1590.txt.",
 "proof": {
  "file": "proof.md",
  "checker": "check_proof.py",
  "logs": [
   "work/check_proof_seed1.log",
   "work/check_proof_seed2.log",
   "work/check_proof_full_seed1.log"
  ],
  "invariant": "1 <= N <= 2p on E(p,N) = G((10)^p, C(N))",
  "start": "E(2,4) at step 165 (H form S(2,4) at step 171)",
  "checks": "108/108 PASS (seed 1, seed 2 default; seed 1 --full)"
 },
 "review": {
  "skeptic_round_1": "sound; 7 minor gaps; all fixed 2026-10-13"
 },
 "kill": {
  "file": "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v",
  "sha256": "75932a97949d61ba11f16e0b8a6d0d6adf05f2e1a63231b44f0acddf0661da1a",
  "lines": 530,
  "check_kill": "PASS (fresh run 2026-10-13T10:09:16Z: compile 3.4 s native, coqchk pass 1.0 s, 0 assumptions; also rocq/check_kill_round1.log and the independent auditor run, same sha256)",
  "submission": "submission/",
  "discord": "submission/discord.md, not posted (fill in <LINK>)"
 }
}
observe.json contract (tools/README-card.md):
2 contract warnings
  • rank: missing
  • diagrams[3].window: not "cells A..B, 1 px = k cells"