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 / W5-8b

`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF`

W5-8blocal proof 28Kill claimedBouncer + Chaotic Edgebbchallenge ↗Explorer parent: W5-8

How we proved it never halts

W5-8's proof in a mirror, from a different start

W5-8's tape is mostly five long blocks of 1s with short words between them; their lengths follow exact rules through 12-trip stretches and collisions of the short words, into a double cycle that repeats forever. W5-8b is W5-8's table seen in a mirror, with its state letters renamed, started in the state that is W5-8's C instead of A. So it shows W5-8's picture in a mirror: the fixed 43-cell pattern sits at the right end and every trip starts there.

A mirror and new state names change nothing about what the machine does, so every rule of W5-8 holds here unchanged, read right to left. What is new is the opening. After 4,098,826 steps the run falls into W5-8's five-block pattern with the lengths W5-8 has when it first gets there, except that the block next to the fixed pattern is 6 cells shorter (1,953 instead of 1,959).

That difference never matters: no rule's result for the other four blocks depends on that block, and the rules only add fixed even amounts to it, which keeps it odd as they require. So the same ten collisions, with the same 12-trip stretches between them, follow in the same order and reach a start of W5-8's double cycle at step 153,013,640, still 6 cells shorter there. From then on W5-8's argument applies unchanged, and the missing transition is never used.

The Rocq proof keeps W5-8's rules and double cycle word for word, for W5-8's table. It replays that table's 4,098,826-step opening from state C, chains the same collisions, and uses busycoq's mirror and renaming lemmas to turn a halt of W5-8b into a halt of that run.

#28local proof number

407lines of Rocq

7 sto compile

6/6automatic checks

Overview

In one sentence

Bouncer. Every round trip starts at a fixed 43-cell gadget G. Beyond it are five 1-blocks n, a, b, c, d with four short particles between them, and a particle turns the head back. (submission/README.md, Mechanism)

parent W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified)

Upstream: Kill claimed · PR #27merged 2026-10-16 07:09 UTC by ccz181078 · PR_BouncerChaoticEdge.v · TM3 · on Submissions →
Rocq proof: check_kill PASS · first Oct 13 06:00
407 lines · 14 KB .v · compile 6.6 s · coqchk pass · 0 axioms · PASS Oct 13 06:00
· the .v file
Automatic review: 6 of 6 checks passtemplate: W5-8's kill file (kill 27) (twin: parent kill's .v) · details in Proof →
Class: Bouncer + Chaotic Edge
On the list: not on BB6_holdouts_663.txt (line 418 of the previous list) · historical 740 line 418
eqv ×1sim 1e15UBRRBA
Derived from: 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LFW5-8 Kill claimed

Your calls on file 1

next: post the Discord draft after the parent's (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); 740 line 636 (same table from E) needs only its own opening + Perm

Mechanism

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

Figures

Fig 1 · bbchallenge default view, 10,000 steps
The site's view. A bouncer: the head sweeps the whole tape, and the right side is ragged from the start.

Fig 2 · One double cycle: Even(212) to Even(244)Q1
Rows go down in time. Follow the dotted diagonal to the wall at left; compare the two halves.

Fig 3 · Right edge to 1e10 stepsQ2
One row per 12 trips. Each tooth is one run; look for any tooth that breaks the two-kind alternation.

More figures (1)Fig 4: Default view, 99,999 steps, wide window

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

rule	from ⟶ to	cases	steps	checked
Sea, right pass	C> 1^2k ⟶ (10)^k C>	any k >= 0	2k	✓200/200
Sea, left pass (composite 11 C>0)	0 (10)^k 1 1 C> 0 ⟶ 0 1 1 C> 0 1^2k	any k >= 0; the cell left of the block is 0	12k	✓200/200
Sea, left pass (composite B>000)	0 (10)^k B> 0 0 0 ⟶ 0 B> 0 0 0 1^2k	any k >= 0; used on the other trip phase	12k	✓200/200
S: 12 round trips	0^∞ <F G 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁴⁸ 0 1^a-8 0 1² 0 1^b+4 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d+4 0 1² 0² 1² 0 1³ 0^∞	n odd >= 1; a even >= 10; b even >= 6; c odd >= 7; d even >= 2 (each bound is the smallest value that works; tested up to 2,000)	84n+84a+77b+70c+63d+13628	✓300/300
TE: P1 hits the wall (even to odd run)	0^∞ <F G 1ⁿ 0 1⁴ 0 1² 0 1^b 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁵⁵⁶ 0 1^b-86 0 1² 0 1⁸² 0⁶ 1^d+51 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	n odd; b even, 88..3,000; d even, 20..2,000 (plus a 25 x 32 grid over b 100..676, d 20..392)	966n+952b+812d+455332 (138 round trips)	✓150/150
TO: P1 hits the wall (odd to even run)	0^∞ <F G 1ⁿ 0 1² 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ ⟶ 0^∞ <F G 1ⁿ⁺⁵⁸⁸ 0 1^b+c-91 0 1² 0 1^d+62 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	n odd; b even >= 82; c odd >= 37; d even >= 18 (half the tests on the reachable line c = b+11, d = b-64, half random)	1029n+1001b+987c+882d+458476 (147 round trips)	✓150/150
Double cycle	Even(n, x) = 0^∞ <F G 1ⁿ 0 1^x 0 1² 0 1^(x+76)/2 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞ ⟶ Even(n+12x+808, x+32)	x = 4 mod 8, x >= 52, n odd. Tested: every x in 52..252, 16 random x up to 5,620, and all 16 even-run starts of the real run up to 1e10	S^((x-4)/8), TE, S^((x-52)/8), TO: 3x+201 round trips	✓42/42
Opening	blank tape, state A ⟶ Even(12863, 212) = 0^∞ <F G 1¹²⁸⁶³ 0 1²¹² 0 1² 0 1¹⁴⁴ 0⁶ 1³⁵ 0 1² 0 1⁴ 0⁶ 1¹⁸ 0 1² 0² 1² 0 1³ 0^∞	direct simulation; it is the first left record of round trip 3,209	153126993	✓1/1

Compressed historythe tape as 0^∞ <F 0² 1² 0 1⁴ 0 1² 0 1⁶ 0 1² 0 1⁵ 0² 1² 0 1⁵ 0 1² 0² 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞ at 35 moments: where the rules are read off

0^∞ <F 0² 1² 0 1⁴ 0 1² 0 1⁶ 0 1² 0 1⁵ 0² 1² 0 1⁵ 0 1² 0² 1ⁿ 0 1^a 0 1² 0 1^b 0⁶ 1^c 0 1² 0 1⁴ 0⁶ 1^d 0 1² 0² 1² 0 1³ 0^∞

step	`n`	`a`	`b`	`c`	`d`
4,097,897	1,959	34	68	45	18
18,629,265	4,351	46	86	89	18
70,933,037	8,675	110	86	133	18
123,039,285	11,503	134	82	157	18
153,126,993	12,863	212	144	35	18
198,114,311	14,667	162	82	173	18
241,393,559	16,215	244	160	35	18
303,350,077	18,211	194	82	189	18
363,208,093	19,951	276	176	35	18
445,948,083	22,139	226	82	205	18
526,157,923	24,071	308	192	35	18
633,882,729	26,451	258	82	221	18
738,604,521	28,575	340	208	35	18
875,902,559	31,147	290	82	237	18
1,009,683,503	33,463	372	224	35	18
1,181,530,261	36,227	322	82	253	18
1,349,304,629	38,735	404	240	35	18
1,561,062,667	41,691	354	82	269	18
1,768,151,803	44,391	436	256	35	18
2,025,570,753	47,539	386	82	285	18
2,277,683,073	50,431	468	272	35	18
2,586,899,639	53,771	418	82	301	18
2,890,130,631	56,855	500	288	35	18
3,257,668,589	60,387	450	82	317	18
3,618,500,813	63,663	532	304	35	18
4,051,271,011	67,387	482	82	333	18
4,476,574,099	70,855	564	320	35	18
4,981,874,457	74,771	514	82	349	18
5,478,905,113	78,431	596	336	35	18
6,064,420,623	82,539	546	82	365	18
6,640,822,623	86,391	628	352	35	18
7,314,625,349	90,691	578	82	381	18
7,978,429,541	94,735	660	368	35	18
8,748,978,619	99,227	610	82	397	18
9,508,602,923	103,463	692	384	35	18

nlast 103,463

alast 692

blast 384

clast 35

dlast 18

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

	0	1
A	1RB	1LD
B	0RC	1RC
C	1LA	1RE
D	---	1LE
E	1RF	0RC
F	0RB	0LF

file: TranslatedBellv5.v:9
module: TM1
machine: 1RB0LA_1LC1LA_0RD0LB_0RE1RC_1LB0RF_1RD--- (11 transitions apart)
diff: different table, same proof architecture. The nearest proved table by transitions is 1RB0LA_1LC1RD_0RB0LC_1LA1RE_1LF0RD_---1LE (distance 3, RWL_mod_v5.v, a decider certificate with no macro rules to reuse)
note: TranslatedBellv5 TM1 proves block-macro rules with ES_v3's symbolic executor (es' a b c d e over word^^n tapes), repeats them with ind, chains them with follow, and ends with progress_nonhalt_cond. Ours needs the same tools for different rules: es' for S (5 variables), TE (3) and TO (4); ind for S^m; follow for the double cycle. The final step is progress_nonhalt_simple over x, since no extra invariant is needed. Bouncer_v2 TM1 shows es' handling a one-variable bouncer BigStep; Bouncer_v3's multistep_c' runs a long opening with nested small counters. New here: the es' calls must cover 12-, 138- and 147-trip stretches.

Proof & checks

6/6 automatic checks pass

Kill 28 · Bouncer + Chaotic Edge · the kill file 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v: 407 lines, 43 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (twin: parent kill's .v): W5-8's kill file (kill 27) · 73% of our lines identical · vs W5-8: same table mirrored, started in W5-8's C; different orbit

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

1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L363

check_kill

✓ PASS · 17/17 checks pass · compile 6.56 s · coqchk pass (44.41 s) · assumptions: 0 (closed) · 2026-10-13 13:00:14 UTC · submission/check_kill.txt

Checked .v

sha256 7bd5af92f5c137c6…

✓	1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v	`7bd5af92f5c137c6…` = checked
✓	submission/1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v	`7bd5af92f5c137c6…` = checked

Status

✓Killed: never halts updated 2026-10-13

✓ args✓ input✓ framework✓ framework_build✓ forbidden✓ structure✓ tm_text✓ theorem_text✓ coq✓ names✓ compile✓ tm_rocq✓ theorem_rocq✓ isolation✓ assumptions✓ coqchk✓ integrity

All 17 check_kill checks with their one-line results

✓	`args`	6x2 machine, framework module Individual62, mode nonhalt
✓	`input`	14395 bytes, 407 lines, 218 sentences
✓	`framework`	HEAD 0940bb9cf434ba68f0c025dabfde45a219999973 == pin; no tracked changes under verify/
✓	`framework_build`	17 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`	6 Require name(s) allowed; no top-level Variable/Context; no shadowing; Module/Section balanced
✓	`tm_text`	line 35: TM_from_str "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF" == <tm> (41 bytes)
✓	`theorem_text`	line 363: nonhalt : ~halts tm c0
✓	`coq`	coqc 8.20.1 (<opam-switch>/bin/coqc)
✓	`names`	halts, c0, TM_from_str resolved inside Individual62
✓	`compile`	compiled in 6.6s with all appended checks
✓	`tm_rocq`	BB6Kill.Candidate.tm = BusyCoq.Individual62.TM_from_str "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF") 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 (44.4s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Same machine as W5-8?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 W5-8 as the parent (1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF); label: “W5-8b”; relation: “sibling of W5-8: W5-8's table mirrored (L<->R) with states renamed sigma = A->B, B->C, C->A, D->D, E->E, F->F (the only map of 720 x 2), started in W5-8's state C; this run = the mirror of the parent's table run from 0^inf C> 0^inf”; parent_note: “W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified)”. Everything below is computed from the two machine strings, not read from notes.

✓ Identical to W5-8's table under the renaming A→B, B→C, C→A, D→D, E→E, F→F (W5-8's state → this machine's), with L and R swapped (mirror image). This machine starts in W5-8's state C (W5-8 itself starts in A). The only such map.

W5-8	W5-8's row (read 0, read 1)	σ	predicted row: renamed by σ, L/R swapped	this machine's actual row
A	`1RB` `1LD`	→ B	`1LC` `1RD`	`1LC` `1RD`	✓	start of W5-8
B	`0RC` `1RC`	→ C	`0LA` `1LA`	`0LA` `1LA`	✓
C	`1LA` `1RE`	→ A	`1RB` `1LE`	`1RB` `1LE`	✓	start of this machine
D	`---` `1LE`	→ D	`---` `1RE`	`---` `1RE`	✓
E	`1RF` `0RC`	→ E	`1LF` `0LA`	`1LF` `0LA`	✓
F	`0RB` `0LF`	→ F	`0LC` `0RF`	`0LC` `0RF`	✓

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

default view of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF — Fig P1 · **bbchallenge default view: W5-8 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: this machine is W5-8's table mirrored, so expect W5-8's picture flipped left to right; it starts in W5-8's state C, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

default view of 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF — Fig P1 · **bbchallenge default view: W5-8 and this machine, first 10,000 steps**
Same view, same settings on both sides. Look for the same band structure: this machine is W5-8's table mirrored, so expect W5-8's picture flipped left to right; it starts in W5-8's state C, not A, so the first steps differ; the numbers below read: different orbit, so expect the same kind of bands, not the same picture.

blaze view of 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF — Fig P2 · **Long run, Blaze (speed): W5-8 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. Here this machine is W5-8's table mirrored, so expect W5-8's picture flipped left to right.

blaze view of 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF — Fig P2 · **Long run, Blaze (speed): W5-8 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. Here this machine is W5-8's table mirrored, so expect W5-8's picture flipped left to right.

Trajectory numbers, from blank (C core)

○ different orbit: 0.012% narrower at 1e9 (34,038 vs 34,042 cells; nonzeros 31,112 vs 23,290); not a fixed offset: the cell gap reaches -10

steps	cells visited (hi − lo + 1)			nonzeros
steps	W5-8	this	ratio (Δ)	W5-8	this	ratio (Δ)
1e5	315	312	0.9905 (-3)	285	292	1.0246 (+7)
1e6	1,078	1,068	0.9907 (-10)	591	883	1.4941 (+292)
1e7	3,442	3,436	0.9983 (-6)	2,350	3,301	1.4047 (+951)
1e8	10,784	10,780	0.9996 (-4)	6,620	7,709	1.1645 (+1,089)
1e9	34,042	34,038	0.9999 (-4)	23,290	31,112	1.3359 (+7,822)

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 W5-8's kill file (kill 27) machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v · detected from status.json

73%of our lines identical to the template

49changed lines

38added lines (ours only)

5template lines dropped

23 / 16 / 4items identical / adapted / new

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

The template is the parent's kill file (adapted from busycoq's verify/TranslatedBellv5.v, Module TM1, ending with progress_nonhalt_simple as in verify/Bouncer_v2.v). Its macro rules, S_iter and DC are kept word for word on the parent's table, renamed tmP. New here: the opening init from C;; tape0 (six cconfig_step pieces cut at left records), opening with new arguments, and the bridge of verify/Skelet15.v: perm : Perm (flip tm) tmP phi with busycoq's flip_halts and perm_halts. The file has 407 lines, every lemma top level.

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

73% identical · 49 changed · 38 added

template 288 lines

81% kept verbatim · 5 not in ours

our items 43

23 identical · 16 adapted · 4 new · 0 template-only

identicalchanged / adaptedours only (new)template only

Template part: whole file, lines 21–361 (leading comment left out). Ours: lines 27–407 (header comment 1–26 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.

Other references found:

adapted from vendor/busycoq/verify/TranslatedBellv5.v Module TM1 (named in 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v line 12)

Side-by-side diff: template (288 lines) vs ours (321 lines), 92 lines differ; runs of identical lines and long template-only runs folded

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

template		ours
22	From BusyCoq Require Import Individual62.	28	From BusyCoq Require Import Individual62.
24	Require Import ZArith Lia.	30	Require Import ZArith Lia.
⋯ 2 identical lines (template 25–26, ours 31–32)
27	From BusyCoq Require Import ES_v3.	33	From BusyCoq Require Import ES_v3.
29	Definition tm := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").	35	Definition tm := Eval compute in (TM_from_str "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF").
31	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
		37	(** tmP: the parent table. All configurations below are tmP's, in its coordinates. *)
32	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
		38	Definition tmP := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").
		40	Notation "c -->* c'" := (c -[ tmP ]->* c') (at level 40).
		41	Notation "c -->+ c'" := (c -[ tmP ]->+ c') (at level 40).
34	(** G: the fixed 43-cell gadget at the left end.	43	(** G: the fixed 43-cell gadget at the left end.
35	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d): F reads the 0 just left of G. *)	44	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d): F reads the 0 just left of G. *)
⋯ 80 identical lines (template 36–133, ours 45–142)
134	all: lia_refl.	143	all: lia_refl.
135	Qed.	144	Qed.
137	( Opening (write-up 5)	146	( Opening (write-up 2)
139	4,097,897 steps from the blank tape to K(1959,34,68,45,18), then 20 macro steps
		148	tmP from C;; tape0: 4,098,826 steps to K(1953,34,68,45,18) = Kr 976 17 34 22 9,
140	to Even(12863,212) = Ev 6431 20.
		149	then 20 macro steps to Even(12857,212) = Ev 6428 20 (the parent's own chain, with
		150	the same a, b, c, d and n smaller by 6).
142	The direct run is cut at five left records (where the tape is short in run-length	152	The direct run is cut at five left records (where the tape is short in run-length
143	form), so that no single computation is too large for the kernel. cc_steps runs	153	form), so that no single computation is too large for the kernel. cc_steps runs
⋯ 4 identical lines (template 144–147, ours 154–157)
148	\| O => Some x	158	\| O => Some x
149	\| S n0 =>	159	\| S n0 =>
150	match cconfig_step tm x with	160	match cconfig_step tmP x with
151	\| Some x0 => cc_steps n0 x0	161	\| Some x0 => cc_steps n0 x0
152	\| None => None	162	\| None => None
⋯ 6 identical lines (template 153–159, ours 163–169)
160	induction n; cbn[cc_steps]; intros x H.	170	induction n; cbn[cc_steps]; intros x H.
161	- inverts H. apply evstep_refl.	171	- inverts H. apply evstep_refl.
162	- pose proof (cconfig_step_spec tm x) as HE.	172	- pose proof (cconfig_step_spec tmP x) as HE.
163	destruct (cconfig_step tm x) as [x0\|]. 2: congruence.	173	destruct (cconfig_step tmP x) as [x0\|]. 2: congruence.
164	eapply evstep_step; eauto.	174	eapply evstep_step; eauto.
165	Qed.	175	Qed.
⋯ 36 identical lines (template 167–207, ours 177–217)
208	cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.	218	cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.
209	Qed.	219	Qed.
211	(** Left record at step 694,884. *)	221	(** Left record at step 696,153. *)
212	Definition W1 : list (nat*nat) :=	222	Definition W1 : list (nat*nat) :=
213	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,746);(2,20);(12,47);(1,20);(6,2);(2,4);(6,2);(1,2)])%nat.	223	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,732);(1,2);(2,14);(2,4);(6,51);(1,2);(1,20);(6,2);(2,4);(6,2);(1,2)])%nat.
215	(** Left record at step 1,397,500. *)	225	(** Left record at step 1,398,101. *)
216	Definition W2 : list (nat*nat) :=	226	Definition W2 : list (nat*nat) :=
217	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1102);(1,2);(1,38);(1,2);(7,35);(1,22);(2,4);(1,2);(2,2);(2,4);(1,2)])%nat.	227	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1088);(2,44);(12,35);(1,22);(2,4);(1,2);(2,2);(2,4);(1,2)])%nat.
219	(** Left record at step 2,099,620. *)	229	(** Left record at step 2,094,215. *)
220	Definition W3 : list (nat*nat) :=	230	Definition W3 : list (nat*nat) :=
221	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1374);(2,132);(6,2);(2,4);(6,7);(1,2);(1,2);(1,2)])%nat.	231	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1365);(2,130);(6,4);(2,2);(2,8);(1,2);(1,2);(1,2);(1,2);(1,2)])%nat.
223	(** Left record at step 2,790,296. *)	233	(** Left record at step 2,795,005. *)
224	Definition W4 : list (nat*nat) :=	234	Definition W4 : list (nat*nat) :=
225	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1599);(1,94);(1,2);(7,35);(1,20);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.	235	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1593);(1,94);(1,2);(7,35);(1,20);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.
227	(** Left record at step 3,493,040. *)	237	(** Left record at step 3,495,649. *)
228	Definition W5 : list (nat*nat) :=	238	Definition W5 : list (nat*nat) :=
229	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1798);(1,2);(2,58);(2,60);(2,44);(1,2);(1,4);(1,2);(1,4);(6,8);(3,6);(1,2)])%nat.	239	([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1792);(1,2);(2,58);(2,60);(2,44);(1,2);(1,4);(1,2);(1,4);(6,8);(3,6);(1,2)])%nat.
231	Lemma init1:	241	Lemma init1:
232	c0 -->* LR W1.
		242	C;; tape0 -->* LR W1.
233	Proof.	243	Proof.
234	change c0 with (cconfig_to_config ([], [], 0, A)).	244	change (C;; tape0) with (cconfig_to_config ([], [], 0, C)).
235	unfold LR.	245	unfold LR.
236	apply (cc_steps'_spec 694 1000 884).	246	apply (cc_steps'_spec 696 1000 153).
237	vm_compute.	247	vm_compute.
238	reflexivity.	248	reflexivity.
⋯ 3 identical lines (template 239–242, ours 249–252)
243	Proof.	253	Proof.
244	unfold LR.	254	unfold LR.
245	apply (cc_steps'_spec 702 1000 616).	255	apply (cc_steps'_spec 701 1000 948).
246	vm_compute.	256	vm_compute.
247	reflexivity.	257	reflexivity.
⋯ 3 identical lines (template 248–251, ours 258–261)
252	Proof.	262	Proof.
253	unfold LR.	263	unfold LR.
254	apply (cc_steps'_spec 702 1000 120).	264	apply (cc_steps'_spec 696 1000 114).
255	vm_compute.	265	vm_compute.
256	reflexivity.	266	reflexivity.
⋯ 3 identical lines (template 257–260, ours 267–270)
261	Proof.	271	Proof.
262	unfold LR.	272	unfold LR.
263	apply (cc_steps'_spec 690 1000 676).	273	apply (cc_steps'_spec 700 1000 790).
264	vm_compute.	274	vm_compute.
265	reflexivity.	275	reflexivity.
⋯ 3 identical lines (template 266–269, ours 276–279)
270	Proof.	280	Proof.
271	unfold LR.	281	unfold LR.
272	apply (cc_steps'_spec 702 1000 744).	282	apply (cc_steps'_spec 700 1000 644).
273	vm_compute.	283	vm_compute.
274	reflexivity.	284	reflexivity.
275	Qed.	285	Qed.
277	Lemma init6:	287	Lemma init6:
278	LR W5 -->* Kr 979 17 34 22 9.	288	LR W5 -->* Kr 976 17 34 22 9.
279	Proof.	289	Proof.
280	unfold LR.	290	unfold LR.
281	rewrite Kr_cc.	291	rewrite Kr_cc.
282	apply (cc_steps'_spec 604 1000 857).	292	apply (cc_steps'_spec 603 1000 177).
283	vm_compute.	293	vm_compute.
284	reflexivity.	294	reflexivity.
285	Qed.	295	Qed.
287	Lemma init:	297	Lemma init:
288	c0 -->* Kr 979 17 34 22 9.	298	C;; tape0 -->* Kr 976 17 34 22 9.
289	Proof.	299	Proof.
290	follow init1.	300	follow init1.
⋯ 5 identical lines (template 291–295, ours 301–305)
296	Qed.	306	Qed.
298	Lemma opening:	308	Lemma opening:
299	Kr 979 17 34 22 9 -->* Ev 6431 20.	309	Kr 976 17 34 22 9 -->* Ev 6428 20.
300	Proof.	310	Proof.
301	unfold Ev.	311	unfold Ev.
302	follow (S_iter 4 979 0 31 19 8).	312	follow (S_iter 4 976 0 31 19 8).
303	follow (TO' 1075 1 4 8).	313	follow (TO' 1072 1 4 8).
304	follow (S_iter 4 1369 2 45 14 8).	314	follow (S_iter 4 1366 2 45 14 8).
305	follow (T6' 1465 15 0 8).	315	follow (T6' 1462 15 0 8).
306	follow (S_iter 6 1761 3 45 14 8).	316	follow (S_iter 6 1758 3 45 14 8).
307	follow (T8' 1905 16 11).	317	follow (T8' 1902 16 11).
308	follow (S_iter 5 2175 2 40 41 8).	318	follow (S_iter 5 2172 2 40 41 8).
309	follow (T6' 2295 12 27 10).	319	follow (T6' 2292 12 27 10).
310	follow (S_iter 12 2591 3 47 14 8).	320	follow (S_iter 12 2588 3 47 14 8).
311	follow (T8' 2879 30 23).	321	follow (T8' 2876 30 23).
312	follow (S_iter 9 3149 0 40 53 8).	322	follow (S_iter 9 3146 0 40 53 8).
313	follow (TO' 3365 20 38 18).	323	follow (TO' 3362 20 38 18).
314	follow (S_iter 17 3659 3 55 14 8).	324	follow (S_iter 17 3656 3 55 14 8).
315	follow (T8' 4067 48 33).	325	follow (T8' 4064 48 33).
316	follow (S_iter 13 4337 2 40 63 8).	326	follow (S_iter 13 4334 2 40 63 8).
317	follow (T6' 4649 28 49 26).	327	follow (T6' 4646 28 49 26).
318	follow (S_iter 22 4945 1 63 14 8).	328	follow (S_iter 22 4942 1 63 14 8).
319	follow (TE' 5473 66 43).	329	follow (TE' 5470 66 43).
320	follow (S_iter 16 5751 2 38 75 8).	330	follow (S_iter 16 5748 2 38 75 8).
321	follow (T6' 6135 32 61 32).	331	follow (T6' 6132 32 61 32).
322	finish.	332	finish.
323	Qed.	333	Qed.
325	Lemma nonhalt: ~halts tm c0.	335	Lemma nonhaltP: ~halts tmP (C;; tape0).
326	Proof.	336	Proof.
327	eapply multistep_nonhalt.	337	eapply multistep_nonhalt.
328	1: { follow init. apply opening. }	338	1: { follow init. apply opening. }
329	apply (progress_nonhalt_simple tm (nat*nat) (fun p => Ev (fst p) (snd p)) (6431,20)).	339	apply (progress_nonhalt_simple tmP (nat*nat) (fun p => Ev (fst p) (snd p)) (6428,20)).
330	intros [N X].	340	intros [N X].
331	exists (48*X+716+N, 4+X).	341	exists (48*X+716+N, 4+X).
332	apply DC.	342	apply DC.
333	Qed.	343	Qed.
		345	( The relation (write-up 1)
		347	phi = sigma^-1 maps this machine's states to tmP's. Every cell (q, s) of flip tm
		348	(this table with the moves reversed) is tmP's cell (phi q, s) with every target
		349	state t replaced by phi t, so flip tm and tmP are equal up to renaming. The blank
		350	tape is its own mirror image (flip_conf c0 = A;; tape0) and phi A = C. *)
		351	Definition phi (q : Q) : Q :=
		352	match q with
		353	\| A => C \| B => A \| C => B \| D => D \| E => E \| F => F
		354	end.
		356	Lemma perm: Perm (flip tm) tmP phi.
		357	Proof.
		358	split.
		359	- intros [] [] H; cbn in *; try discriminate; reflexivity.
		360	- intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
		361	Qed.
		363	Lemma nonhalt: ~halts tm c0.
		364	Proof.
		365	intros H.
		366	apply flip_halts in H.
		367	change (halts (flip tm) (A;; tape0)) in H.
		368	exact (nonhaltP (perm_halts _ _ _ _ _ perm H)).
		369	Qed.
335	(*	371	(*
336	1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (only D0 undefined; D is entered only by A1 = 1LD)	372	1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF (only D0 undefined; D is entered only by B1 = 1RD)
		373	= tmP 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF mirrored (L <-> R), states renamed
		374	sigma = A->B, B->C, C->A, D->D, E->E, F->F (phi = sigma^-1); start A = sigma(C)
		376	relation c --tmP--> c' iff Phi c --tm--> Phi c' (Phi: cell p -> -p, state q -> sigma q)
		377	Phi (C;; tape0) = c0, so tm's run is Phi of tmP's run from C;; tape0
		379	below, configurations are tmP's (left records); tm sees their mirror images (right records)
338	G = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2 (43 cells)	381	G = 0^2 1^2 0 1^4 0 1^2 0 1^6 0 1^2 0 1^5 0^2 1^2 0 1^5 0 1^2 0^2 (43 cells)
339	K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf	382	K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf
		383	Phi K = 0^inf 111 0110 0110 1^d 0^6 1111 0110 1^c 0^6 1^b 0110 1^a 0 1^n G^R F> 0^inf
340	Even(n,x) = K(n, x, (x+76)/2, 35, 18)	384	Even(n,x) = K(n, x, (x+76)/2, 35, 18)
341	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d) Ev N X = Even(2N+1, 8X+52)	385	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d) Ev N X = Even(2N+1, 8X+52)
		387	tmP's rules (tmP's coordinates):
343	R1 C> 1 1 --> 1 0 C> 2 steps C1 E1	388	R1 C> 1 1 --> 1 0 C> 2 steps C1 E1
344	R2b 0 1 0 B> 0 0 0 --> 0 B> 0 0 0 1 1 12 steps B0 C0 A0 B1 C0 A1 D1 E0 F1 F1 F1 F0	389	R2b 0 1 0 B> 0 0 0 --> 0 B> 0 0 0 1 1 12 steps B0 C0 A0 B1 C0 A1 D1 E0 F1 F1 F1 F0
⋯ 9 identical lines (template 345–355, ours 390–400)
356	n odd, x = 4 mod 8, x >= 52; 3x+201 trips	401	n odd, x = 4 mod 8, x >= 52; 3x+201 trips
357	(Rocq: Ev N X -->+ Ev (48X+716+N) (X+4))	402	(Rocq: Ev N X -->+ Ev (48X+716+N) (X+4))
359	start c0 -->(4,097,897) K(1959,34,68,45,18) --(S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6)-->	404	start C;; tape0 -(4,098,826)-> K(1953,34,68,45,18) --(S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6)-->
360	Even(12863,212) at step 153,126,993; then DC forever (x = 212, 244, 276, ...)	405	Even(12857,212) at step 153,013,640; then DC forever (x = 212, 244, 276, ...)
		406	(the same for tm from c0, through Phi)
361	*)	407	*)

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

43 items in 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v (407 lines): 27 Lemma, 13 Definition, 3 Fixpoint. Tags against the template: identical = same name and same text once each file's own TM string is <TM> (marked "except the TM string" when that is the only difference); adapted = same name, different text; new = no item of that name in the template part.

#	kind	name	statement (no proof body)	line	vs template
1	Definition	`tm`	Definition tm := Eval compute in (TM_from_str "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF").	L35	identicalexcept the TM string
2	Definition	`tmP`	Definition tmP := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").	L38	new
3	Definition	`G`	Definition G : list sym := [0;0;1;1;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;0;1;1;0;1;1;1;1;1;0;1;1;0;0].	L45	identical
4	Definition	`Kr`	Definition Kr n a b c d := 0inf <{{F}} G > [1] > [1;1]^^n > [0] > [1;1]^^a > [0;1;1;0] > [1;1]^^b > [0;0;0;0;0;0] > [1] > [1;1]^^c > [0;1;1;0;1;1;1;1;0;0;0;0;0;0] > [1;1]^^d > [0;1;1;0;0;1;1;0;1;1;1] *> 0inf.	L48	identical
5	Lemma	`S_step`	Lemma S_step n a b c d: Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d).	L59	identical
6	Lemma	`TE`	Lemma TE n b d: Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9.	L66	identical
7	Lemma	`TO`	Lemma TO n b c d: Kr n 1 (41+b) (18+c) (9+d) -->+ Kr (294+n) (14+b+c) (40+d) 17 9.	L73	identical
8	Lemma	`T6`	Lemma T6 n b c d: Kr n 3 (41+b) (17+c) (9+d) -->+ Kr (296+n) (13+b+c) (40+d) 17 9.	L80	identical
9	Lemma	`T8`	Lemma T8 n b d: Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9.	L87	identical
10	Lemma	`S_step'`	Lemma S_step' n a b c d: Kr n (5+a) (3+b) (3+c) (1+d) -->* Kr (24+n) (1+a) (5+b) (3+c) (3+d).	L93	identical
11	Lemma	`TE'`	Lemma TE' n b d: Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.	L97	identical
12	Lemma	`TO'`	Lemma TO' n b c d: Kr n 1 (41+b) (18+c) (9+d) -->* Kr (294+n) (14+b+c) (40+d) 17 9.	L101	identical
13	Lemma	`T6'`	Lemma T6' n b c d: Kr n 3 (41+b) (17+c) (9+d) -->* Kr (296+n) (13+b+c) (40+d) 17 9.	L105	identical
14	Lemma	`T8'`	Lemma T8' n b d: Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.	L109	identical
15	Lemma	`S_iter`	Lemma S_iter k: forall n a b c d, Kr n (4k+1+a) (3+b) (3+c) (1+d) --> Kr (24k+n) (1+a) (2k+3+b) (3+c) (2*k+1+d).	L114	identical
16	Definition	`Ev`	Definition Ev N X := Kr N (4X+26) (2X+32) 17 9.	L128	identical
17	Lemma	`prog_eq`	Lemma prog_eq c1 c2 c1' c2': c1 -->+ c2 -> c1 = c1' -> c2 = c2' -> c1' -->+ c2'.	L130	identical
18	Lemma	`DC`	Lemma DC N X: Ev N X -->+ Ev (48*X+716+N) (4+X).	L134	identical
19	Fixpoint	`cc_steps`	Fixpoint cc_steps (n:nat) (x:cconfig) : option cconfig := match n with \| O => Some x \| S n0 => match cconfig_step tmP x with \| Some x0 => cc_steps n0 x0 … +3 lines	L156	adapted
20	Lemma	`cc_steps_spec`	Lemma cc_steps_spec n x y: cc_steps n x = Some y -> cconfig_to_config x -->* cconfig_to_config y.	L166	adapted
21	Fixpoint	`cc_steps'`	Fixpoint cc_steps' (n1 n2 n3:nat) (x:cconfig) : option cconfig := match n1 with \| O => cc_steps n3 x \| S n1 => match cc_steps n2 x with \| Some x0 => cc_steps' n1 n2 n3 x0 … +3 lines	L177	identical
22	Lemma	`cc_steps'_spec`	Lemma cc_steps'_spec n1 n2 n3 x y: cc_steps' n1 n2 n3 x = Some y -> cconfig_to_config x -->* cconfig_to_config y.	L187	identical
23	Fixpoint	`rl`	Fixpoint rl (xs : list (nat*nat)) : list sym := match xs with \| [] => [] \| (z,o)::t => [0]^^z ++ [1]^^o ++ rl t end.	L200	identical
24	Definition	`LR`	Definition LR (xs : list (natnat)) : Q tape := cconfig_to_config ([], rl xs, 0, F).	L207	identical
25	Definition	`Kr_list`	Definition Kr_list n a b c d : list sym := G ++ [1] ++ [1;1]^^n ++ [0] ++ [1;1]^^a ++ [0;1;1;0] ++ [1;1]^^b ++ [0;0;0;0;0;0] ++ [1] ++ [1;1]^^c ++ [0;1;1;0;1;1;1;1;0;0;0;0;0;0] ++ [1;1]^^d ++ [0;1;1;0;0;1;1;0;1;1;1].	L209	identical
26	Lemma	`Kr_cc`	Lemma Kr_cc n a b c d: Kr n a b c d = cconfig_to_config ([], Kr_list n a b c d, 0, F).	L214	identical
27	Definition	`W1`	Definition W1 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,732);(1,2);(2,14);(2,4);(6,51);(1,2);(1,20);(6,2);(2,4);(6,2);(1,2)])%nat.	L222	adapted
28	Definition	`W2`	Definition W2 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1088);(2,44);(12,35);(1,22);(2,4);(1,2);(2,2);(2,4);(1,2)])%nat.	L226	adapted
29	Definition	`W3`	Definition W3 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1365);(2,130);(6,4);(2,2);(2,8);(1,2);(1,2);(1,2);(1,2);(1,2)])%nat.	L230	adapted
30	Definition	`W4`	Definition W4 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1593);(1,94);(1,2);(7,35);(1,20);(2,20);(1,2);(1,4);(1,2);(3,4);(1,2)])%nat.	L234	adapted
31	Definition	`W5`	Definition W5 : list (nat*nat) := ([(2,2);(5,2);(6,4);(6,4);(1,2);(1,4);(1,2);(2,1792);(1,2);(2,58);(2,60);(2,44);(1,2);(1,4);(1,2);(1,4);(6,8);(3,6);(1,2)])%nat.	L238	adapted
32	Lemma	`init1`	Lemma init1: C;; tape0 -->* LR W1.	L241	adapted
33	Lemma	`init2`	Lemma init2: LR W1 -->* LR W2.	L251	adapted
34	Lemma	`init3`	Lemma init3: LR W2 -->* LR W3.	L260	adapted
35	Lemma	`init4`	Lemma init4: LR W3 -->* LR W4.	L269	adapted
36	Lemma	`init5`	Lemma init5: LR W4 -->* LR W5.	L278	adapted
37	Lemma	`init6`	Lemma init6: LR W5 -->* Kr 976 17 34 22 9.	L287	adapted
38	Lemma	`init`	Lemma init: C;; tape0 -->* Kr 976 17 34 22 9.	L297	adapted
39	Lemma	`opening`	Lemma opening: Kr 976 17 34 22 9 -->* Ev 6428 20.	L308	adapted
40	Lemma	`nonhaltP`	Lemma nonhaltP: ~halts tmP (C;; tape0).	L335	new
41	Definition	`phi`	Definition phi (q : Q) : Q := match q with \| A => C \| B => A \| C => B \| D => D \| E => E \| F => F end.	L351	new
42	Lemma	`perm`	Lemma perm: Perm (flip tm) tmP phi.	L356	new
43	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L363	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 128: 1.4 The parent's rules carry over

Each rule of the parent is an exact run of the parent's table: the shift rules R1 and R2b, the macro rules S, TE, TO, T6 and T8 (P§1, P§3). By Lemma M the mirror of each is an exact run of this machine, with the same domain and the same step count.

In particular the double cycle (P§4) holds here in the form

Phi Even(n, x)  -->  Phi Even(n + 12x + 808, x + 32)        (n odd, x = 4 mod 8, x >= 52)

From here on, configurations are written in the parent's coordinates, as members K(...) of the parent's table run from C. On this machine they are read through Φ.

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

3 machines, 3 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
W5-8 kill 27	`1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF`	✓Killed: never halts	parent link; = W5-8b's table mirrored, run from state B; named in W5-8b's .v header; named in W5-8b's proof.md; named in W5-8b's notes.md · review · compared side by side above · mechanism
W5-8b kill 28	`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF`	✓Killed: never halts	this kill
W5-8c kill 29	`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA`	✓Killed: never halts	= W5-8b's table mirrored, run from state E; named in W5-8c's proof.md; named in W5-8b's notes.md · review

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 447 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 44.41 s
✓
.v hash matches the checked hash
.v = checked sha256 7bd5af92f5c1…; submission/ copy = checked sha256 7bd5af92f5c1…
✓
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 L57: - Checkpoint B (Dennis, non-blocking).
- proof.md L209: ## 8. Checkpoint B (Dennis)
○
Family posted together?
2 other kill(s) in the family: W5-8, W5-8c; 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 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF

Files

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

name	size	changed
notes.md ↓	7.3 KB	2026-10-13 06:38
proof.md ↓	15 KB	2026-10-13 05:49
how_proved.md ↓	1.6 KB	2026-10-14 10:51
status.json ↓	4.6 KB	2026-10-16 10:28
1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v ↓	14 KB	2026-10-13 05:54
img/	5 items	2026-10-16 10:29
rocq/	11 items	2026-10-13 05:59
scripts/	1 item	2026-10-13 05:34
submission/	6 items	2026-10-14 09:18
work/	8 items	2026-10-13 05:49
check_proof.py ↓	25 KB	2026-10-13 05:41

status.json in full

{
 "tm": "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF",
 "label": "W5-8b",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "confidence": "high",
 "parent": "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF",
 "parent_note": "W5-8 (740 line 214), KILLED_NONHALT 2026-10-13 (check_kill PASS, sha256 beef54a5..cf48, independently re-verified)",
 "relation": "sibling of W5-8: W5-8's table mirrored (L<->R) with states renamed sigma = A->B, B->C, C->A, D->D, E->E, F->F (the only map of 720 x 2), started in W5-8's state C; this run = the mirror of the parent's table run from 0^inf C> 0^inf",
 "holdout_line_740": 418,
 "checks": {
  "byte_exact_740": "line 418, exactly once, no CR",
  "claims": "none: sheet Results row = class 'Bouncer + Chaotic Edge' only (no status/notes/sources/done-by), level-0 row no status; Discord only mxdys's UBRRBA_TODO list (data/discord/2026-08-24_mxdys_ubrrba_86.txt line 85), an acceleration to-do list, not a claim",
  "upstream_9cf9e88": "not proved: no .v in the 9cf9e88 verify tree (plus local PR commit 69c43b6) contains any of the 1,440 renaming/mirror variants of the table; tools/holdouts.py solved: absent from verify/",
  "canon": "canon(this, start A) == canon(parent, start C) (renaming + mirror)"
 },
 "opening": "blank --(4,098,826 direct steps)--> Phi K(1953,34,68,45,18) (first K-shaped right record), then the parent's 20-row chain S^4 TO S^4 T6 S^6 T8 S^5 T6 S^12 T8 S^9 TO S^17 T8 S^13 T6 S^22 TE S^16 T6 with the parent's a,b,c,d and n - 6 -> Phi Even(12857,212) at step 153,013,640; from there the parent's double cycle (no adjusted invariant)",
 "proof_md": "proof.md (working delta proof); public write-up submission/proof.md (writeup_lint 0/0) + submission/parent-proof.md",
 "check_proof": {
  "result": "PASS",
  "claims": "58/58 seed 1 default (93 s), 58/58 seed 2 default (93 s), 58/58 seed 1 --full (321 s); each re-ran the parent's check_proof.py in the same mode (196/196); DOC/INV/K re-run 11/11 after the last prose pass",
  "out": [
   "work/check_proof_seed1.log",
   "work/check_proof_seed2.log",
   "work/check_proof_full_seed1.log",
   "work/check_proof_doc_after_prose.log",
   "work/parent_check_proof_default_seed1.log",
   "work/parent_check_proof_default_seed2.log",
   "work/parent_check_proof_full_seed1.log"
  ],
  "teeth": "n=1955 in the opening start -> 5 FAIL; wrong sigma -> REL+DOC FAIL; one wrong step number in proof.md -> DOC FAIL",
  "cross_check": "tools/sim.py engine (sim.run) reproduces Phi K(1953,34,68,45,18) at 4,098,826 and Phi Even(12857,212) at 153,013,640"
 },
 "open_lemmas": [],
 "next": "post the Discord draft after the parent's (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); 740 line 636 (same table from E) needs only its own opening + Perm",
 "workflow_name": "W5-8b",
 "template": "parent W5-8's kill file (TranslatedBellv5.v TM1 style) on tmP + Perm (flip tm) tmP phi / flip_halts / perm_halts bridge as verify/Skelet15.v",
 "kill": {
  "file": "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v",
  "sha256": "7bd5af92f5c137c6355744f598e7882be3101d63ee857bbe02e970d083b326f0",
  "lines": 407,
  "check_kill": "PASS (fresh run 2026-10-13T13:00:14Z: compile 6.6 s native, coqchk pass 44.4 s, 0 assumptions; rocq/check_kill_final.log; also rocq/check_kill_r1.log (round 1) and the independent auditor run, same sha256)",
  "route": "proof.md 6 route 1 (conjugacy): parent's development on tmP, new opening C;; tape0 -->* Kr 976 17 34 22 9 (4,098,826 steps, six pieces at left records), 20 follows to Ev 6428 20, progress_nonhalt_simple; rocq/assemble.py builds the file from the parent's",
  "submission": "submission/",
  "discord": "submission/discord.md, not posted (fill in <LINK>; post after the parent's message and fix its 'not formalized' sentence)"
 },
 "outcome": "never halts (check_kill PASS, independently re-verified; delta proof from W5-8 complete)",
 "alias_labels": [
  "W5-8d"
 ],
 "redispatch_2026-10-13": "re-dispatched as W5-8d (delta-proof task); already KILLED_NONHALT as W5-8b, nothing redone. Re-checked: byte-exact 740 line 418 (once), canon(this,A)==canon(parent,C) (only start C), .v sha256 7bd5af92..26f0 unchanged = check_kill_final.log PASS, check_proof logs 58/58 (seeds 1,2, --full), no sheet/Discord data newer than this status",
 "pr": "https://github.com/ccz181078/busycoq/pull/27",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB1LE_1LC1RD_0LA1LA_HHH1RE_1LF0LA_0LC0RF.v",
 "pr_opened": "2026-10-15T22:48:31Z",
 "pr_comments": 0,
 "pr_head_sha": "94903f626ae503be6be39ac40e53038ab98ac4d8",
 "posted": "2026-10-15 (Discord; user confirmed sent)",
 "pr_merged_at": "2026-10-16T07:09:03Z",
 "pr_merged_by": "ccz181078"
}

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 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF (the kill review: python3 -B tools/killreview.py 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF, which also renders a derived kill's same-machine pictures)