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 / #12b

`1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB`

#12blocal proof 6Claimed by someone elseCounter Class 4bbchallenge ↗Explorer parent: #12

How we proved it never halts

#12's proof with a smaller budget and zero slack

#12 works like a recursive call stack written in runs of 1s. Each round starts at the left end with a bottom call that can pay for three calls, the machine halts only if a round needs a fourth, and an exact law shows that every round costs exactly 2. #12b, once its states are renamed, is #12's table with one transition changed, started in the state that is #12's B instead of A; no renaming or mirror makes it exactly #12.

The changed transition is used only at the start of a round, when the bottom call is created at the left end. There it takes a 6-step detour to the same tape that #12 reaches in 2 steps. So the call-stack picture, the replay of rounds one level down and the cost law all carry over unchanged.

What is new is the budget. After a 48-step opening, every round starts with the left end reading 11 00 instead of 111 00, so the bottom call is three 1s long and can pay for only two calls. A single round needing three would halt the machine. But #12's law counts the calls exactly, not just as a bound: every round needs exactly 2, the budget is always just enough, and the missing transition never fires.

The Rocq proof is #12's file with the start-of-round move re-proved by running it, detour included, plus the new 48-step opening and one added lemma for a round that starts with the smaller bottom call.

#6local proof number

896lines of Rocq

4 sto compile

6/6automatic checks

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

Rename the twin's states A..F to B,C,D,E,F,A. The result is #12 with one transition changed (A0 = 1RA instead of 1RB; in twin names F0 = 1RF), started in #12's state B. It is not #12 up to renaming or mirroring (all 1,440 relabelings checked). F0 is read only at the first step of the left-edge push R3, where it takes a 6-step detour (F0 F0 F1 B1 A1 A0) to the configuration #12 reaches in 2 steps. The tape effect is the same; it costs 4 more steps. (submission/README.md, Mechanism)

Upstream: The blank-start machine never halts: CounterClass4.v.TM1 ↗. 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-14T06:19:56Z. First public push time is not established.
Rocq proof: check_kill PASS · first Oct 10 09:52
896 lines · 40 KB .v · compile 4.2 s · coqchk pass · 0 axioms · PASS Oct 10 09:52 (re-run Oct 10 11:54)
· the .v file
Automatic review: 6 of 6 checks passtemplate: #12's kill file (kill 5) (twin: parent kill's .v) · details in Proof →
Class: Counter Class 4
On the list: not on BB6_holdouts_663.txt (line 640 of the previous list) · historical 740 line 640
eqv ×2sim 1e13
Derived from: 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF#12 Claimed by someone else

Mechanism

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

Figures

Fig 1 · Blaze view, 10 million stepsQ1
Blaze view, time runs down. Find each row where the left edge steps out, and compare the gaps between them.

Fig 2 · Zoom: one long epoch (k = 8)Q2
One long epoch (k = 8), time runs down. Find each step where the long left block (run 1) shrinks.

Fig 3 · Edge records to 1 billion stepsQ3
Edge records to 1e9 (only 134 rows). Look at the two thin white lines in the black right half.

More figures (1)Fig 4: bbchallenge Default view, first 10,000 steps

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

rule	from ⟶ to	cases	steps	checked
R1 pointer right	1ⁿ⁺² <A 0 1^m+1 0² 1^x 0 ⟶ 1ⁿ⁺¹ 0 1^m+1 <A 0 1^x+1 0²	n,m,x>=0; x=0 covers 0^3 and 0^inf after the 00	3m+2x+15	✓60/60
R2 lone 1 merges, jump back	1^j+1 0 1^k+1 0 1 <A 0 ⟶ 1^j+1 <A 0 1^k+2 0²	j,k>=0	k+10	✓60/60
R2e jump to edge	0^∞ 1^k+1 0 1 <A 0 ⟶ 0^∞ <A 0 1^k+2 0²	k>=0	k+10	✓60/60
R3 edge refill	0^∞ <A 0 1^k+1 0² 1^m 0 ⟶ 0^∞ 1^k+2 <A 0 1^m+1 0²	k,m>=0	3k+2m+11	✓60/60
HALT	0³ 1 <A 0 ⟶ halt	only halting route; needs a lone 1 at the far left	4 (incl. halting transition)	✓40/40
short epoch	Fs(k,P) = 0^∞ <A 0 1³ 0² 1² 0² 1^2k 0² 1^2k+1 0^P 1 0^Q 1 0^∞, P+Q=2k ⟶ Fl(k,P) = 0^∞ <A 0 1³ 0² 1^2k+1 0² 1^2k+3 0² 1 0^P 1 0^Q 1 0^∞	P,Q even >=2 (k up to 200 tested)	40k+288	✓24/24
long epoch	Fl(k,P) ⟶ Fs(k+1,P') with P' even, 2<=P'<=2k; or D(k+1)	P' irregular in (k,P), e.g. k=11: P 2,4,6,8,10,12 -> 6,8,10,16,D,4. Macro model: every even P for k<=13 closes with no halt	~1260*2^k (+-200, depends on P)	✓22/22
degenerate D	D(k) = 0^∞ <A 0 1³ 0² 1² 0² 1^2k+2 0² 1^2k+1 0^∞ ⟶ E(k) = 0^∞ <A 0 1³ 0² 1^2k+3 0² 1^2k+3 0² 1 0^∞	k>=3	40k+312	✓8/8
E back to family	E(k) ⟶ Fs(k+1,2)	k=3..10; the real orbit takes D at k=25 (step 4.2e10), then E, then Fs(26,2)	~1260*2^k	✓8/8

Compressed historythe tape as 0^∞ <A 0 1³ 0² 1² 0² 1^2k 0² 1^2k+1 0^P 1 0^Q 1 0^∞ at 26 moments: where the rules are read off

0^∞ <A 0 1³ 0² 1² 0² 1^2k 0² 1^2k+1 0^P 1 0^Q 1 0^∞

step	`k`	`P`	`Q`
1,590	1	D	D
4,090	2	2	2
8,806	3	D	D
18,826	4	2	6
38,730	5	6	4
78,838	6	4	8
159,230	7	4	10
320,186	8	10	6
642,526	9	4	14
1,287,310	10	8	12
2,577,198	11	12	10
5,157,430	12	4	20
10,317,966	13	12	14
20,639,446	14	20	8
41,282,870	15	24	6
82,570,218	16	18	14
165,145,050	17	30	4
330,295,486	18	16	20
660,596,506	19	14	24
1,321,198,810	20	26	14
2,642,404,258	21	10	32
5,284,815,110	22	28	16
10,569,637,546	23	38	8
21,139,283,246	24	24	24
42,278,575,038	25	D	D
84,557,158,858	26	2	50

klast 26

Plast 2

Qlast 50

Template comparisonCounterClass2v1.v: does not apply · the nearest solved proof, what carries over, and the transitions that differ

	0	1
A	1RB	1LC
B	1RC	1LB
C	1LD	0RB
D	0LE	1RD
E	---	0LF
F	0LA	1LF

file: CounterClass2v1.v
module: —
machine: 1RB1RD_1LC---_1LE0LD_0RE1LC_1RA1RF_1RE0LF (11 transitions apart)
diff: 10/12 transitions differ (best renaming+mirror); CounterClass3v2 8/12, closest CounterClass1 machine 8/12
note: No rules or shapes carry over: 7 of 16 CC2v1 starting shapes (SkelE/Be) halt on this machine. What does carry over is the proof skeleton: an Inductive Side type, a Good invariant and progress_nonhalt_cond.

Proof & checks

6/6 automatic checks pass

Kill 6 · Counter Class 4 · the kill file 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v: 896 lines, 106 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (twin: parent kill's .v): #12's kill file (kill 5) · 95% of our lines identical · vs #12: table differs in 1 transition(s); trajectory twin

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

1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L847

check_kill

✓ PASS · 17/17 checks pass · compile 4.18 s · coqchk pass (1.3 s) · assumptions: 0 (closed) · 2026-10-10 18:54:14 UTC · submission/check_kill.txt

Checked .v

sha256 81348b14976e863f…

✓	1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v	`81348b14976e863f…` = checked
✓	submission/1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v	`81348b14976e863f…` = 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`	41142 bytes, 896 lines, 980 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`	5 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 26: TM_from_str "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB" == <tm> (41 bytes)
✓	`theorem_text`	line 847: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 ([local working file]
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 4.2s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB") 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 (1.3s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Same machine as #12?Check: every row of the table is ✓ under the computed renaming (or the listed differences are what status.json's relation says), the two pictures show the same bands, and the trajectory numbers agree with the claimed relation (a twin keeps a fixed small offset; a sibling's gap grows).

status.json names #12 as the parent (1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF); label: “#12b”; relation: “neighbour of #12: one transition away from #12's table (after renaming); its run is nearly identical (134 vs 133 cells at 1e9), so a look-alike, not a sibling”. Everything below is computed from the two machine strings, not read from notes.

✗ Not the same table. No renaming of #12's states, with or without mirroring, gives this machine's table. Closest: A→F, B→A, C→B, D→C, E→D, F→E (#12's state → this machine's), no mirror, where 1 of 12 transitions differ:

#12's A0 = 1RB predicts this machine's F0 = 1RA; it is 1RF.

Under that map: This machine starts in #12's state B (#12 itself starts in A).

#12	#12's row (read 0, read 1)	σ	predicted row: renamed by σ	this machine's actual row
A	`1RB` `1LC`	→ F	`1RA` `1LB`	`1RF` `1LB`	✗	start of #12
B	`1RC` `1LB`	→ A	`1RB` `1LA`	`1RB` `1LA`	✓	start of this machine
C	`1LD` `0RB`	→ B	`1LC` `0RA`	`1LC` `0RA`	✓
D	`0LE` `1RD`	→ C	`0LD` `1RC`	`0LD` `1RC`	✓
E	`---` `0LF`	→ D	`---` `0LE`	`---` `0LE`	✓
F	`0LA` `1LF`	→ E	`0LF` `1LE`	`0LF` `1LE`	✓

Rows aligned by σ: each of #12's states X sits next to this machine's state σ(X). ✓ = the actual row equals #12's row with every target state renamed by σ; --- (halt) must stay ---. Searched: all 720 renamings × with/without mirror.

default view of 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF — Fig P1 · **bbchallenge default view: #12 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: the tables differ in 1 transition(s) (listed above); it starts in #12's state B, not A, so the first steps differ; the numbers below read: trajectory twin, so after the start the bands should match line for line.

default view of 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB — Fig P1 · **bbchallenge default view: #12 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: the tables differ in 1 transition(s) (listed above); it starts in #12's state B, not A, so the first steps differ; the numbers below read: trajectory twin, so after the start the bands should match line for line.

blaze view of 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF — Fig P2 · **Long run, Blaze (speed): #12 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

blaze view of 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB — Fig P2 · **Long run, Blaze (speed): #12 and this machine, 100 million steps**
The macro behaviour, identical settings on both sides: each picture is its machine's own visited span stretched to 800 px, so compare the shape and order of the bands, not their absolute width. Speed mode samples one cell per column, so a one-cell shift can swap orange and white inside a band; compare band edges, not colours.

Trajectory numbers, from blank (C core)

✓ trajectory twin: within 2.2% at 1e9 (cells -1, nonzeros -2); the offset stays within 2 at every checkpoint instead of growing

steps	cells visited (hi − lo + 1)			nonzeros
steps	#12	this	ratio (Δ)	#12	this	ratio (Δ)
1e5	56	55	0.9821 (-1)	35	35	1.0000 (+0)
1e6	74	73	0.9865 (-1)	48	46	0.9583 (-2)
1e7	92	91	0.9891 (-1)	61	59	0.9672 (-2)
1e8	116	115	0.9914 (-1)	76	75	0.9868 (-1)
1e9	134	133	0.9925 (-1)	89	87	0.9775 (-2)

Each machine from blank in its own start state, sim.py C core. Trajectory twin = cells and nonzeros stay within 16 of the parent's at every checkpoint (a fixed offset from a different start, not a growing gap). Cached in img/vs-parent.json (2026-10-16 10:29 PDT); --force recomputes.

3Where 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).

twin: parent kill's .v #12's kill file (kill 5) machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v · detected from status.json

95%of our lines identical to the template

18changed lines

19added lines (ours only)

4template lines dropped

98 / 7 / 1items identical / adapted / new

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

This extends kill #12's .v (876 lines; in #12's own package). The changes:

the tm string;
the head state <{{A}} becomes <{{F}} (9 places: tR1, tR3, tR2, tR3c and conf);
the new Ep_tm2;
init's target, and nonhalt's C and top step;
the comments.

The proof text differs in 4 lines plus the one new lemma, and the file compiled on the first try. It is a direct proof on the holdout string and does not use TM113.eqv. The file is 896 lines and imports only Individual62 from busycoq.

Fig P3 · 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 766 lines

95% identical · 18 changed · 19 added

template 751 lines

97% kept verbatim · 4 not in ours

our items 106

98 identical · 7 adapted · 1 new · 0 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 15–876 (leading comment left out). Ours: lines 19–896 (header comment 1–18 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.

Side-by-side diff: template (751 lines) vs ours (766 lines), 41 lines differ; runs of identical lines and long template-only runs folded

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

template		ours
16	From BusyCoq Require Import Individual62.	20	From BusyCoq Require Import Individual62.
17	Require Import Lia.	21	Require Import Lia.
⋯ 6 identical lines (template 18–25, ours 22–29)
26	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	30	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
28	Open Scope list.	32	Open Scope list.
30	(* R1: l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r *)	34	(* R1: l 1^(n+2) <F 0 1^(m+1) 0 0 1^x 0 r --> l 1^(n+1) 0 1^(m+1) <F 0 1^(x+1) 0 0 r *)
31	Lemma tR1 n m x l r :	35	Lemma tR1 n m x l r :
32	l <* [1]^^(S (S n)) <{{A}} [0] > [1]^^(S m) > [0;0] > [1]^^x > [0] *> r -->+	36	l <* [1]^^(S (S n)) <{{F}} [0] > [1]^^(S m) > [0;0] > [1]^^x > [0] *> r -->+
33	l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{A}} [0] > [1]^^(S x) > [0;0] *> r.	37	l <* [1]^^(S n) <* [0] <* [1]^^(S m) <{{F}} [0] > [1]^^(S x) > [0;0] *> r.
34	Proof. es. Qed.	38	Proof. es. Qed.
36	(* R3: l 0 <A 0 1^(k+1) 0 0 1^m 0 r --> l 1^(k+2) <A 0 1^(m+1) 0 0 r *)	40	(* R3': l 0 <F 0 1^(k+1) 0 0 1^m 0 r --> l 1^(k+2) <F 0 1^(m+1) 0 0 r
		41	(detour F0 F0 F1 B1 A1 A0, then #12's R3 tail; 4 more steps than #12) *)
37	Lemma tR3 k m l r :	42	Lemma tR3 k m l r :
38	l <* [0] <{{A}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] *> r -->+	43	l <* [0] <{{F}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] *> r -->+
39	l <* [1]^^(S (S k)) <{{A}} [0] > [1]^^(S m) > [0;0] *> r.	44	l <* [1]^^(S (S k)) <{{F}} [0] > [1]^^(S m) > [0;0] *> r.
40	Proof. es. Qed.	45	Proof. es. Qed.
42	(* R2: l 0 1^(k+1) 0 1 <A 0 r --> l <A 0 1^(k+2) 0 0 r *)	47	(* R2: l 0 1^(k+1) 0 1 <F 0 r --> l <F 0 1^(k+2) 0 0 r *)
43	Lemma tR2 k l r :	48	Lemma tR2 k l r :
44	l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{A}} [0] *> r -->+	49	l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{F}} [0] *> r -->+
45	l <{{A}} [0] > [1]^^(S (S k)) > [0;0] *> r.	50	l <{{F}} [0] > [1]^^(S (S k)) > [0;0] *> r.
46	Proof. es. Qed.	51	Proof. es. Qed.
48	Lemma tR3c k m r :	53	Lemma tR3c k m r :
49	const 0 <{{A}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] *> r -->+	54	const 0 <{{F}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] *> r -->+
50	const 0 <* [1]^^(S (S k)) <{{A}} [0] > [1]^^(S m) > [0;0] *> r.	55	const 0 <* [1]^^(S (S k)) <{{F}} [0] > [1]^^(S m) > [0;0] *> r.
51	Proof. rewrite (const_unfold _ S0) at 1. es. Qed.	56	Proof. rewrite (const_unfold _ S0) at 1. es. Qed.
53	(* ---------- tape encoding of the run model ---------- *)	58	(* ---------- tape encoding of the run model ---------- *)
⋯ 14 identical lines (template 54–69, ours 59–74)
70	\| c :: g :: R' => [1]^^c > [0]^^g > rside R'	75	\| c :: g :: R' => [1]^^c > [0]^^g > rside R'
71	end.	76	end.
73	Definition conf (L R : list nat) : Q * tape := lside L <{{A}} [0] *> rside R.	78	Definition conf (L R : list nat) : Q * tape := lside L <{{F}} [0] *> rside R.
75	Lemma c0_1 : 0 >> const 0 = const 0.	80	Lemma c0_1 : 0 >> const 0 = const 0.
76	Proof. symmetry. apply const_unfold. Qed.	81	Proof. symmetry. apply const_unfold. Qed.
⋯ 119 identical lines (template 78–209, ours 83–214)
210	intros z Hz. destruct z as [\|z]; [lia\|].	215	intros z Hz. destruct z as [\|z]; [lia\|].
211	replace (S z - S c + 1) with (z - c + 1) by lia. eapply L_cpp; eauto; [lia \| apply Hm; lia].	216	replace (S z - S c + 1) with (z - c + 1) by lia. eapply L_cpp; eauto; [lia \| apply Hm; lia].
		217	Qed.
		219	(* the twin's edge frame has value 3 (budget 2): an epoch of cost 2 runs at z = 3
		220	(proof.md section 5, budget-2 edge lemma) *)
		221	Lemma Ep_tm2 W W' : Ep W 2 W' -> conf [] (2 :: 2 :: W) -->+ conf [] (2 :: 2 :: W').
		222	Proof.
		223	intros (R0 & Hu & HL).
		224	destruct (Life_shape _ _ _ HL 2 _ eq_refl) as (W'' & E & Hc & Hm).
		225	inversion E; subst.
		226	eapply progress_trans. { apply push0_ok; [exact Hu \| lia]. }
		227	exact (Life_tm _ _ _ (Hm 3 ltac:(lia)) []).
212	Qed.	228	Qed.
214	Definition bump (o : outcome) : outcome :=	230	Definition bump (o : outcome) : outcome :=
⋯ 533 identical lines (template 215–824, ours 231–840)
825	Qed.	841	Qed.
827	(* ---------- top level ---------- *)	843	(* ---------- top level ---------- *)
828	Lemma init : c0 -->* conf [] [3; 2; 1].	844	Lemma init : c0 -->* conf [] [2; 2; 1].
829	Proof. unfold conf, lside, rside. cbn [lpow app]. solve_init. Qed.	845	Proof. unfold conf, lside, rside. cbn [lpow app]. solve_init. Qed.
831	Lemma nonhalt: ~halts tm c0.	847	Lemma nonhalt: ~halts tm c0.
832	Proof.	848	Proof.
833	eapply multistep_nonhalt; [apply init \|].	849	eapply multistep_nonhalt; [apply init \|].
834	apply (progress_nonhalt_cond tm (nat * list nat) (0, [1]) (fun i => conf [] (3 :: 2 :: snd i))	850	apply (progress_nonhalt_cond tm (nat * list nat) (0, [1]) (fun i => conf [] (2 :: 2 :: snd i))
835	(fun i => Orb [] (fst i) (snd i) /\ (1 <= fst i -> Inv [] (fst i) (snd i)))).	851	(fun i => Orb [] (fst i) (snd i) /\ (1 <= fst i -> Inv [] (fst i) (snd i)))).
836	- intros [n W] [HO HI]. cbn [fst snd] in *.	852	- intros [n W] [HO HI]. cbn [fst snd] in *.
837	destruct (step_lemma n (main n) [] n W ltac:(cbn; lia) I HO HI) as (W' & HE & HI').	853	destruct (step_lemma n (main n) [] n W ltac:(cbn; lia) I HO HI) as (W' & HE & HI').
838	exists (S n, W'). cbn [fst snd]. split.	854	exists (S n, W'). cbn [fst snd]. split.
839	+ apply Ep_tm in HE. replace (cost [] n) with 2 in HE by reflexivity. exact HE.	855	+ replace (cost [] n) with 2 in HE by reflexivity. exact (Ep_tm2 _ _ HE).
840	+ split; [econstructor; eauto \| intros; exact HI'].	856	+ split; [econstructor; eauto \| intros; exact HI'].
841	- cbn [fst snd]. split; [exact (O0 []) \| lia].	857	- cbn [fst snd]. split; [exact (O0 []) \| lia].
⋯ 2 identical lines (template 842–845, ours 858–861)
846	```	862	```
847	1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF	863	1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB
849	conf L R := 0^inf 1^a_1 0 1^a_2 0 .. 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 .. 1^c_r 0^inf	865	conf L R := 0^inf 1^a_1 0 1^a_2 0 .. 0 1^a_p <F 0 1^c_1 0^g_1 1^c_2 .. 1^c_r 0^inf
850	(L = [a_p; ..; a_1] top first, R = [c_1; g_1; c_2; ..; c_r])	866	(L = [a_p; ..; a_1] top first, R = [c_1; g_1; c_2; ..; c_r])
851	tR1 l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r -->+ l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r	867	tR1 l 1^(n+2) <F 0 1^(m+1) 0 0 1^x 0 r -->+ l 1^(n+1) 0 1^(m+1) <F 0 1^(x+1) 0 0 r
852	tR3 l 0 <A 0 1^(k+1) 0 0 1^m 0 r -->+ l 1^(k+2) <A 0 1^(m+1) 0 0 r	868	tR3 l 0 <F 0 1^(k+1) 0 0 1^m 0 r -->+ l 1^(k+2) <F 0 1^(m+1) 0 0 r (3k+2m+15 steps:
853	tR2 l 0 1^(k+1) 0 1 <A 0 r -->+ l <A 0 1^(k+2) 0 0 r
		869	detour F0 F0 F1 B1 A1 A0, then #12's R3 tail)
		870	tR2 l 0 1^(k+1) 0 1 <F 0 r -->+ l <F 0 1^(k+2) 0 0 r
854	push conf (x::L) (h::R') -->+ conf (h::x-1::L) (updt R') x >= 2 (tR1)	871	push conf (x::L) (h::R') -->+ conf (h::x-1::L) (updt R') x >= 2 (tR1)
855	push0 conf [] (h::R') -->+ conf [h+1] (updt R') (tR3)	872	push0 conf [] (h::R') -->+ conf [h+1] (updt R') (tR3)
856	pop conf (1::y::L) R -->+ conf L (y+1::2::R) y >= 1 (tR2)	873	pop conf (1::y::L) R -->+ conf L (y+1::2::R) y >= 1 (tR2)
857	updt [] = [1], updt [2;c] = [c+1], updt (2::c::g::R) = c+1::g+1::R, updt (g::R) = 1::g-1::R (g >= 3)	874	updt [] = [1], updt [2;c] = [c+1], updt (2::c::g::R) = c+1::g+1::R, updt (g::R) = 1::g-1::R (g >= 3)
859	Edge W := conf [] (3::2::W); Ep W c W' : Edge W -->+ conf [] (5-c::2::W')
		876	Ep W c W' : conf [] (3::2::W) -->+ conf [] (5-c::2::W') (edge frame of value 4, as in #12)
		877	Ep_tm2 : Ep W 2 W' -> conf [] (2::2::W) -->+ conf [] (2::2::W')
		878	(edge frame of value 3: Life_shape at z = 3, push0 at h = 2, Life_tm at L = [])
860	U0 Ep [1] = (2, [2;2;1])	879	U0 Ep [1] = (2, [2;2;1])
861	U1 Ep (1::g::rest) = (2, 2::2::1::g-2::rest) g >= 4	880	U1 Ep (1::g::rest) = (2, 2::2::1::g-2::rest) g >= 4
⋯ 9 identical lines (template 862–870, ours 881–889)
871	Q = Qi ++ Qe, \|Qi\| = b+1-a+[k in P], every q in Qi <= a-2-[k in P],	890	Q = Qi ++ Qe, \|Qi\| = b+1-a+[k in P], every q in Qi <= a-2-[k in P],
872	Qe = the indices of P above k, each shifted by a-k-3	891	Qe = the indices of P above k, each shifted by a-k-3
873	start: c0 -->* Edge [1] = Edge (O_0([])) (50 steps)
		892	start: c0 -->* conf [] [2;2;1] = conf [] (2::2::O_0([])) (48 steps)
874	top: O_n([]) has no markers, so Edge (O_n([])) -->+ Edge (O_(n+1)([])) for every n
		893	top: O_n([]) has no markers, so every epoch costs exactly 2 and
		894	conf [] (2::2::O_n([])) -->+ conf [] (2::2::O_(n+1)([])) for every n
875	```	895	```
876	*)	896	*)

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

106 items in 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v (896 lines): 81 Lemma, 16 Definition, 5 Fixpoint, 3 Inductive, 1 Theorem. 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 "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB").	L26	identicalexcept the TM string
2	Lemma	`tR1`	Lemma tR1 n m x l r : l <* [1]^^(S (S n)) <{{F}} [0] > [1]^^(S m) > [0;0] > [1]^^x > [0] > r -->+ l < [1]^^(S n) <* [0] <* [1]^^(S m) <{{F}} [0] > [1]^^(S x) > [0;0] *> r.	L35	adapted
3	Lemma	`tR3`	Lemma tR3 k m l r : l <* [0] <{{F}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] > r -->+ l < [1]^^(S (S k)) <{{F}} [0] > [1]^^(S m) > [0;0] *> r.	L42	adapted
4	Lemma	`tR2`	Lemma tR2 k l r : l <* [0] <* [1]^^(S k) <* [0] <* [1] <{{F}} [0] > r -->+ l <{{F}} [0] > [1]^^(S (S k)) > [0;0] > r.	L48	adapted
5	Lemma	`tR3c`	Lemma tR3c k m r : const 0 <{{F}} [0] > [1]^^(S k) > [0;0] > [1]^^m > [0] > r -->+ const 0 < [1]^^(S (S k)) <{{F}} [0] > [1]^^(S m) > [0;0] *> r.	L53	adapted
6	Fixpoint	`lsep`	Fixpoint lsep (L : list nat) : side := match L with \| [] => const 0 \| y :: L' => lsep L' <* [1]^^y <* [0] end.	L59	identical
7	Definition	`lside`	Definition lside (L : list nat) : side := match L with \| [] => const 0 \| x :: L' => lsep L' <* [1]^^x end.	L65	identical
8	Fixpoint	`rside`	Fixpoint rside (R : list nat) : side := match R with \| [] => const 0 \| [c] => [1]^^c > const 0 \| c :: g :: R' => [1]^^c > [0]^^g *> rside R' end.	L71	identical
9	Definition	`conf`	Definition conf (L R : list nat) : Q * tape := lside L <{{F}} [0] *> rside R.	L78	adapted
10	Lemma	`c0_1`	Lemma c0_1 : 0 >> const 0 = const 0.	L80	identical
11	Lemma	`lsep_eq`	Lemma lsep_eq L : lsep L = lside L <* [0].	L83	identical
12	Definition	`updt`	Definition updt (R' : list nat) : option (list nat) := match R' with \| [] => Some [1] \| g :: R'' => match g with \| 0 \| 1 => None … +11 lines	L91	identical
13	Lemma	`updt_shape`	Lemma updt_shape m R' R1 : updt R' = Some R1 -> exists x r, rside (S m :: R') = [S1]^^(S m) > [S0;S0] > [S1]^^x > [S0] > r /\ rside R1 = [S1]^^(S x) > [S0;S0] > r.	L109	identical
14	Lemma	`push_ok`	Lemma push_ok y h R' R1 L : updt R' = Some R1 -> 1 <= y -> 1 <= h -> conf (S y :: L) (h :: R') -->+ conf (h :: y :: L) R1.	L123	identical
15	Lemma	`push0_ok`	Lemma push0_ok h R' R1 : updt R' = Some R1 -> 1 <= h -> conf [] (h :: R') -->+ conf [S h] R1.	L133	identical
16	Lemma	`pop_ok`	Lemma pop_ok y L R : 1 <= y -> conf (1 :: y :: L) R -->+ conf L (S y :: 2 :: R).	L143	identical
17	Inductive	`outcome`	Inductive outcome := Fin (R : list nat) \| Pop (c : nat) (R : list nat).	L153	identical
18	Inductive	`Life`	Inductive Life : nat -> list nat -> outcome -> Prop := \| L_fin R : Life 1 R (Fin R) \| L_cf y h R' R1 Rc : 1 <= y -> updt R' = Some R1 -> Life h R1 (Fin Rc) -> Life (S y) (h :: R') (Pop 1 (S y :: 2 :: Rc)) \| L_cpf y h R' R1 c' R2 Rf : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> Life y R2 (Fin Rf) -> Life (S y) (h :: R') (Fin Rf) … +2 lines	L159	identical
19	Lemma	`Life_pos`	Lemma Life_pos x R o : Life x R o -> 1 <= x.	L168	identical
20	Lemma	`Life_tm`	Lemma Life_tm x R o : Life x R o -> forall L, match o with \| Fin Rf => conf (x :: L) R -->* conf (1 :: L) Rf \| Pop _ Rf => conf (x :: L) R -->+ conf L Rf end.	L171	identical
21	Definition	`Ep`	Definition Ep (W : list nat) (c : nat) (W' : list nat) : Prop := exists R0, updt (2 :: W) = Some R0 /\ Life 4 R0 (Pop c ((5 - c) :: 2 :: W')).	L194	identical
22	Lemma	`Ep_tm`	Lemma Ep_tm W c W' : Ep W c W' -> conf [] (3 :: 2 :: W) -->+ conf [] ((5 - c) :: 2 :: W').	L197	identical
23	Lemma	`Life_shape`	Lemma Life_shape x R o : Life x R o -> forall c Rf, o = Pop c Rf -> exists W', Rf = (x - c + 1) :: 2 :: W' /\ c + 1 <= x /\ forall z, c + 1 <= z -> Life z R (Pop c ((z - c + 1) :: 2 :: W')).	L204	identical
24	Lemma	`Ep_tm2`	Lemma Ep_tm2 W W' : Ep W 2 W' -> conf [] (2 :: 2 :: W) -->+ conf [] (2 :: 2 :: W').	L221	new
25	Definition	`bump`	Definition bump (o : outcome) : outcome := match o with Fin W => Fin W \| Pop c W => Pop (S c) W end.	L230	identical
26	Lemma	`L_cp`	Lemma L_cp y h R' R1 c' R2 o : 1 <= y -> updt R' = Some R1 -> Life h R1 (Pop c' R2) -> Life y R2 o -> Life (S y) (h :: R') (bump o).	L233	identical
27	Lemma	`updt_cons2`	Lemma updt_cons2 W R0 : updt (2 :: W) = Some R0 -> exists c2 W1, W = c2 :: W1.	L237	identical
28	Lemma	`frame_step`	Lemma frame_step y z W c W' o y' z' : Ep W c W' -> 2 <= y -> c + 1 <= z -> y' = y - 1 -> z' = z - c + 1 -> Life y' (z' :: 2 :: W') o -> Life y (z :: 2 :: W) (bump o).	L241	identical
29	Definition	`tail_ok`	Definition tail_ok (N : list nat) : Prop := N = [] \/ exists g rest, N = S (S g) :: rest.	L264	identical
30	Lemma	`U0`	Lemma U0 : Ep [1] 2 [2;2;1].	L266	identical
31	Lemma	`U1`	Lemma U1 g rest : Ep (1 :: S (S (S (S g))) :: rest) 2 (2 :: 2 :: 1 :: S (S g) :: rest).	L269	identical
32	Lemma	`U2`	Lemma U2 b N : tail_ok N -> Ep (1 :: 2 :: S b :: N) 2 (S (S (S b)) :: 2 :: 1 :: N).	L272	identical
33	Lemma	`ruleS`	Lemma ruleS a b N : tail_ok N -> Ep (2 :: 2 :: S a :: 2 :: S b :: N) 2 (S (S a) :: 2 :: S (S (S b)) :: 2 :: 1 :: N).	L275	identical
34	Lemma	`TRF`	Lemma TRF a b N Rc : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Fin Rc) -> Ep (a :: 2 :: S b :: N) 2 Rc.	L279	identical
35	Lemma	`Xin0`	Lemma Xin0 a'' b'' : 1 <= a'' -> Life 2 [2; 2; a''; 2; b''] (Pop 1 [2; 2; S a''; 2; S b'']).	L283	identical
36	Lemma	`Xin1`	Lemma Xin1 a'' b'' g rest : 1 <= a'' -> Life 2 (2 :: 2 :: a'' :: 2 :: b'' :: S g :: rest) (Pop 1 (2 :: 2 :: S a'' :: 2 :: S b'' :: S (S g) :: rest)).	L287	identical
37	Lemma	`TRX0`	Lemma TRX0 a b N c a'' b'' : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c [2; 2; S a''; 2; S b'']) -> Ep (a :: 2 :: S b :: N) 3 [S (S a''); 2; S (S b'')].	L291	identical
38	Lemma	`TRX1`	Lemma TRX1 a b N c a'' b'' g rest : tail_ok N -> 2 <= a -> Life a (S (S (S b)) :: 2 :: 1 :: N) (Pop c (2 :: 2 :: S a'' :: 2 :: S b'' :: S g :: rest)) -> Ep (a :: 2 :: S b :: N) 3 (S (S a'') :: 2 :: S (S b'') :: S (S g) :: rest).	L296	identical
39	Fixpoint	`mwf`	Fixpoint mwf (s : nat) (P : list nat) : list nat := match P with \| [] => [] \| p :: P' => (p - s + 1) :: 1 :: mwf p P' end.	L304	identical
40	Definition	`mw`	Definition mw (P : list nat) : list nat := mwf 0 P.	L309	identical
41	Fixpoint	`valid_from`	Fixpoint valid_from (s : nat) (P : list nat) : Prop := match P with \| [] => True \| p :: P' => (exists t, p = s + 2 * t + 1) /\ valid_from p P' end.	L312	identical
42	Definition	`valid`	Definition valid (P : list nat) : Prop := valid_from 0 P.	L317	identical
43	Definition	`cnt`	Definition cnt (Q : list nat) (n : nat) : nat := length (filter (fun q => q <? n) Q).	L319	identical
44	Definition	`ind`	Definition ind (Q : list nat) (n : nat) : nat := cnt Q (S n) - cnt Q n.	L320	identical
45	Definition	`cost`	Definition cost (Q : list nat) (n : nat) : nat := 2 + ind Q n.	L321	identical
46	Inductive	`Orb`	Inductive Orb (Q : list nat) : nat -> list nat -> Prop := \| O0 : Orb Q 0 (1 :: mw Q) \| OS n W W' : Orb Q n W -> Ep W (cost Q n) W' -> Orb Q (S n) W'.	L323	identical
47	Fixpoint	`bumpn`	Fixpoint bumpn (k : nat) (o : outcome) : outcome := match k with 0 => o \| S k => bumpn k (bump o) end.	L327	identical
48	Lemma	`bumpn_fin`	Lemma bumpn_fin k W : bumpn k (Fin W) = Fin W.	L330	identical
49	Lemma	`bumpn_pop`	Lemma bumpn_pop k c W : bumpn k (Pop c W) = Pop (k + c) W.	L333	identical
50	Lemma	`cnt_0`	Lemma cnt_0 Q : cnt Q 0 = 0.	L336	identical
51	Lemma	`cnt_mono`	Lemma cnt_mono Q n : cnt Q n <= cnt Q (S n).	L339	identical
52	Lemma	`cnt_mono'`	Lemma cnt_mono' Q n m : n <= m -> cnt Q n <= cnt Q m.	L345	identical
53	Lemma	`replay`	Lemma replay Q k Wk : Orb Q k Wk -> forall y z o, k + 1 <= y -> (k = 0 \/ k + 2 + cnt Q k <= z) -> Life (y - k) ((z - k - cnt Q k) :: 2 :: Wk) o -> Life y (z :: 2 :: 1 :: mw Q) (bumpn k o).	L348	identical
54	Lemma	`mw_tail_ok`	Lemma mw_tail_ok Q : valid Q -> tail_ok (mw Q).	L358	identical
55	Lemma	`ruleT`	Lemma ruleT a b Q W' : Orb Q (a - 1) W' -> 2 <= a -> 1 <= b -> valid Q -> a - 1 + cnt Q (a - 1) <= b -> Ep (a :: 2 :: b :: mw Q) 2 ((b + 3 - a - cnt Q (a - 1)) :: 2 :: W').	L364	identical
56	Lemma	`mwf_shift`	Lemma mwf_shift s k P : mwf (s + k) (map (fun p => p + k) P) = mwf s P.	L377	identical
57	Lemma	`ruleX`	Lemma ruleX a b Q a'' Q'' : Orb Q (a - 2) (a'' :: 2 :: b :: mw Q'') -> 3 <= a -> 1 <= b -> 1 <= a'' -> valid Q -> valid Q'' -> b = a - 2 + cnt Q (a - 2) -> Ep (a :: 2 :: b :: mw Q) 3 (S (S a'') :: 2 :: S (S b) :: mw (map (fun q => q + 2) Q'')).	L383	identical
58	Lemma	`valid_gt`	Lemma valid_gt s P : valid_from s P -> Forall (fun p => s < p) P.	L406	identical
59	Lemma	`cnt_cons_lt`	Lemma cnt_cons_lt q Q n : q < n -> cnt (q :: Q) n = S (cnt Q n).	L413	identical
60	Lemma	`cnt_cons_ge`	Lemma cnt_cons_ge q Q n : n <= q -> cnt (q :: Q) n = cnt Q n.	L416	identical
61	Lemma	`cnt_app`	Lemma cnt_app X Y n : cnt (X ++ Y) n = cnt X n + cnt Y n.	L419	identical
62	Lemma	`cnt_all_lt`	Lemma cnt_all_lt X n : Forall (fun q => q < n) X -> cnt X n = length X.	L422	identical
63	Lemma	`cnt_all_ge`	Lemma cnt_all_ge X n : Forall (fun q => n <= q) X -> cnt X n = 0.	L428	identical
64	Lemma	`cnt_S_nin`	Lemma cnt_S_nin Q n : ~ In n Q -> cnt Q (S n) = cnt Q n.	L434	identical
65	Lemma	`cnt_S_in`	Lemma cnt_S_in s Q n : valid_from s Q -> In n Q -> cnt Q (S n) = S (cnt Q n).	L444	identical
66	Lemma	`ind_in`	Lemma ind_in Q n : valid Q -> In n Q -> ind Q n = 1.	L454	identical
67	Lemma	`ind_nin`	Lemma ind_nin Q n : ~ In n Q -> ind Q n = 0.	L457	identical
68	Lemma	`ind_iff`	Lemma ind_iff P Q k k' : valid P -> valid Q -> (In k P <-> In k' Q) -> ind P k = ind Q k'.	L460	identical
69	Lemma	`parity_in`	Lemma parity_in s P n : valid_from s P -> In n P -> exists u, n + cnt P n + s = 2 * u + 1.	L467	identical
70	Lemma	`filter_lt_app`	Lemma filter_lt_app X Y k : Forall (fun q => q <= k) X -> filter (fun q => k <? q) (X ++ Y) = filter (fun q => k <? q) Y.	L479	identical
71	Lemma	`filter_filter_lt`	Lemma filter_filter_lt P k k' : k <= k' -> filter (fun p => k' <? p) (filter (fun p => k <? p) P) = filter (fun p => k' <? p) P.	L487	identical
72	Lemma	`filter_all`	Lemma filter_all P k : Forall (fun p => k < p) P -> filter (fun p => k <? p) P = P.	L494	identical
73	Lemma	`filter_gt`	Lemma filter_gt P k p : In p (filter (fun p => k <? p) P) -> k < p.	L500	identical
74	Lemma	`filter_in`	Lemma filter_in P k p : k < p -> (In p (filter (fun p => k <? p) P) <-> In p P).	L503	identical
75	Lemma	`filter_cnt_len`	Lemma filter_cnt_len P n : length (filter (fun p => n <? p) P) + cnt P (S n) = length P.	L508	identical
76	Definition	`Sh`	Definition Sh (u v : nat) (Q P : list nat) : Prop := Forall2 (fun q p => q + u = p + v) Q P.	L517	identical
77	Lemma	`Sh_len`	Lemma Sh_len u v Q P : Sh u v Q P -> length Q = length P.	L519	identical
78	Lemma	`Sh_eq`	Lemma Sh_eq u v u' v' Q P : Sh u v Q P -> u = u' -> v = v' -> Sh u' v' Q P.	L522	identical
79	Lemma	`Sh_filter`	Lemma Sh_filter u v Q P k k' : Sh u v Q P -> k + u = k' + v -> Sh u v (filter (fun q => k <? q) Q) (filter (fun p => k' <? p) P).	L525	identical
80	Lemma	`Sh_in`	Lemma Sh_in u v Q P k k' : Sh u v Q P -> k + u = k' + v -> (In k Q <-> In k' P).	L534	identical
81	Lemma	`Sh_trans`	Lemma Sh_trans u1 v1 u2 v2 u v w X Y Z : Sh u1 v1 X Y -> Sh u2 v2 Y Z -> u1 + u2 = u + w -> v1 + v2 = v + w -> Sh u v X Z.	L540	identical
82	Lemma	`Sh_map`	Lemma Sh_map u v d Q P : Sh u v Q P -> Sh u (v + d) (map (fun q => q + d) Q) P.	L547	identical
83	Lemma	`Sh_unmap`	Lemma Sh_unmap v k P : Forall (fun p => k <= p) P -> Sh (v + k) v (map (fun p => p - k) P) P.	L550	identical
84	Lemma	`Sh_ge`	Lemma Sh_ge u v Q P k k' : Sh u v Q P -> (forall p, In p P -> k' <= p) -> k + u <= k' + v -> Forall (fun q => k <= q) Q.	L553	identical
85	Lemma	`valid_shift`	Lemma valid_shift s k P : valid_from s P -> valid_from (s + k) (map (fun p => p + k) P).	L561	identical
86	Lemma	`valid_map2`	Lemma valid_map2 s P : valid_from s P -> valid_from s (map (fun p => p + 2) P).	L567	identical
87	Lemma	`valid_cons1`	Lemma valid_cons1 Q : valid Q -> valid (1 :: map (fun q => q + 1) Q).	L573	identical
88	Lemma	`valid_unshift`	Lemma valid_unshift s k P : valid_from (s + k) P -> valid_from s (map (fun p => p - k) P).	L576	identical
89	Lemma	`valid_app_l`	Lemma valid_app_l X Y : valid (X ++ Y) -> Forall (fun q => 1 <= q) X.	L583	identical
90	Lemma	`mwf_unshift`	Lemma mwf_unshift s k P : k <= s -> Forall (fun p => k <= p) P -> mwf (s - k) (map (fun p => p - k) P) = mwf s P.	L589	identical
91	Lemma	`mw_cons1`	Lemma mw_cons1 Q : 2 :: 1 :: mw Q = mw (1 :: map (fun q => q + 1) Q).	L596	identical
92	Lemma	`valid_tail_ok`	Lemma valid_tail_ok s P : valid_from s P -> tail_ok (mwf s P).	L599	identical
93	Lemma	`cnt1_valid`	Lemma cnt1_valid P : valid P -> cnt P 1 = 0.	L605	identical
94	Lemma	`in_transfer`	Lemma in_transfer Qi Qe P k k' u v kf : Forall (fun q => q < k) Qi -> Sh u v Qe (filter (fun p => kf <? p) P) -> k + u = k' + v -> kf < k' -> (In k (Qi ++ Qe) <-> In k' P).	L610	identical
95	Lemma	`sh_compose`	Lemma sh_compose Qi Qe Qe' P n a a' k k' : Forall (fun q => q <= k) Qi -> n <= k' -> k + (n + 3) = k' + a -> Sh (k + 3) a' Qe' (filter (fun q => k <? q) (Qi ++ Qe)) -> Sh (n + 3) a Qe (filter (fun p => n <? p) P) -> Sh (k' + 3) a' Qe' (filter (fun p => k' <? p) P).	L619	identical
96	Definition	`Core`	Definition Core (P : list nat) (k a b : nat) (Q : list nat) : Prop := valid Q /\ 2 <= a /\ exists Qi Qe, Q = Qi ++ Qe /\ length Qi + a = b + 1 + ind P k /\ Forall (fun q => q + 2 + ind P k <= a) Qi /\ Sh (k + 3) a Qe (filter (fun p => k <? p) P).	L634	identical
97	Definition	`Inv`	Definition Inv (P : list nat) (n : nat) (W : list nat) : Prop := (Nat.Odd (n + cnt P n) /\ exists a Q, W = a :: 2 :: (n + cnt P n) :: mw Q /\ Core P n a (n + cnt P n) Q) \/ (Nat.Even (n + cnt P n) /\ exists a Q, W = 2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q /\ Core P (S n) a (n + cnt P n - 1) Q).	L639	identical
98	Definition	`Claim`	Definition Claim (Lm : nat) : Prop := forall Q k, k + length Q <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W).	L645	identical
99	Lemma	`stepU`	Lemma stepU P : valid P -> exists W', Ep (1 :: mw P) (cost P 0) W' /\ Inv P 1 W'.	L648	identical
100	Lemma	`stepS`	Lemma stepS P n a Q : valid P -> 1 <= n -> Nat.Even (n + cnt P n) -> Core P (S n) a (n + cnt P n - 1) Q -> exists W', Ep (2 :: 2 :: a :: 2 :: (n + cnt P n - 1) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.	L694	identical
101	Lemma	`stepT_nabs`	Lemma stepT_nabs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> Nat.Odd (n + cnt P n) -> ~ In n P -> Core P n a (n + cnt P n) Q -> exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.	L725	identical
102	Lemma	`stepT_abs`	Lemma stepT_abs Lm P n a Q : Claim Lm -> valid P -> 1 <= n -> n + length P <= Lm -> Nat.Odd (n + cnt P n) -> In n P -> Core P n a (n + cnt P n) Q -> exists W', Ep (a :: 2 :: (n + cnt P n) :: mw Q) (cost P n) W' /\ Inv P (S n) W'.	L770	identical
103	Lemma	`step_lemma`	Lemma step_lemma Lm : Claim Lm -> forall P n W, n + length P <= Lm -> valid P -> Orb P n W -> (1 <= n -> Inv P n W) -> exists W', Ep W (cost P n) W' /\ Inv P (S n) W'.	L819	identical
104	Theorem	`main`	Theorem main Lm : Claim Lm.	L832	identical
105	Lemma	`init`	Lemma init : c0 -->* conf [] [2; 2; 1].	L844	adapted
106	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L847	adapted

5What 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)
submission/parent-proof.md · the parent's proof, as shipped
proof.md (working copy) · differs from the submitted copy

submission/proof.md line 38: 2. Changed rule: R3 becomes R3' (the only TM-level change)

Where A0 is read. By Lemma RM (P§1.1) and the initial segment (§4, whose first 8 steps use no A0), the whole run splits into the macro rules of P§1. Each of them is a fixed transition sequence, listed in P§1. A0 occurs in exactly one of these sequences: as the first transition of R3. R1, R2 and R2e start with A1, and so does HALT. CW, DW and FW use C1/B1/B0, D1 and F1. Every other transition is the same in both machines under σ. So changing A0 changes R3 and nothing else.

Why this is so: in the parent, A is entered only by F0 = 0LA [twin E0 = 0LF], the last transition of every macro rule. A then reads the last cell of lside L. That cell is a 1 when L ≠ [] (the top run), and the edge 0 when L = [], which is the p = 0 case of RM, R3. In the twin, A [twin F] is also entered by the changed transition itself (A0 = 1RA, twin F0 = 1RF), but only inside the R3' detour below.

R3   (parent)  0^inf <A 0 1^(k+1) 0 0 1^m 0 r  -->  0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r     3k+2m+11
               = A0 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
R3'  (twin)    0^inf <A 0 1^(k+1) 0 0 1^m 0 r  -->  0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r     3k+2m+15
               = A0 A0 A1 C1 B1 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
                 [twin names: F0 F0 F1 B1 A1 A0 · CW(k) · ...]

The detour. Call the head cell e, the next cell z (the 0), and the first cell of 1^(k+1) u.

step	transition (parent name, twin name)	effect
1	`A0 = 1RA` (twin `F0 = 1RF`)	e := 1, move right, stay in A
2	`A0`	z := 1, move right
3	`A1 = 1LC` (twin `F1 = 1LB`)	reads u = 1, moves left to z, state C
4	`C1 = 0RB`	z := 0, move right to u, state B
5	`B1 = 1LB`	u stays 1, move left to z
6	`B0 = 1RC`	z := 1, move right to u, state C

The result is e = 1, z = 1, with C reading u. The parent reaches this same configuration after A0 = 1RB, B0 = 1RC. From here both machines run the identical sequence CW(k) · C1 B0 C0 · ..., which uses no A0. The detour touches only e, z and u. It needs u = 1, which holds because c_1 >= 1 in the domain, and the cells left of e play no part. So R3' also holds with an arbitrary left side l 0 <A 0 1^(k+1) ..., which is the form of tR3; tR3c is its instance at the left edge.

Unchanged rules. CW, DW, FW, R1, R2, R2e and HALT (P§1) are unchanged: they use the same transitions in the same order and take the same number of steps. HALT is 0^inf 1 <A 0 r, then A1 C0 D0, and E reads 0 [twin: F1 B0 C0, then D reads 0 at ---]. The twin's macro rules, in parent names, with l and r arbitrary and all parameters >= 0:

R1   l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r  -->  l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r      3m+2x+15   (tR1)
R3'  l 0 <A 0 1^(k+1) 0 0 1^m 0 r        -->  l 1^(k+2) <A 0 1^(m+1) 0 0 r                3k+2m+15   (tR3, tR3c)
R2   l 1^(j+1) 0 1^(k+1) 0 1 <A 0 r       -->  l 1^(j+1) <A 0 1^(k+2) 0 0 r               k+10       (tR2)
R2e  0^inf 1^(k+1) 0 1 <A 0 r             -->  0^inf <A 0 1^(k+2) 0 0 r                   k+10       (tR2, l = 0^inf)
HALT 0^inf 1 <A 0 r                       -->  A1 C0 D0, then E reads 0: halt             3

6FamilyCheck: 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
#12 kill 5	`1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF`	✓Killed: never halts	parent link; named in #12's proof.md; named in #12's notes.md; named in #12b's .v header; named in #12b's proof.md; named in #12b's notes.md · review · compared side by side above · mechanism
#12b kill 6	`1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB`	✓Killed: never halts	this kill

7ChecklistCheck: 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 676 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.3 s
✓
.v hash matches the checked hash
.v = checked sha256 81348b14976e…; submission/ copy = checked sha256 81348b14976e…
✓
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 L61: - No Checkpoint A or 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 L6: - Status: delta proof, written 2026-10-10 (overnight, unattended). Every claim is checked by simulation in `check_proof.py` (labels R, A, C, B, T, H, F, G). Not formalized yet. Checkpoint B (Dennis) is pending.
○
Family posted together?
1 other kill(s) in the family: #12; the Discord draft names 1 of them

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 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB

Files

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

name	size	changed
notes.md ↓	6.4 KB	2026-10-10 09:56
proof.md ↓	17 KB	2026-10-10 09:46
how_proved.md ↓	1.4 KB	2026-10-14 10:51
status.json ↓	434 B	2026-10-10 16:07
1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v ↓	40 KB	2026-10-10 11:50
img/	5 items	2026-10-16 10:29
rocq/	5 items	2026-10-10 09:54
scripts/	2 items	2026-10-10 09:46
submission/	6 items	2026-10-14 09:18
work/	1 item	2026-10-10 15:58
check_proof.py ↓	23 KB	2026-10-10 09:41

status.json in full

{
 "tm": "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-10",
 "reason": "check_kill PASS, independently re-verified",
 "parent": "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF",
 "label": "#12b",
 "relation": "neighbour of #12: one transition away from #12's table (after renaming); its run is nearly identical (134 vs 133 cells at 1e9), so a look-alike, not a sibling"
}

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