Built . It shows the files as they were then (ages and “working now” follow your clock). tools/rebuild_pages.sh rebuilds the site within 5 minutes of a change; by hand: python3 -B tools/site.py.

Machines / #4

`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---`

#4local proof 2Kill claimedSync bouncer counterbbchallenge ↗Explorer

How we proved it never halts

Both cycle formulas keep the block counts in a safe region

The tape is a binary counter at the left end, four cells per digit, followed by a row of five-cell blocks: "A" blocks 00111 and "B" blocks 10111. The head bounces between the counter and the right end, adding 1 to the counter on every visit and, along the way, new B blocks at the right end.

When the counter rolls over, it gains a digit, and a three-cell marker 111 appears just to its right. The marker walks right through the A blocks, two blocks for every three counts, and on reaching the B blocks turns them all into A blocks. Then the cycle repeats, one digit longer.

The key idea: at each cycle start, count the A blocks ahead of the new marker and the B blocks beyond them (a rollover in mid-conversion needs a small correction). One cycle changes this pair of counts by one of two exact formulas, chosen by whether the A count is even or odd, a choice that looks random.

Why that settles it: the machine stays on these rails only if the timing works out, for example the marker finishing its walk before the next rollover. Scale both counts by the counter's size and each cycle start becomes a point in the plane. The proof finds a six-sided region where every timing condition holds and which both formulas map into itself, so the even/odd choices never matter. The run is inside it at step 17,215, so it never leaves the rails and never uses the missing transition.

The Rocq proof (checked against busycoq) checks the 21 basic tape moves by running them, the longer moves by induction, the region by linear arithmetic, and the first 17,215 steps by exact replay.

#2local proof number

504lines of Rocq

6 sto compile

6/6automatic checks

Overview

In one sentence

TM4's binary counter + 00111/10111 block bouncer; 7 phase rules validated; parity branch, both branches safe

Submitted mechanism On the left is a binary counter C_k(n): k digits, MSB first, 1 = 1010, 0 = 0010 (TM4's d1/d0). The head bounces between the counter and the right edge, adding 1 to the counter on each visit. Between them is a row of 5-cell blocks, A = 00111 and B = 10111. (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #24merged 2026-10-16 07:07 UTC by ccz181078 · SBCv13.v · TM1 · on Submissions →
Rocq proof: check_kill PASS · first Oct 10 05:13
504 lines · 20 KB .v · compile 6.4 s · coqchk pass · 0 axioms · PASS Oct 10 05:13 (re-run Oct 10 11:50)
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/SBCv7.v Module TM4 (adapted from) · details in Proof →
Class: Sync bouncer counterours: Sync bouncer counter (sheet) · ours adds: TM4 binary counter + 3-block bouncer with moving front · high confidence
On the list: not on BB6_holdouts_663.txt (line 645 of the previous list) · historical 740 line 645
#4eqv ×1sim 1e15UBRRBAlongit.

Mechanism

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

How it works: 3 notes

Left: TM4's binary counter, k bits MSB first (1=1010, 0=0010), +1 per bounce.
Right: A blocks 00111, one 111 marker (the front), B blocks 10111. P phase: each bounce adds a B block.
Overflow: counter gains a bit; the front moves right 2 A blocks per visit; on reaching B, all B blocks become A blocks.

Figures for Checkpoint A

Fig 1 · Left/right records to 2.7M stepsQ1 Q2 viewer ↗
Edge records to 2.7M steps. Look at each horizontal reset and the diagonal that follows it.

Fig 2 · One cycle up close, every 60 stepsQ1
One cycle of the same run, up close: every 60 steps from step 74,114, the tape Q(8,129,1,24,29).

More figures (2)Fig 3–4: Blaze, 10 million steps · bbchallenge default view, first 10,000 steps

Rules (7/7 validated)exact tape rewrites the proof will formalize, each re-checked by simulation

rule	from ⟶ to	cases	steps	checked
R1 P-bounce	0^∞ C_k(n) (00111)^X (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_k(n+1) (00111)^X (10111)^z+1 00 C> 0^∞	n+1 <= 2^k-1, X >= 1	32X+32z+16t(n)+47, t(n) = trailing 1-bits of n	✓65/65
R2 overflow	0^∞ C_k(2^k-1) (00111)^X (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_(k+1)(2^k+1) 00111 111 (00111)^X-2 (10111)^z+1 00 C> 0^∞	X >= 2	—	✓25/25
R3 Q-bounce (front +2)	0^∞ C_k(n) (00111)^x 111 (00111)^y+2 (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_k(n+3) (00111)^x+2 111 (00111)^y (10111)^z+1 00 C> 0^∞	n+3 <= 2^k-1	96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197	✓65/65
R4 even end (y=0)	0^∞ C_k(n) (00111)^x 111 (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_k(n+z+2) (00111)^x+z+1 00 C> 0^∞	n+z+2 <= 2^k-1	—	✓25/25
R5 odd end (y=1)	0^∞ C_k(n) (00111)^x 111 00111 (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_k(n+2z+7) (00111)^x+z+4 00 C> 0^∞	n+2z+7 <= 2^k-1	—	✓25/25
R4o even end + overflow	0^∞ C_k(n) (00111)^x 111 (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_(k+1)(2^k+1+3m) (00111)^1+2m 111 (00111)^x+z-1-2m 00 C> 0^∞	m = n+z+2-2^k >= 0, x+z <= 2^(k-1); outside that regime 2/25 fail	—	✓25/25
R5o odd end + overflow	0^∞ C_k(n) (00111)^x 111 00111 (10111)^z 00 C> 0^∞ ⟶ 0^∞ C_(k+1)(2^k+1+3m) (00111)^1+2m 111 (00111)^x+z+2-2m 00 C> 0^∞	m = n+2z+7-2^k >= 0, x+z <= 2^(k-1); outside that regime 4/25 fail	—	✓50/50

Compressed historythe tape as 0^∞ C_k(n) (00111)^x [111 (00111)^y] (10111)^z 00 C> 0^∞ at 38 moments: where the rules are read off

0^∞ C_k(n) (00111)^x [111 (00111)^y] (10111)^z 00 C> 0^∞

step	`phase`	`k`	`n`	`x`	`y`	`z`
1,047	P	4	14	4	-	0
1,222	P	4	15	4	-	1
1,507	Q	5	17	1	2	2
1,912	Q	5	20	3	0	3
2,826	P	5	25	7	-	0
4,996	P	5	31	7	-	6
5,553	Q	6	33	1	5	7
7,003	Q	6	39	5	1	9
17,215	Q	7	65	1	16	0
27,975	Q	7	89	17	0	8
35,105	P	7	99	26	-	0
72,213	P	7	127	26	-	28
74,114	Q	8	129	1	24	29
108,318	Q	8	165	25	0	41
172,672	P	8	208	67	-	0
310,913	P	8	255	67	-	47
314,750	Q	9	257	1	65	48
518,654	Q	9	353	65	1	80
1,101,764	Q	10	537	17	131	0
1,824,857	Q	10	732	147	1	65
2,625,871	P	10	869	216	-	0
4,076,949	P	10	1,023	216	-	154
4,089,010	Q	11	1,025	1	214	155
6,289,433	Q	11	1,346	215	0	262
9,222,995	P	11	1,610	478	-	0
18,983,294	P	11	2,047	478	-	437
19,012,811	Q	12	2,049	1	476	438
30,552,161	Q	12	2,763	477	0	676
48,261,531	P	12	3,441	1,154	-	0
79,286,557	P	12	4,095	1,154	-	654
79,344,666	Q	13	4,097	1	1,152	655
139,306,778	Q	13	5,825	1,153	0	1,231
209,134,028	P	13	7,058	2,385	-	0
316,196,767	P	13	8,191	2,385	-	1,133
316,309,612	Q	14	8,193	1	2,383	1,134
564,062,495	Q	14	11,766	2,383	1	2,325
1,093,007,525	Q	15	16,502	79	4,632	0
2,318,632,923	P	15	25,768	7,028	-	0

phaselast P

not plottable

klast 15

nlast 25,768

xlast 7,028

ylast -

zlast 0

Template comparisonSBCv7.v TM4: partly applies · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	0LA
B	0RC	1RD
C	0LD	1RE
D	1LA	0RB
E	0RD	1RF
F	1RCtpl 0RA	---

differs from the template

file: SBCv7.v:610
module: TM4 (line 610); also TM37 (line 7021)
machine: 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA--- (1 transition apart)
diff: F0 only: 0RA (TM4) / 1RB (TM37) -> 1RC; A-E identical
note: Left counter carries over (same d1/d0 digits; TM37's overflow form reached 5/5). Right side doesn't: TM4's BigStep holds 2/8, only when F0 is never read.

Proof strategy & riskshow the formal proof will go · 3 risks to watch

Longitudinal proof in TM4 style: reuse the counter lemma (BC.Mul2/BC.Incs on d0/d1), add new segRLs lemmas for 00111/10111/111 words, prove R1-R5o with es/ind/follow. Then progress_nonhalt_cond with a linear invariant on (n, X, z)/2^k that holds for both parity branches. init: c0 -->* Q(5,17,1,2,2) at step 1507 by esx.

▲Branch = parity of X (X grows ~3X/2: Collatz-like); proof needs an invariant valid for both branches (holds numerically under adversarial branching to k=600).
▲R5o (odd end + overflow) has front and conversion running at once: hardest low-level lemma.
▲Outside the regime (x+z >> 2^k) the head breaks through the counter and can halt; the invariant must exclude this.

Stats & provenance3·10⁹ steps simulated · 48,013 cells · the status in full · files

simulated: 3·10⁹ steps
tape: 48,013 cells · 22,929 nonzeros
growth: span ~ t^0.5 (cycle k: ~2^k blocks in ~4^k steps); left edge -2 cells per cycle
status now: check_kill PASS, independently re-verified (status.json, 2026-10-10)
observer's note: Mechanism found; 7 rules validated by simulation; the phase map built from them reproduces all 36 phase boundaries in history from step 1507 (its start) to 2.3e9 steps. Parity branch present but halting does not depend on it.
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v

Proof & checks

6/6 automatic checks pass

Kill 2 · Sync bouncer counter · the kill file 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v: 504 lines, 73 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/SBCv7.v Module TM4 · 7% 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

1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

vs holdout list

✓ byte-exact: the .v literal (L18) == 2026-10-07_778.txt line 681 (41 bytes, via tools/holdouts.py)

Theorem

✓ Lemma nonhalt: ~halts tm c0. L466

check_kill

✓ PASS · 17/17 checks pass · compile 6.42 s · coqchk pass (2.04 s) · assumptions: 0 (closed) · 2026-10-10 18:50:58 UTC · submission/check_kill.txt

Checked .v

sha256 51e3dea1f666153c…

✓	1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v	`51e3dea1f666153c…` = checked
✓	submission/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v	`51e3dea1f666153c…` = checked

Status

✓Killed: never halts updated 2026-10-10

✓ 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

✓	`args`	6x2 machine, framework module Individual62, mode nonhalt
✓	`input`	20787 bytes, 504 lines, 532 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	13 needed framework .vo files present and fresh, with native code no older than the .vo
✓	`forbidden`	none of 30 forbidden patterns occur (ground rule 1's words: anywhere; command words: outside comments and strings; comments never split a token)
✓	`structure`	4 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 18: TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---" == <tm> (41 bytes)
✓	`theorem_text`	line 466: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 6.4s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---") c0 with absolute names (in-file and isolated)
✓	`isolation`	only stock proof plugins loaded; guard/positivity/universe checking on, definitional UIP off
✓	`assumptions`	0 assumption(s), all in the baseline
✓	`coqchk`	coqchk -norec BB6Kill.Candidate ok (2.0s); its context summary lists nothing of the file's own
✓	`integrity`	input 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/SBCv7.v Module TM4 · detected from 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v line 5

7%of our lines identical to the template

4changed lines

394added lines (ours only)

154template lines dropped

1 / 1 / 71items identical / adapted / new

What the package README says it reused and changed (submission/README.md line 18, Template and what changed), quoted:

This extends SBCv7.v Module TM4 (1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA---), which differs only in F0 (0RA there, 1RC here). TM1, TM2, TM3, TM18 and TM37 in that file also differ only in F0.

Kept: TM4's moving head <A 001 / 001 E> (hL/hR), its digits d0/d1, and the overall shape: init, a big step per cycle, and progress_nonhalt_cond with a linear invariant.
Changed:
F0 = 1RC changes every right-side word. TM4's unary right counter is replaced by the A/B blocks, the front gadget (FL, FR1–FR3) and the conversion gadget.
TM4's Longitudinal counter lemma is replaced by a direct Fixpoint ctr, so the file imports only Individual62, Arith, Lia and String.
TM4's one-inequality invariant is replaced by a 6-facet hexagon that holds on both branches.
New lemmas ConvOV/PostOV cover the overflow during an odd conversion.

The file is 504 lines, about 3 times TM4's 170. The informal proof is proof.md.

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 428 lines

7% identical · 4 changed · 394 added

template 188 lines

16% kept verbatim · 154 not in ours

our items 73

1 identical · 1 adapted · 71 new · 18 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 1–57 (shared header, before the first Module) + 611–778 (body of Module TM4; the Module/End lines left out). Ours: lines 13–504 (header comment 1–12 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: lrcons_lpow1', sideRLs_wall, tm', LIncs, Incs, RC0, Incs0, Incs', RCa, RCb, cons, RCb_shift, Rn, Rn_cons, RIncs, S, Rst, BigStep

Other references found:

template vendor/busycoq/verify/SBCv7.v (named in submission/proof.md line 222)

Side-by-side diff: template (188 lines) vs ours (428 lines), 552 lines differ; runs of identical lines and long template-only runs folded

identicalequal once each TM string is <TM>changedours onlytemplate only

template		ours
1	From BusyCoq Require Import Individual62.	14	From BusyCoq Require Import Individual62.
2	Require Import ZifyNat Lia.	15	Require Import Arith Lia.
3	Require Import ZArith.
4	Require Import String.	16	Require Import String.
5	Require Import List.
6	From BusyCoq Require Import Longitudinal.
⋯ 35 template-only lines (template 7–51), not in ours
53	Ltac am a a' k b b' :=
54	applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.
612	Definition tm := Eval compute in (TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_0RA---").	18	Definition tm := Eval compute in (TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---").
613	Definition tm' := flip tm.
615	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	20	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
616	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	21	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
618	Notation hR := (E,<[0;0;1]).
		23	Open Scope list.
619	Notation hL := (A,[0;0;1]).
620	Notation hRL := [(hR,hL)].
621	Notation hLR := [(hL,hR)].
623	Notation d0 := <[0;0;1;0].	25	Notation d0 := <[0;0;1;0].
624	Notation d1 := <[1;0;1;0].	26	Notation d1 := <[1;0;1;0].
625	Notation dh := (0inf <* d1).
		27	Notation bA := <[0;0;1;1;1].
627	Notation w0 := [0;0;1;0;0].	28	Notation bB := <[1;0;1;1;1].
628	Notation w1 := [0;0;1;0;1].	29	Notation bAr := [0;0;1;0;1].
629	Notation w0' := [0;0;0;0;1].	30	Notation bBr := [0;0;0;0;1].
630	Notation w1' := [1;0;1;0;0].
		32	Ltac fw H := eapply evstep_trans; [solve [apply H; lia] \| ].
632	Lemma LIncs n:
		33	Ltac fp H := eapply progress_evstep_trans; [solve [apply H; lia] \| ].
633	sideRLs tm' (hLR^^((2^n-1)2)) (dh < d0^^n <* d1) (dh <* d1^^(1+n)).
		35	Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.
		36	Proof. intros H E. subst. exact H. Qed.
		38	Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.
		39	Proof. intros H E. subst. exact H. Qed.
		41	(** * Shift rules (proof.md 3.1) *)
		43	Lemma ENDL l : l <* <[0;0] {{C}}> 0inf -->+ l <{{A}} [0;0;1] *> 0inf. Proof. es. Qed.
		44	Lemma AL l r : l <* bA <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bAr > r. Proof. es. Qed.
		45	Lemma BL l r : l <* bB <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bBr > r. Proof. es. Qed.
		46	Lemma AR l r : l <* <[0;0;1] {{E}}> bAr > r --> l <* bA <* <[0;0;1] {{E}}> r. Proof. es. Qed.
		47	Lemma BR l r : l <* <[0;0;1] {{E}}> bBr > r --> l <* bB <* <[0;0;1] {{E}}> r. Proof. es. Qed.
		48	Lemma ENDR l : l <* <[0;0;1] {{E}}> 0inf -->* l <* bB <* <[0;0] {{C}}> 0inf. Proof. es. Qed.
		49	Lemma D1L l r : l <* d1 <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;1;0;1] > r. Proof. es. Qed.
		50	Lemma FLIP l r : l <* d0 <{{A}} [0;0;1] > r --> l <* d1 <* <[0;0;1] {{E}}> r. Proof. es. Qed.
		51	Lemma D0R l r : l <* <[0;0;1] {{E}}> [0;1;0;1] > r --> l <* d0 <* <[0;0;1] {{E}}> r. Proof. es. Qed.
		52	Lemma D0R' l r : l <* <[0;0;1] {{E}}> [0;1] > [0;1;0;1] > r -->* l <* d0 <* <[0;0;1] {{E}}> [0;1] *> r.
		53	Proof. es. Qed.
		54	Lemma OVL r : 0inf <{{A}} [0;0;1] > [0;1;0;1] > r -->* 0inf <* d1 <* <[0;0;1] {{E}}> [0;1] *> r.
		55	Proof. es. Qed.
		56	Lemma OVR l r : l <* <[0;0;1] {{E}}> [0;1] > bAr > r -->* l <* d0 <{{A}} [0;0;1] > [1;0;1] > r.
		57	Proof. es. Qed.
		58	Lemma FL l r : l <* bA <* <[1;1;1] <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;0;1] > bBr *> r.
		59	Proof. es. Qed.
		60	Lemma FR1 l r : l <* <[0;0;1] {{E}}> [0;0;1] > bBr > r -->* l <* bA <{{A}} [0;0;1] > [0;0;1] > r.
		61	Proof. es. Qed.
		62	Lemma FR2 l r : l <* <[0;0;1] {{E}}> [0;0;1] > bAr > r -->* l <* bA <{{A}} [0;0;1] > [1;0;1] > r.
		63	Proof. es. Qed.
		64	Lemma FR3 l r : l <* <[0;0;1] {{E}}> [1;0;1] > bAr > r -->* l <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.
		65	Proof. es. Qed.
		66	Lemma FR4 l r : l <* <[0;0;1] {{E}}> [1;0;1] > bBr > r -->* l <{{A}} [0;0;1] > [0;0;1] > bAr *> r.
		67	Proof. es. Qed.
		68	Lemma FE0 l : l <* <[0;0;1] {{E}}> [0;0;1] > 0inf --> l <* bA <* <[0;0] {{C}}> 0inf.
		69	Proof. es. Qed.
		70	Lemma FE1 l : l <* <[0;0;1] {{E}}> [1;0;1] > 0inf --> l <{{A}} [0;0;1] > [0;0;1] > [0;0;1] *> 0inf.
		71	Proof. es. Qed.
		72	Lemma FE2 l : l <* <[0;0;1] {{E}}> [0;0;1] > [0;0;1] > 0inf -->* l <* bA <{{A}} [0;0;1] > [1] > 0inf.
		73	Proof. es. Qed.
		74	Lemma FE3 l : l <* <[0;0;1] {{E}}> [1] > 0inf --> l <{{A}} [0;0;1] > [0;0;1;1] > 0inf.
		75	Proof. es. Qed.
		76	Lemma FE4 l : l <* <[0;0;1] {{E}}> [0;0;1;1] > 0inf --> l <* bA <{{A}} [0;0;1] > [0;0;1] > 0inf.
		77	Proof. es. Qed.
		79	(** * Repeated rules (proof.md 3.2) *)
		81	Lemma ALs a : forall l r, l <* bA^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bAr^^a > r.
634	Proof.	82	Proof.
635	rewrite lpow_add,Str_app_assoc.
		83	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow AL; follow IH; rewrite lpow_shift'; finish].
636	eapply segRLs_sideRLs_concat.
637	1: eapply BC.Mul2.
⋯ 4 template-only lines (template 638–641), not in ours
642	all: ss.
643	esx.
644	Qed.	84	Qed.
646	Lemma Incs n m:
		85	Lemma BLs a : forall l r, l <* bB^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bBr^^a > r.
647	segRLs tm (hRL^^(n+m)) (hRL^^m) (w0^^n) (w1^^n).
648	Proof.	86	Proof.
649	eapply UC1.Incs.
		87	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow BL; follow IH; rewrite lpow_shift'; finish].
650	all: ss.
651	Qed.	88	Qed.
653	Definition RC0 n := w0'^^n *> 0inf.
		89	Lemma ARs a : forall l r, l <* <[0;0;1] {{E}}> bAr^^a > r --> l <* bA^^a <* <[0;0;1] {{E}}> r.
655	Lemma Incs0 n:
656	sideRLs tm (hRL^^n) (RC0 0) (RC0 n).
657	Proof.	90	Proof.
658	unfold RC0.
		91	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow AR; follow IH; rewrite <-lpow_shift'; finish].
659	sideRLs_ind n.
660	Qed.	92	Qed.
662	Lemma Incs' n m:
		93	Lemma BRs a : forall l r, l <* <[0;0;1] {{E}}> bBr^^a > r --> l <* bB^^a <* <[0;0;1] {{E}}> r.
663	segRLs tm (hRL^^(n+m)) (hRL^^m) (w1'^^n) (w0'^^n).
664	Proof.	94	Proof.
665	eapply UC1.Incs.
		95	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow BR; follow IH; rewrite <-lpow_shift'; finish].
666	all: ss.
667	Qed.	96	Qed.
669	Fixpoint RCa ls :=
		97	Lemma D1Ls a : forall l r, l <* d1^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;1;0;1]^^a > r.
670	match ls with
		98	Proof.
671	\| [] => 0inf
		99	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow D1L; follow IH; rewrite lpow_shift'; finish].
672	\| (a,b)::t => w1'^^a > w0^^b > RCa t
		100	Qed.
		101	Lemma D0R's a : forall l r, l <* <[0;0;1] {{E}}> [0;1] > [0;1;0;1]^^a > r -->* l <* d0^^a <* <[0;0;1] {{E}}> [0;1] *> r.
		102	Proof.
		103	induction a as [\|a IH]; intros; [finish \| rewrite !lpow_S, !Str_app_assoc; follow D0R'; follow IH; rewrite <-lpow_shift'; finish].
		104	Qed.
		106	(** * The binary counter: k digits, MSB first (proof.md: C_k(n)) *)
		108	Fixpoint ctr (k n : nat) : side :=
		109	match k with
		110	\| O => 0inf
		111	\| S k => ctr k (Nat.div2 n) <* (if Nat.odd n then d1 else d0)
673	end.	112	end.
675	Fixpoint RCb ls n :=
		114	Lemma ctr_even k q : ctr (S k) (2q) = ctr k q < d0.
676	match ls with
		115	Proof. cbn [ctr]. rewrite Nat.div2_double, Nat.odd_even. reflexivity. Qed.
677	\| [] => RC0 n
		117	Lemma ctr_odd k q : ctr (S k) (S (2q)) = ctr k q < d1.
678	\| (a,b)::t => w0'^^a > w1^^b > RCb t n
		118	Proof. cbn [ctr]. rewrite Nat.div2_succ_double, Nat.odd_succ, Nat.even_even. reflexivity. Qed.
679	end.
		120	Lemma pow2_pos k : 1 <= 2^k.
681	Fixpoint cons(l:nat)(x:list (nat*nat))(r:nat) :=
		121	Proof. pose proof (Nat.pow_nonzero 2 k). lia. Qed.
682	match x with
		123	(** CTR: one increment, n+1 <= 2^k - 1 *)
683	\| [] => [(l,r)]
		124	Lemma CTR k : forall n r, S n < 2^k ->
684	\| (a,b)::t => (l,a)::cons b t r
		125	ctr k n <{{A}} [0;0;1] > r --> ctr k (S n) <* <[0;0;1] {{E}}> r.
685	end.
687	Lemma RCb_shift ls n:
688	RCb ls n = [0;0] *> RCa (cons 0 ls n).
689	Proof.	126	Proof.
690	gen n.
		127	induction k as [\|k IH]; intros n r H.
691	induction ls; intros.
		128	- cbn in H. lia.
692	- cbn; unfold RC0.
		129	- rewrite Nat.pow_succ_r' in H.
693	simpl_rotate; reflexivity.
		130	destruct (Nat.Even_or_Odd n) as [[q Hq]\|[q Hq]]; subst n.
694	- destruct a as [a b].
		131	+ rewrite ctr_even, ctr_odd.
695	cbn.
		132	fw FLIP. finish.
696	rewrite IHls.
		133	+ replace (S (2q+1)) with (2 S q) by lia.
697	destruct ls as [\|[a0 b0] ls];
		134	replace (2q+1) with (S (2q)) by lia.
698	simpl_rotate; reflexivity.
		135	rewrite ctr_even, ctr_odd.
		136	fw D1L. fw (IH q). fw D0R. finish.
699	Qed.	137	Qed.
701	Fixpoint Rn (ls:list (nat*nat)) :=
		139	Lemma ctr_ones k : ctr k (2^k - 1) = 0inf <* d1^^k.
702	match ls with
703	\| [] => O
⋯ 2 template-only lines (template 704–705), not in ours
707	Lemma Rn_cons l ls r:
708	Rn (cons l ls r) = l + Rn ls + r.
709	Proof.	140	Proof.
710	gen l.
		141	induction k as [\|k IH].
711	induction ls; intros; cbn.
		142	- reflexivity.
712	- lia.
		143	- pose proof (pow2_pos k).
713	- destruct a as [a b]; cbn.
		144	replace (2^(S k) - 1) with (S (2 * (2^k - 1))) by (rewrite Nat.pow_succ_r'; lia).
714	rewrite IHls.
		145	rewrite ctr_odd, IH. reflexivity.
715	lia.
716	Qed.	146	Qed.
719	Lemma RIncs ls n:
		148	Lemma ctr_pow k : ctr (S k) (2^k) = 0inf <* d1 <* d0^^k.
720	sideRLs tm (hRL^^(Rn ls+n)) (RCa ls) (RCb ls n).
721	Proof.	149	Proof.
722	induction ls.
		150	induction k as [\|k IH].
723	- cbn.
		151	- reflexivity.
724	apply Incs0.
		152	- rewrite Nat.pow_succ_r', ctr_even, IH. reflexivity.
725	- destruct a as [a b].
726	cbn.
⋯ 3 template-only lines (template 727–729), not in ours
730	1: applys_eq (Incs b (Rn ls+n)); flia.
731	apply IHls.
732	Qed.	153	Qed.
734	Definition S '(k,ls) :=
		155	Lemma ctr_ov k : ctr (S (S k)) (2^(S k) + 1) = 0inf <* d1 <* d0^^k <* d1.
735	dh <* d0^^k <* d1 {{{ (hR,R) }}} RCa ls.
737	Lemma Rst k ls n:
738	dh <* d1^^k {{{ (hL,L) }}} RCb ls n -->*
739	S (k,cons 0 ls n).
740	Proof.	156	Proof.
741	rewrite RCb_shift.
		157	replace (2^(S k) + 1) with (S (2 * 2^k)) by (rewrite Nat.pow_succ_r'; lia).
742	es.
		158	rewrite ctr_odd, ctr_pow. reflexivity.
743	Qed.	159	Qed.
745	Lemma BigStep k ls:
		161	(** OV: the counter overflows; it gains a digit and a new front 111 appears *)
746	Rn ls <= (2^k-1)*2 ->
		162	Lemma OV k r :
747	S (k,ls) -->+
		163	ctr (S k) (2^(S k) - 1) <{{A}} [0;0;1] > bAr > bAr > r -->
748	S (1+k,cons 0 ls ((2^k-1)*2+1-Rn ls)).
		164	ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.
749	Proof.	165	Proof.
750	intros Hn.
		166	rewrite ctr_ones, ctr_ov.
751	remember ((2^k-1)*2-Rn ls+1) as n.
		167	fw D1Ls. rewrite lpow_S, Str_app_assoc.
752	unfold S.
		168	fw OVL. fw D0R's. fw OVR. fw FLIP. fw FR3. finish.
753	epose proof (sideRLs_concat (LIncs _)) as I1.
		169	Qed.
754	eapply progress_evstep_trans.
		171	(** RT: a round trip of the head through the counter (no overflow) *)
755	- apply I1.
		172	Lemma RT K n a r : S n < 2^K ->
756	rewrite lrcons_lpow1'.
		173	ctr K n <* bA^^a <{{A}} [0;0;1] > r --> ctr K (S n) <* bA^^a <* <[0;0;1] {{E}}> r.
757	replace ((2^k-1)*2) with (Rn ls+(n-1)) by lia.
		174	Proof.
758	rewrite <-Nat.add_assoc.
		175	intros H. fw ALs. fw CTR. fw ARs. finish.
759	apply RIncs.
		176	Qed.
760	- follow Rst.
		178	(** OVRT: a round trip that overflows the counter *)
761	unfold S.
		179	Lemma OVRT k a r :
		180	ctr (S k) (2^(S k) - 1) <* bA^^(S (S a)) <{{A}} [0;0;1] > r -->
		181	ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* bA^^a <* <[0;0;1] {{E}}> r.
		182	Proof.
		183	fw ALs. rewrite !lpow_S, !Str_app_assoc. fw OV. fw ARs. finish.
		184	Qed.
		186	(** QC: one step of the front (3 round trips, the front moves 2 blocks right) *)
		187	Lemma QC K n x y r : 3 + n < 2^K ->
		188	ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^(S (S y)) <{{A}} [0;0;1] > r -->
		189	ctr K (3 + n) <* bA^^(S (S (S x))) <* <[1;1;1] <* bA^^y <* <[0;0;1] {{E}}> r.
		190	Proof.
		191	intros H.
		192	fw ALs.
		193	fw (FL (ctr K n <* bA^^x) (bAr^^(S (S y)) *> r)).
		194	fw (RT K n x).
		195	fw FR1.
		196	fw (RT K (S n) (S x)).
		197	fw (FR2 (ctr K (S (S n)) <* bA^^(S x)) (bAr^^(S y) *> r)).
		198	fw (RT K (S (S n)) (S (S x))).
		199	fw (FR3 (ctr K (S (S (S n))) <* bA^^(S (S x))) (bAr^^y *> r)).
		200	fw ARs.
762	finish.	201	finish.
763	Qed.	202	Qed.
		204	(** * Configurations at the right edge (proof.md 1) *)
		206	Definition Pc K n X z := ctr K n <* bA^^X <* bB^^z <* <[0;0] {{C}}> 0inf.
		207	Definition Qc K n x y z := ctr K n <* bA^^x <* <[1;1;1] <* bA^^y <* bB^^z <* <[0;0] {{C}}> 0inf.
		209	Lemma R1 K n X z : S n < 2^K -> Pc K n X z -->+ Pc K (S n) X (S z).
		210	Proof.
		211	intros H. unfold Pc.
		212	fp ENDL. fw BLs. fw RT. fw BRs. fw ENDR. finish.
		213	Qed.
		215	Lemma R1s K c : forall n X z, c + n < 2^K -> Pc K n X z -->* Pc K (c + n) X (c + z).
		216	Proof.
		217	induction c as [\|c IH]; intros n X z H.
		218	- finish.
		219	- eapply evstep_trans. { apply progress_evstep, R1. lia. }
		220	eapply ev_eq. { apply IH. lia. }
		221	f_equal; lia.
		222	Qed.
		224	Lemma R2 k X z : Pc (S k) (2^(S k) - 1) (S (S X)) z -->+ Qc (S (S k)) (2^(S k) + 1) 1 X (S z).
		225	Proof.
		226	unfold Pc, Qc.
		227	fp ENDL. fw BLs. fw OVRT. fw BRs. fw ENDR. finish.
		228	Qed.
		230	(** Pfin: the rest of a P phase (R1 repeatedly, then R2) *)
		231	Lemma Pfin (k n X z n' x' X' z' : nat) :
		232	n < 2^(S k) -> X = 2 + X' -> n' = 2^(S k) + 1 -> x' = 1%nat -> z' = z + 2^(S k) - n ->
		233	Pc (S k) n X z -->+ Qc (S (S k)) n' x' X' z'.
		234	Proof.
		235	intros H1 H2 H3 H4 H5. subst.
		236	eapply evstep_progress_trans. { apply (R1s (S k) (2^(S k) - 1 - n) n). lia. }
		237	replace (2^(S k) - 1 - n + n) with (2^(S k) - 1) by lia.
		238	eapply prog_eq. { apply R2. }
		239	f_equal; lia.
		240	Qed.
		242	Lemma R3 K n x y z : 3 + n < 2^K ->
		243	Qc K n (S x) (S (S y)) z -->+ Qc K (3 + n) (S (S (S x))) y (S z).
		244	Proof.
		245	intros H. unfold Qc.
		246	fp ENDL. fw BLs. fw QC. fw BRs. fw ENDR. finish.
		247	Qed.
		249	(** * The conversion gadget (proof.md 3.3)
		251	After FL, the old front plus the B blocks form a word G right of the head. Each round
		252	the head goes through the counter and back (+1) and then hits G: a hit either reflects
		253	the head, with 0 or 1 new A block (Hit0 / Hit1), or ends at the right edge (FE0).
		254	Gad G T D: G takes T rounds in all, which add D A blocks. *)
		256	Definition Hit0 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <{{A}} [0;0;1] *> G'.
		257	Definition Hit1 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <* bA <{{A}} [0;0;1] *> G'.
		259	Inductive Gad : side -> nat -> nat -> Prop :=
		260	\| Gad_end : Gad ([0;0;1] *> 0inf) 1%nat 1%nat
		261	\| Gad_h0 G G' T D : Hit0 G G' -> Gad G' T D -> Gad G (S T) D
		262	\| Gad_h1 G G' T D : Hit1 G G' -> Gad G' T D -> Gad G (S T) (S D).
		264	Lemma Gad_DT G T D : Gad G T D -> D <= T.
		265	Proof. induction 1; lia. Qed.
		267	Lemma Gad_eq {G T D T' D'} : T = T' -> D = D' -> Gad G T D -> Gad G T' D'.
		268	Proof. intros E1 E2 H. subst. exact H. Qed.
		270	(** even (y = 0): FR1^(z+1), FE0 *)
		271	Lemma gad_even z : Gad ([0;0;1] > bBr^^z > 0inf) (S z) (S z).
		272	Proof.
		273	induction z as [\|z IH].
		274	- apply Gad_end.
		275	- eapply Gad_h1; [intro l; apply (FR1 l (bBr^^z *> 0inf)) \| exact IH].
		276	Qed.
		278	(** odd (y = 1): FR1, FR2, (FR4, FR2)^z, FE1, FE2, FE3, FE4, FE0 *)
		279	Lemma gad_tail : Gad ([1;0;1] *> 0inf) 5 3.
		280	Proof.
		281	eapply Gad_h0; [intro l; apply FE1 \|].
		282	eapply Gad_h1; [intro l; apply FE2 \|].
		283	eapply Gad_h0; [intro l; apply FE3 \|].
		284	eapply Gad_h1; [intro l; apply FE4 \|].
		285	apply Gad_end.
		286	Qed.
		288	Lemma gad_mid z : Gad ([1;0;1] > bBr^^z > 0inf) (5 + 2*z) (3 + z).
		289	Proof.
		290	induction z as [\|z IH].
		291	- exact gad_tail.
		292	- apply (Gad_eq (T := S (S (5 + 2*z))) (D := S (3 + z))); [lia \| lia \|].
		293	eapply Gad_h0; [intro l; apply (FR4 l (bBr^^z *> 0inf)) \|].
		294	eapply Gad_h1; [intro l; apply FR2 \|].
		295	exact IH.
		296	Qed.
		298	Lemma gad_odd z : Gad ([0;0;1] > bBr > bAr > bBr^^z > 0inf) (7 + 2*z) (5 + z).
		299	Proof.
		300	apply (Gad_eq (T := S (S (5 + 2*z))) (D := S (S (3 + z)))); [lia \| lia \|].
		301	eapply Gad_h1; [intro l; apply FR1 \|].
		302	eapply Gad_h1; [intro l; apply FR2 \|].
		303	apply gad_mid.
		304	Qed.
		306	(** All T rounds without overflow (R4, R5) *)
		307	Lemma ConvNo K : forall G T D, Gad G T D -> forall n a, n + T < 2^K ->
		308	ctr K n <* bA^^a <{{A}} [0;0;1] > G --> Pc K (n + T) (a + D) 0.
		309	Proof.
		310	induction 1 as [\|G G' T D HH HG IH\|G G' T D HH HG IH]; intros n a Hn.
		311	- fw (RT K n a). fw FE0. unfold Pc.
		312	replace (n + 1) with (S n) by lia. replace (a + 1) with (S a) by lia. finish.
		313	- fw (RT K n a). fw HH. eapply ev_eq. { apply (IH (S n) a). lia. } f_equal; lia.
		314	- fw (RT K n a). fw HH. eapply ev_eq. { apply (IH (S n) (S a)). lia. } f_equal; lia.
		315	Qed.
		317	(** Rounds after an overflow: a new front (QC) runs while the old gadget converts *)
		318	Lemma PostOV K : forall G T D, Gad G T D -> forall n x b y,
		319	b + D = 2T + y -> 1 <= y -> 3T + n < 2^K ->
		320	ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^b <{{A}} [0;0;1] > G -->
		321	Qc K (3T + n) (2T + S x) y 0.
		322	Proof.
		323	induction 1 as [\|G G' T D HH HG IH\|G G' T D HH HG IH]; intros n x b y Hb Hy Hn.
		324	- destruct y as [\|y]; [lia\|].
		325	assert (b = S (S y)) by lia. subst b.
		326	fw (QC K n x y). fw FE0. unfold Qc. finish.
		327	- pose proof (Gad_DT _ _ _ HG).
		328	destruct b as [\|[\|b]]; [lia\|lia\|].
		329	fw (QC K n x b). fw HH.
		330	eapply ev_eq. { apply (IH (3 + n) (S (S x)) b y); lia. }
		331	f_equal; lia.
		332	- pose proof (Gad_DT _ _ _ HG).
		333	destruct b as [\|[\|b]]; [lia\|lia\|].
		334	fw (QC K n x b). fw HH.
		335	eapply ev_eq. { apply (IH (3 + n) (S (S x)) (S b) y); lia. }
		336	f_equal; lia.
		337	Qed.
		339	(** A conversion during which the counter overflows (R5o) *)
		340	Lemma ConvOV k : forall G T D, Gad G T D -> forall n a m y,
		341	n + T = 2^(S k) + m -> n < 2^(S k) -> a + D = 2 + 2*m + y -> 1 <= y ->
		342	3*m + (2^(S k) + 1) < 2^(S (S k)) ->
		343	ctr (S k) n <* bA^^a <{{A}} [0;0;1] > G -->
		344	Qc (S (S k)) (3m + (2^(S k) + 1)) (1 + 2m) y 0.
		345	Proof.
		346	pose proof (pow2_pos (S k)) as Hp.
		347	induction 1 as [\|G G' T D HH HG IH\|G G' T D HH HG IH]; intros n a m y E1 E2 E3 E4 E5.
		348	- assert (m = 0%nat) by lia. subst m.
		349	assert (n = 2^(S k) - 1) by lia. subst n.
		350	destruct y as [\|y]; [lia\|].
		351	assert (a = S (S y)) by lia. subst a.
		352	fw (OVRT k y). fw FE0. unfold Qc. finish.
		353	- pose proof (Gad_DT _ _ _ HG).
		354	destruct (Nat.eq_dec n (2^(S k) - 1)) as [En\|En].
		355	+ subst n. assert (m = T) by lia. subst m.
		356	destruct a as [\|[\|a]]; [lia\|lia\|].
		357	fw (OVRT k a). fw HH.
		358	eapply ev_eq. { apply (PostOV (S (S k)) _ _ _ HG (2^(S k) + 1) O a y); lia. }
		359	f_equal; lia.
		360	+ fw (RT (S k) n a). fw HH.
		361	apply (IH (S n) a m y); lia.
		362	- pose proof (Gad_DT _ _ _ HG).
		363	destruct (Nat.eq_dec n (2^(S k) - 1)) as [En\|En].
		364	+ subst n. assert (m = T) by lia. subst m.
		365	destruct a as [\|[\|a]]; [lia\|lia\|].
		366	fw (OVRT k a). fw HH.
		367	eapply ev_eq. { apply (PostOV (S (S k)) _ _ _ HG (2^(S k) + 1) O (S a) y); lia. }
		368	f_equal; lia.
		369	+ fw (RT (S k) n a). fw HH.
		370	apply (IH (S n) (S a) m y); lia.
		371	Qed.
		373	(** From a Q configuration with y in {0,1}: the front meets the B blocks *)
		374	Lemma QG0 K n x z : Qc K n (S x) 0 z -->+
		375	ctr K n <* bA^^x <{{A}} [0;0;1] > [0;0;1] > bBr^^(S z) *> 0inf.
		376	Proof.
		377	unfold Qc. fp ENDL. fw BLs. fw (FL (ctr K n <* bA^^x) (bBr^^z *> 0inf)). finish.
		378	Qed.
		380	Lemma QG1 K n x z : Qc K n (S x) 1 z -->+
		381	ctr K n <* bA^^x <{{A}} [0;0;1] > [0;0;1] > bBr > bAr > bBr^^z *> 0inf.
		382	Proof.
		383	unfold Qc. fp ENDL. fw BLs.
		384	fw (AL (ctr K n <* bA^^(S x) <* <[1;1;1]) (bBr^^z *> 0inf)).
		385	fw (FL (ctr K n <* bA^^x) (bAr > bBr^^z > 0inf)). finish.
		386	Qed.
		388	(** R4 *)
		389	Lemma Conv0 K n x z : n + z + 2 < 2^K ->
		390	Qc K n (S x) 0 z -->+ Pc K (n + z + 2) (x + z + 2) 0.
		391	Proof.
		392	intros H. eapply progress_evstep_trans. { apply QG0. }
		393	eapply ev_eq. { apply (ConvNo K _ _ _ (gad_even (S z))). lia. }
		394	f_equal; lia.
		395	Qed.
		397	(** R5 *)
		398	Lemma Conv1 K n x z : n + 2*z + 7 < 2^K ->
		399	Qc K n (S x) 1 z -->+ Pc K (n + 2*z + 7) (x + z + 5) 0.
		400	Proof.
		401	intros H. eapply progress_evstep_trans. { apply QG1. }
		402	eapply ev_eq. { apply (ConvNo K _ _ _ (gad_odd z)). lia. }
		403	f_equal; lia.
		404	Qed.
		406	(** R5o *)
		407	Lemma Conv1o (k m n x z n' x' y : nat) :
		408	n + 2z + 7 = 2^(S k) + m -> n < 2^(S k) -> x + z + 5 = 2 + 2m + y -> 1 <= y ->
		409	3m + (2^(S k) + 1) < 2^(S (S k)) -> n' = 3m + (2^(S k) + 1) -> x' = 1 + 2*m ->
		410	Qc (S k) n (S x) 1 z -->+ Qc (S (S k)) n' x' y 0.
		411	Proof.
		412	intros. subst n' x'.
		413	eapply progress_evstep_trans. { apply QG1. }
		414	apply (ConvOV k _ _ _ (gad_odd z)); lia.
		415	Qed.
		417	(** * The cycle (proof.md 4)
		419	Index (k,i,y,z) stands for Q(k+2, 2^(k+1)+1+3i, 1+2i, y, z): the Q phase of the cycle
		420	whose counter has k+2 digits, after i front steps. In proof.md's cycle coordinates
		421	N = 2^(k+1), Y = y+2i, Z = z-i. Inv is the hexagon of proof.md 4 in these coordinates
		422	(Z = z-i may be negative), plus N >= 64. *)
		424	Definition CfgF (k i y z : nat) := Qc (S (S k)) (3i + (2^(S k) + 1)) (1 + 2i) y z.
		426	Definition Inv (k i y z : nat) : Prop :=
		427	64 <= 2^(S k) /\ 2^(S k) <= 8(y + 2i) /\ 8(y + 2i) <= 3 * 2^(S k) /\
		428	3z <= 2^(S k) + 3i /\ 8i <= 8z + 2^(S k) /\
		429	2^(S k) <= 4y + 6i + 2z /\ 20y + 24i + 16z <= 9 * 2^(S k).
		431	Lemma cycle_step k i y z : Inv k i y z ->
		432	exists k' i' y' z', CfgF k i y z -->+ CfgF k' i' y' z' /\ Inv k' i' y' z'.
		433	Proof.
		434	unfold Inv, CfgF. intros HI.
		435	pose proof (Nat.pow_succ_r' 2 (S k)) as HN.
		436	pose proof (Nat.pow_succ_r' 2 (S (S k))) as HN2.
		437	destruct y as [\|[\|y]].
		438	- (* y = 0: R4, R1^, R2 )
		439	exists (S k), O, (2i + z), (2^(S k) - 3 - 3i - z). split; [\|lia].
		440	eapply progress_evstep_trans. { apply Conv0. lia. }
		441	apply progress_evstep. apply Pfin; lia.
		442	- destruct (Nat.lt_ge_cases (3i + (2^(S k) + 1) + 2z + 7) (2^(S (S k)))) as [Hno\|Hov].
		443	+ (* y = 1, no overflow: R5, R1^, R2 )
		444	exists (S k), O, (2i + z + 3), (2^(S (S k)) - (3i + (2^(S k) + 1) + 2*z + 7)).
		445	split; [\|lia].
		446	eapply progress_evstep_trans. { apply Conv1. lia. }
		447	apply progress_evstep. apply Pfin; lia.
		448	+ (* y = 1, overflow during the conversion: R5o *)
		449	remember (3i + (2^(S k) + 1) + 2z + 7 - 2^(S (S k))) as m eqn:Em.
		450	exists (S k), m, (2i + z + 3 - 2m), O. split; [\|lia].
		451	apply (Conv1o (S k) m); lia.
		452	- (* y >= 2: R3 *)
		453	exists k, (S i), y, (S z). split; [\|lia].
		454	eapply prog_eq. { apply R3. lia. }
		455	f_equal; lia.
		456	Qed.
		458	(** * Start: c0 reaches Q(7,65,1,16,0) = CfgF 5 0 16 0 in 17,215 steps *)
		460	Lemma init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^16 <* <[0;0] {{C}}> 0inf.
		461	Proof. esx. Qed.
		463	Lemma init : c0 -->* CfgF 5 0 16 0.
		464	Proof. apply init0. Qed.
765	Lemma nonhalt: ~halts tm c0.	466	Lemma nonhalt: ~halts tm c0.
766	Proof.	467	Proof.
767	eapply multistep_nonhalt with (c':=S(2,[(0,3)])%nat).
		468	eapply multistep_nonhalt. { apply init. }
768	1: unfold S; esx.
		469	apply (progress_nonhalt_cond tm _ (5,0,16,0)%nat
769	eapply progress_nonhalt_cond with (P:=fun '(k,ls) => Rn ls<=(2^k-1)*2).
		470	(fun '(k,i,y,z) => CfgF k i y z) (fun '(k,i,y,z) => Inv k i y z)).
770	2: cbn; lia.
		471	- intros [[[k i] y] z] HI.
771	intros [k ls] HP.
		472	destruct (cycle_step k i y z HI) as (k' & i' & y' & z' & H1 & H2).
772	eexists (_,_); split.
		473	exists (k',i',y',z'). split; assumption.
773	1: apply BigStep; lia.
		474	- unfold Inv. cbn. lia.
774	rewrite Rn_cons.
775	rewrite Nat.pow_add_r by lia.
776	lia.
777	Qed.	475	Qed.
		477	(*
		478	```
		479	1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---
		481	C_k(n): n in k bits MSB first, digit 1 -> 1010 (d1), digit 0 -> 0010 (d0) [ctr k n]
		482	A = 00111, B = 10111 left of the head; A' = 00101, B' = 00001 right of the head
		483	moving head: <A 001 / 001 E> (TM4's hL / hR)
		485	P(k,n,X,z) := 0^inf C_k(n) A^X B^z 00 C> 0^inf [Pc]
		486	Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 C> 0^inf [Qc]
		488	R1 P(k,n,X,z) -->+ P(k,n+1,X,z+1) n+1 < 2^k
		489	R2 P(k,2^k-1,X+2,z) -->+ Q(k+1,2^k+1,1,X,z+1)
		490	R3 Q(k,n,x+1,y+2,z) -->+ Q(k,n+3,x+3,y,z+1) n+3 < 2^k
		491	R4 Q(k,n,x+1,0,z) -->+ P(k,n+z+2,x+z+2,0) n+z+2 < 2^k
		492	R5 Q(k,n,x+1,1,z) -->+ P(k,n+2z+7,x+z+5,0) n+2z+7 < 2^k
		493	R5o Q(k,n,x+1,1,z) -->+ Q(k+1,2^k+1+3m,1+2m,y,0) n+2z+7 = 2^k+m, n < 2^k,
		494	x+z+5 = 2+2m+y, y >= 1, 3m+2^k+1 < 2^(k+1)
		496	cycle index (k,i,y,z) = Q(k+2, 2^(k+1)+1+3i, 1+2i, y, z); N = 2^(k+1), Y = y+2i, Z = z-i
		497	y >= 2: R3 -> (k, i+1, y-2, z+1)
		498	y = 0: R4, R1 repeated, R2 -> (k+1, 0, 2i+z, N-3-3i-z)
		499	y = 1: R5, R1 repeated, R2 -> (k+1, 0, 2i+z+3, N-8-3i-2z) no overflow
		500	R5o, m = 3i+2z+8-N -> (k+1, m, 2i+z+3-2m, 0) overflow
		501	invariant: N >= 64, 8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
		502	start: c0 -->(17215) Q(7,65,1,16,0), index (5,0,16,0)
		503	```
		504	*)

3Proof outlineCheck: the new items (green) carry the argument; the names read like the proof.md rules.

73 items in 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v (504 lines): 64 Lemma, 7 Definition, 1 Fixpoint, 1 Inductive. 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.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---").	L18	identicalexcept the TM string
2	Lemma	`ev_eq`	Lemma ev_eq {c1 c2 c2'} : c1 -->* c2 -> c2 = c2' -> c1 -->* c2'.	L35	new
3	Lemma	`prog_eq`	Lemma prog_eq {c1 c2 c2'} : c1 -->+ c2 -> c2 = c2' -> c1 -->+ c2'.	L38	new
4	Lemma	`ENDL`	Lemma ENDL l : l <* <[0;0] {{C}}> 0inf -->+ l <{{A}} [0;0;1] *> 0inf.	L43	new
5	Lemma	`AL`	Lemma AL l r : l <* bA <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bAr > r.	L44	new
6	Lemma	`BL`	Lemma BL l r : l <* bB <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bBr > r.	L45	new
7	Lemma	`AR`	Lemma AR l r : l <* <[0;0;1] {{E}}> bAr > r --> l <* bA <* <[0;0;1] {{E}}> r.	L46	new
8	Lemma	`BR`	Lemma BR l r : l <* <[0;0;1] {{E}}> bBr > r --> l <* bB <* <[0;0;1] {{E}}> r.	L47	new
9	Lemma	`ENDR`	Lemma ENDR l : l <* <[0;0;1] {{E}}> 0inf -->* l <* bB <* <[0;0] {{C}}> 0inf.	L48	new
10	Lemma	`D1L`	Lemma D1L l r : l <* d1 <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;1;0;1] > r.	L49	new
11	Lemma	`FLIP`	Lemma FLIP l r : l <* d0 <{{A}} [0;0;1] > r --> l <* d1 <* <[0;0;1] {{E}}> r.	L50	new
12	Lemma	`D0R`	Lemma D0R l r : l <* <[0;0;1] {{E}}> [0;1;0;1] > r --> l <* d0 <* <[0;0;1] {{E}}> r.	L51	new
13	Lemma	`D0R'`	Lemma D0R' l r : l <* <[0;0;1] {{E}}> [0;1] > [0;1;0;1] > r -->* l <* d0 <* <[0;0;1] {{E}}> [0;1] *> r.	L52	new
14	Lemma	`OVL`	Lemma OVL r : 0inf <{{A}} [0;0;1] > [0;1;0;1] > r -->* 0inf <* d1 <* <[0;0;1] {{E}}> [0;1] *> r.	L54	new
15	Lemma	`OVR`	Lemma OVR l r : l <* <[0;0;1] {{E}}> [0;1] > bAr > r -->* l <* d0 <{{A}} [0;0;1] > [1;0;1] > r.	L56	new
16	Lemma	`FL`	Lemma FL l r : l <* bA <* <[1;1;1] <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;0;1] > bBr *> r.	L58	new
17	Lemma	`FR1`	Lemma FR1 l r : l <* <[0;0;1] {{E}}> [0;0;1] > bBr > r -->* l <* bA <{{A}} [0;0;1] > [0;0;1] > r.	L60	new
18	Lemma	`FR2`	Lemma FR2 l r : l <* <[0;0;1] {{E}}> [0;0;1] > bAr > r -->* l <* bA <{{A}} [0;0;1] > [1;0;1] > r.	L62	new
19	Lemma	`FR3`	Lemma FR3 l r : l <* <[0;0;1] {{E}}> [1;0;1] > bAr > r -->* l <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.	L64	new
20	Lemma	`FR4`	Lemma FR4 l r : l <* <[0;0;1] {{E}}> [1;0;1] > bBr > r -->* l <{{A}} [0;0;1] > [0;0;1] > bAr *> r.	L66	new
21	Lemma	`FE0`	Lemma FE0 l : l <* <[0;0;1] {{E}}> [0;0;1] > 0inf --> l <* bA <* <[0;0] {{C}}> 0inf.	L68	new
22	Lemma	`FE1`	Lemma FE1 l : l <* <[0;0;1] {{E}}> [1;0;1] > 0inf --> l <{{A}} [0;0;1] > [0;0;1] > [0;0;1] *> 0inf.	L70	new
23	Lemma	`FE2`	Lemma FE2 l : l <* <[0;0;1] {{E}}> [0;0;1] > [0;0;1] > 0inf -->* l <* bA <{{A}} [0;0;1] > [1] > 0inf.	L72	new
24	Lemma	`FE3`	Lemma FE3 l : l <* <[0;0;1] {{E}}> [1] > 0inf --> l <{{A}} [0;0;1] > [0;0;1;1] > 0inf.	L74	new
25	Lemma	`FE4`	Lemma FE4 l : l <* <[0;0;1] {{E}}> [0;0;1;1] > 0inf --> l <* bA <{{A}} [0;0;1] > [0;0;1] > 0inf.	L76	new
26	Lemma	`ALs`	Lemma ALs a : forall l r, l <* bA^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bAr^^a > r.	L81	new
27	Lemma	`BLs`	Lemma BLs a : forall l r, l <* bB^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > bBr^^a > r.	L85	new
28	Lemma	`ARs`	Lemma ARs a : forall l r, l <* <[0;0;1] {{E}}> bAr^^a > r --> l <* bA^^a <* <[0;0;1] {{E}}> r.	L89	new
29	Lemma	`BRs`	Lemma BRs a : forall l r, l <* <[0;0;1] {{E}}> bBr^^a > r --> l <* bB^^a <* <[0;0;1] {{E}}> r.	L93	new
30	Lemma	`D1Ls`	Lemma D1Ls a : forall l r, l <* d1^^a <{{A}} [0;0;1] > r --> l <{{A}} [0;0;1] > [0;1;0;1]^^a > r.	L97	new
31	Lemma	`D0R's`	Lemma D0R's a : forall l r, l <* <[0;0;1] {{E}}> [0;1] > [0;1;0;1]^^a > r -->* l <* d0^^a <* <[0;0;1] {{E}}> [0;1] *> r.	L101	new
32	Fixpoint	`ctr`	Fixpoint ctr (k n : nat) : side := match k with \| O => 0inf \| S k => ctr k (Nat.div2 n) <* (if Nat.odd n then d1 else d0) end.	L108	new
33	Lemma	`ctr_even`	Lemma ctr_even k q : ctr (S k) (2q) = ctr k q < d0.	L114	new
34	Lemma	`ctr_odd`	Lemma ctr_odd k q : ctr (S k) (S (2q)) = ctr k q < d1.	L117	new
35	Lemma	`pow2_pos`	Lemma pow2_pos k : 1 <= 2^k.	L120	new
36	Lemma	`CTR`	Lemma CTR k : forall n r, S n < 2^k -> ctr k n <{{A}} [0;0;1] > r --> ctr k (S n) <* <[0;0;1] {{E}}> r.	L124	new
37	Lemma	`ctr_ones`	Lemma ctr_ones k : ctr k (2^k - 1) = 0inf <* d1^^k.	L139	new
38	Lemma	`ctr_pow`	Lemma ctr_pow k : ctr (S k) (2^k) = 0inf <* d1 <* d0^^k.	L148	new
39	Lemma	`ctr_ov`	Lemma ctr_ov k : ctr (S (S k)) (2^(S k) + 1) = 0inf <* d1 <* d0^^k <* d1.	L155	new
40	Lemma	`OV`	Lemma OV k r : ctr (S k) (2^(S k) - 1) <{{A}} [0;0;1] > bAr > bAr > r --> ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* <[0;0;1] {{E}}> r.	L162	new
41	Lemma	`RT`	Lemma RT K n a r : S n < 2^K -> ctr K n <* bA^^a <{{A}} [0;0;1] > r --> ctr K (S n) <* bA^^a <* <[0;0;1] {{E}}> r.	L172	new
42	Lemma	`OVRT`	Lemma OVRT k a r : ctr (S k) (2^(S k) - 1) <* bA^^(S (S a)) <{{A}} [0;0;1] > r --> ctr (S (S k)) (2^(S k) + 1) <* bA <* <[1;1;1] <* bA^^a <* <[0;0;1] {{E}}> r.	L179	new
43	Lemma	`QC`	Lemma QC K n x y r : 3 + n < 2^K -> ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^(S (S y)) <{{A}} [0;0;1] > r --> ctr K (3 + n) <* bA^^(S (S (S x))) <* <[1;1;1] <* bA^^y <* <[0;0;1] {{E}}> r.	L187	new
44	Definition	`Pc`	Definition Pc K n X z := ctr K n <* bA^^X <* bB^^z <* <[0;0] {{C}}> 0inf.	L206	new
45	Definition	`Qc`	Definition Qc K n x y z := ctr K n <* bA^^x <* <[1;1;1] <* bA^^y <* bB^^z <* <[0;0] {{C}}> 0inf.	L207	new
46	Lemma	`R1`	Lemma R1 K n X z : S n < 2^K -> Pc K n X z -->+ Pc K (S n) X (S z).	L209	new
47	Lemma	`R1s`	Lemma R1s K c : forall n X z, c + n < 2^K -> Pc K n X z -->* Pc K (c + n) X (c + z).	L215	new
48	Lemma	`R2`	Lemma R2 k X z : Pc (S k) (2^(S k) - 1) (S (S X)) z -->+ Qc (S (S k)) (2^(S k) + 1) 1 X (S z).	L224	new
49	Lemma	`Pfin`	Lemma Pfin (k n X z n' x' X' z' : nat) : n < 2^(S k) -> X = 2 + X' -> n' = 2^(S k) + 1 -> x' = 1%nat -> z' = z + 2^(S k) - n -> Pc (S k) n X z -->+ Qc (S (S k)) n' x' X' z'.	L231	new
50	Lemma	`R3`	Lemma R3 K n x y z : 3 + n < 2^K -> Qc K n (S x) (S (S y)) z -->+ Qc K (3 + n) (S (S (S x))) y (S z).	L242	new
51	Definition	`Hit0`	Definition Hit0 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <{{A}} [0;0;1] *> G'.	L256	new
52	Definition	`Hit1`	Definition Hit1 (G G' : side) := forall l, l <* <[0;0;1] {{E}}> G -->* l <* bA <{{A}} [0;0;1] *> G'.	L257	new
53	Inductive	`Gad`	Inductive Gad : side -> nat -> nat -> Prop := \| Gad_end : Gad ([0;0;1] *> 0inf) 1%nat 1%nat \| Gad_h0 G G' T D : Hit0 G G' -> Gad G' T D -> Gad G (S T) D \| Gad_h1 G G' T D : Hit1 G G' -> Gad G' T D -> Gad G (S T) (S D).	L259	new
54	Lemma	`Gad_DT`	Lemma Gad_DT G T D : Gad G T D -> D <= T.	L264	new
55	Lemma	`Gad_eq`	Lemma Gad_eq {G T D T' D'} : T = T' -> D = D' -> Gad G T D -> Gad G T' D'.	L267	new
56	Lemma	`gad_even`	Lemma gad_even z : Gad ([0;0;1] > bBr^^z > 0inf) (S z) (S z).	L271	new
57	Lemma	`gad_tail`	Lemma gad_tail : Gad ([1;0;1] *> 0inf) 5 3.	L279	new
58	Lemma	`gad_mid`	Lemma gad_mid z : Gad ([1;0;1] > bBr^^z > 0inf) (5 + 2*z) (3 + z).	L288	new
59	Lemma	`gad_odd`	Lemma gad_odd z : Gad ([0;0;1] > bBr > bAr > bBr^^z > 0inf) (7 + 2*z) (5 + z).	L298	new
60	Lemma	`ConvNo`	Lemma ConvNo K : forall G T D, Gad G T D -> forall n a, n + T < 2^K -> ctr K n <* bA^^a <{{A}} [0;0;1] > G --> Pc K (n + T) (a + D) 0.	L307	new
61	Lemma	`PostOV`	Lemma PostOV K : forall G T D, Gad G T D -> forall n x b y, b + D = 2T + y -> 1 <= y -> 3T + n < 2^K -> ctr K n <* bA^^(S x) <* <[1;1;1] <* bA^^b <{{A}} [0;0;1] > G --> Qc K (3T + n) (2T + S x) y 0.	L318	new
62	Lemma	`ConvOV`	Lemma ConvOV k : forall G T D, Gad G T D -> forall n a m y, n + T = 2^(S k) + m -> n < 2^(S k) -> a + D = 2 + 2m + y -> 1 <= y -> 3m + (2^(S k) + 1) < 2^(S (S k)) -> ctr (S k) n <* bA^^a <{{A}} [0;0;1] > G --> Qc (S (S k)) (3m + (2^(S k) + 1)) (1 + 2m) y 0.	L340	new
63	Lemma	`QG0`	Lemma QG0 K n x z : Qc K n (S x) 0 z -->+ ctr K n <* bA^^x <{{A}} [0;0;1] > [0;0;1] > bBr^^(S z) *> 0inf.	L374	new
64	Lemma	`QG1`	Lemma QG1 K n x z : Qc K n (S x) 1 z -->+ ctr K n <* bA^^x <{{A}} [0;0;1] > [0;0;1] > bBr > bAr > bBr^^z *> 0inf.	L380	new
65	Lemma	`Conv0`	Lemma Conv0 K n x z : n + z + 2 < 2^K -> Qc K n (S x) 0 z -->+ Pc K (n + z + 2) (x + z + 2) 0.	L389	new
66	Lemma	`Conv1`	Lemma Conv1 K n x z : n + 2z + 7 < 2^K -> Qc K n (S x) 1 z -->+ Pc K (n + 2z + 7) (x + z + 5) 0.	L398	new
67	Lemma	`Conv1o`	Lemma Conv1o (k m n x z n' x' y : nat) : n + 2z + 7 = 2^(S k) + m -> n < 2^(S k) -> x + z + 5 = 2 + 2m + y -> 1 <= y -> 3m + (2^(S k) + 1) < 2^(S (S k)) -> n' = 3m + (2^(S k) + 1) -> x' = 1 + 2*m -> Qc (S k) n (S x) 1 z -->+ Qc (S (S k)) n' x' y 0.	L407	new
68	Definition	`CfgF`	Definition CfgF (k i y z : nat) := Qc (S (S k)) (3i + (2^(S k) + 1)) (1 + 2i) y z.	L424	new
69	Definition	`Inv`	Definition Inv (k i y z : nat) : Prop := 64 <= 2^(S k) /\ 2^(S k) <= 8(y + 2i) /\ 8(y + 2i) <= 3 * 2^(S k) /\ 3z <= 2^(S k) + 3i /\ 8i <= 8z + 2^(S k) /\ 2^(S k) <= 4y + 6i + 2z /\ 20y + 24i + 16z <= 9 * 2^(S k).	L426	new
70	Lemma	`cycle_step`	Lemma cycle_step k i y z : Inv k i y z -> exists k' i' y' z', CfgF k i y z -->+ CfgF k' i' y' z' /\ Inv k' i' y' z'.	L431	new
71	Lemma	`init0`	Lemma init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^16 <* <[0;0] {{C}}> 0inf.	L460	new
72	Lemma	`init`	Lemma init : c0 -->* CfgF 5 0 16 0.	L463	new
73	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L466	adapted

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 · informal proof (submitted copy)
submission/README.md · the package README
submission/discord.md · Discord draft (not posted)
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 37: 2. Rule table (busycoq comment-block style)

1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

C_k(n): n in k bits MSB first, 1 -> 1010, 0 -> 0010;   A = 00111, B = 10111
P(k,n,X,z)   := 0^inf C_k(n) A^X B^z 00 C> 0^inf
Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 C> 0^inf                    (x >= 1)

R1  P(k,n,X,z)      --> P(k,n+1,X,z+1)                     n+1 <= 2^k-1
R2  P(k,2^k-1,X,z)  --> Q(k+1,2^k+1,1,X-2,z+1)             X >= 2
R3  Q(k,n,x,y+2,z)  --> Q(k,n+3,x+2,y,z+1)                 n+3 <= 2^k-1
R4  Q(k,n,x,0,z)    --> P(k,n+z+2,x+z+1,0)                 n+z+2  <= 2^k-1
R5  Q(k,n,x,1,z)    --> P(k,n+2z+7,x+z+4,0)                n+2z+7 <= 2^k-1
R5o Q(k,n,x,1,z)    --> Q(k+1,2^k+1+3m,1+2m,x+z+2-2m,0)    m := n+2z+7-2^k >= 0,  x+z+2-2m >= 1,  3m <= 2^k-2

remark (true, never used): R4o Q(k,n,x,0,z) --> Q(k+1,2^k+1+3m,1+2m,x+z-1-2m,0),
                           m := n+z+2-2^k >= 0, x+z-1-2m >= 1, 3m <= 2^k-2

steps: R1 32X+32z+16t(n)+47,  R2 32X+32z+16k+61,  R3 96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197
       (t(n) = number of trailing 1 bits of n)

cycle (N = 2^k):  S(k,Y,Z) := Q(k+1, N+1+3m, 1+2m, Y-2m, Z+m),  m = max(0,-Z)
  (S(k,.) is the first right-edge visit after the counter grows to k+1 digits; its counter
   lies in [N,2N) and overflows at 2N)
  S(k,2j,Z)   -->+ S(k+1, 3j+Z,   N-3-4j-Z)      via R3^(j-m), R4, R1^(N-4-2Y-Z), R2
  S(k,2j+1,Z) -->+ S(k+1, 3j+3+Z, N-8-5j-2Z)     via R3^(j-m), then R5, R1^*, R2  or  R5o
invariant (N >= 64):  8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
start: c0 -->(17215) S(6,16,0) = Q(7,65,1,16,0)

Every case is covered. For P: n < 2^k-1 uses R1, and n = 2^k-1 uses R2 (X ≥ 2 holds; see §4). For Q: y ≥ 2 uses R3. y = 0 uses R4: on the invariant the counter never overflows during an even conversion (§4), so R4o is never needed. y = 1 uses R5 if the counter does not overflow during the conversion, and R5o if it does. The domain conditions that the run must satisfy (no overflow inside a Q phase, R2's X ≥ 2, no overflow in an even conversion, and the R5o conditions) are exactly what the invariant in §4 guarantees. The conditions matter: on each of 677 small out-of-domain instances, the overflow chain of §3.3 does not apply, and the out-of-domain configuration Q(4,8,400,0,180) halts (after 327,891 steps). This shows the conditions matter, not that they are necessary; the domain of R5o is a sufficient condition chosen for the cycle lemma.

5FamilyCheck: related machines are killed together or have a reason to be left open.

2 machines, 2 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.

who	machine	status	relation to this kill
#4 kill 2	`1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---`	✓Killed: never halts	this kill
#4b kill 11	`1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA`	✓Killed: never halts	parent link; = #4's table, run from state F; named in #4b's .v header; named in #4b's proof.md; named in #4b's notes.md · review · same machine as this kill? (same table, started in #4's F; different orbit; tables, pictures and numbers side by side) · 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 681 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 2.04 s
✓
.v hash matches the checked hash
.v = checked sha256 51e3dea1f666…; submission/ copy = checked sha256 51e3dea1f666…
✓
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 L92: - Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
- notes.md L116: - No Checkpoint B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
- proof.md L277: ## Review log (Checkpoint B skeptic, 2026-10-10)
○
Family posted together?
1 other kill(s) in the family: #4b; the Discord draft names 0 of them

Generated by tools/killreview.py at 2026-10-16 13:29 PDT in 0.1 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 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---

Files

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

name	size	changed
notes.md ↓	10 KB	2026-10-10 05:16
proof.md ↓	29 KB	2026-10-10 04:32
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	575 B	2026-10-16 10:28
observe.json ↓	12 KB	2026-10-10 04:41
1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v ↓	20 KB	2026-10-10 11:50
img/	9 items	2026-10-10 00:32
rocq/	3 items	2026-10-10 05:10
submission/	6 items	2026-10-15 15:49
work/	19 items	2026-10-10 15:58
check_proof.py ↓	31 KB	2026-10-10 04:29

status.json in full

{
 "tm": "1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "pr": "https://github.com/ccz181078/busycoq/pull/24",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RCHHH.v",
 "pr_opened": "2026-10-15T22:46:17Z",
 "pr_comments": 0,
 "pr_head_sha": "1b57cbac0ccf590232647c1b29389f2efe7f26a4",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:07:18Z",
 "pr_merged_by": "ccz181078"
}

Rendered 2026-10-16 13:29 by tools/machinepage.py from status.json, observe.json (the card), the kill files (tools/killreview.py) and the dashboard records · rebuild: python3 -B tools/card.py 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (the kill review: python3 -B tools/killreview.py 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, which also renders a derived kill's same-machine pictures)