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-8

`1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF`

W5-8local proof 27Kill claimedBouncer + Chaotic Edgebbchallenge ↗Explorer

How we proved it never halts

Exact rules for five block lengths, and a double cycle that repeats forever

The tape is mostly five long blocks of 1s, with short words between them, the "particles", and a 43-cell pattern at the left end that is the same at the start of every trip. Each trip runs right across the first block, sometimes further, until a particle turns the head back; how far it gets follows a 12-trip cycle. Every 12 trips the first block grows by 48 cells and the second shrinks by 8, so the particles around the second block close in. When it is down to 2, 4, 6 or 8 cells they collide, and 135 to 147 trips later the five blocks are back with new lengths.

The key idea: each of these events is an exact rule on the five lengths, one for 12 ordinary trips and one for each of the four kinds of collision. Each rule is proved once for all lengths in a stated range, by running the machine on a tape whose block lengths are symbols.

Why that settles it: two of the collisions, at 4 cells and at 2, alternate forever. Call the tape a checkpoint when the first block has odd length, the third is 38 longer than half the second, the fourth is 35 and the fifth 18. From a checkpoint whose second block is at least 52 and leaves remainder 4 when divided by 8, the rules lead through both collisions to another checkpoint, with the second block 32 longer. The run reaches the first checkpoint at step 153,126,993, and every later step lies inside a rule that avoids the missing transition.

The Rocq proof (checked against busycoq) proves the five rules with busycoq's symbolic executor, replays the 4,097,897-step opening exactly, and chains the rules from there to the first checkpoint and from each checkpoint to the next.

#27local proof number

361lines of Rocq

7 sto compile

6/6automatic checks

Overview

In one sentence

Bouncer whose right edge is a 4-particle system; the law Even(x) -> Even(x+32) repeats forever, so it never halts.

Submitted mechanism Bouncer. Every round trip starts at a fixed 43-cell gadget G at the left end. Right of it are five 1-blocks n, a, b, c, d with four short particles between them. The head crosses blocks by C> 11 -> 10 C> going right and 0 10 B> 000 -> 0 B> 000 11 going left, and a particle turns it back; how far it gets depends on the phase (period 12 trips). (submission/README.md, Mechanism)

Upstream: Kill claimed · PR #27merged 2026-10-16 07:09 UTC by ccz181078 · PR_BouncerChaoticEdge.v · TM1 · on Submissions →
Rocq proof: check_kill PASS · first Oct 13 05:23
361 lines · 12 KB .v · compile 6.6 s · coqchk pass · 0 axioms · PASS Oct 13 05:23
· the .v file
Automatic review: 6 of 6 checks passtemplate: verify/TranslatedBellv5.v Module TM1 (adapted from) · details in Proof →
Class: Bouncer + Chaotic Edgeours: sheet Bouncer + Chaotic Edge ≠ ours Bouncer with a 4-particle right edge (closed double-cycle law; the edge is not chaotic) · high confidence
On the list: not on BB6_holdouts_663.txt (line 214 of the previous list) · historical 740 line 214 · observe.json rank #214
eqv ×1sim 1e15UBRRBA

Your calls on file 1

next: post the Discord draft (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); siblings 740 lines 418/636 need only their own openings + Perm/flip (proof.md 7.3)

Mechanism

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

How it works: 3 notes

A bouncer: the left end is a fixed gadget G (lo moves 2 left per trip), and the rest is a sea of 1s that each pass rewrites 1^(2k) <-> (10)^k. The left pass uses a moving composite, 11 C>0 or B>000.
In the sea float 4 particles: a wall W and an edge E (fixed relative to the right end), a fast P1 and two slow Q, Q'. Every 12 trips: K(n,a,b,c,d) -> K(n+48,a-8,b+4,c,d+4).
When P1 reaches W, one of two collisions (TE, TO) fires, in alternation. Even(x) = K(n,x,(x+76)/2,35,18) -> Even(x+32) for x = 4 mod 8, x >= 52, so the macro rules chain forever. The run enters Even(212) at step 153,126,993; halting (A on 1 after a 0) never occurs.

Figures for Checkpoint A

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.

Checkpoint A · 3 open

check: does the figure show what I claim? A “no” stops proof work built on a wrong reading. decision: your call.

Q1
check Fig 2 shows one double cycle from the real tape at step 153,126,993. Do you see two runs, each ending when the dotted fast line reaches the wall at the left? Does the wall step left after each, the second run's slow thin line end at the next run, and the bottom row look like the top?
Q2
check Fig 3 runs to 1e10 steps. Does every tooth after the first few belong to one of the same two kinds, in alternation, only longer each time, with no third kind of event?
Q3
decision Plan: one ES_v3 file for this table (S, TE, TO, double cycle) with three openings, for 214, 418 (start C, mirrored) and 636 (start E). Go with all three in one stage, or prove 214 alone first?

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 strategy & riskshow the formal proof will go · 3 risks to watch

Write K(n,a,b,c,d) for ES_v3. Prove S, TE and TO each with one es' call, S^m by ind, and Even(x) ->+ Even(x+32) by follow. Prove the 153,126,993-step opening with a nested multistep_c' and finish with progress_nonhalt_simple. 418 and 636 reuse the lemmas with new openings.

▲es' must find every shift rule across the 138- and 147-trip transitions within the fuel bound. Fallback: split TE and TO into one lemma per few trips.
▲The opening is 153M steps, 11x the largest stepn in busycoq; N.to_nat of 153M is a 153M-deep unary nat. Use Bouncer_v3's nested multistep_c' (small counters), or begin from a smaller Even(x) if a shorter opening is found.
▲Exponent normal forms: K's blocks need a representation that es' rewrites both ways (n = 2n'+1, a = 2a'+10 and so on), or the final config comparison fails.

Stats & provenance10¹⁰ steps simulated · 107,321 cells · the status in full · files

simulated: 10¹⁰ steps
tape: 107,321 cells
growth: span ~ 1.07 sqrt(steps): lo moves -2 per round trip, hi about +2.05; 26,506 trips to 1e10; right part (wall to edge) ~ 1,180 cells at 1e10, +48 per double cycle
status now: check_kill PASS, independently re-verified (status.json, 2026-10-13)
observer's note: Mechanism closed. Every regime from blank to 1e10 is covered by validated rules: the opening to Even(212) at 153,126,993 steps, then S, TE and TO. The law Even(x) -> Even(x+32) was validated from constructed tapes up to x = 5,620. Not proved in Rocq yet.
files: observe.json · notes.md · proof.md · how_proved.md · status.json · 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v

Proof & checks

6/6 automatic checks pass

Kill 27 · Bouncer + Chaotic Edge · the kill file 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v: 361 lines, 39 items · the package submission/

✓ 6/6 automatic checks pass · Checkpoint B: no note from Dennis yet · template (adapted from): verify/TranslatedBellv5.v Module TM1 · 17% of our lines identical

1What is provedCheck: the string, the theorem and every check_kill line are green, and the .v on disk is the one that was checked (same sha256).

Machine

1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF

vs holdout list

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

Theorem

✓ Lemma nonhalt: ~halts tm c0. L325

check_kill

✓ PASS · 17/17 checks pass · compile 6.63 s · coqchk pass (44.9 s) · assumptions: 0 (closed) · 2026-10-13 12:23:55 UTC · submission/check_kill.txt

Checked .v

sha256 beef54a54f6272e7…

✓	1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v	`beef54a54f6272e7…` = checked
✓	submission/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v	`beef54a54f6272e7…` = 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`	12214 bytes, 361 lines, 203 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 29: TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF" == <tm> (41 bytes)
✓	`theorem_text`	line 325: 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 "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF" by eq_refl (in-file and isolated)
✓	`theorem_rocq`	nonhalt : ~ halts (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF") 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.9s); its context summary lists nothing of the file's own
✓	`integrity`	input sha256 and framework HEAD/cleanliness identical before and after

2Where it came fromCheck: the template is the one you expect, and the measured reuse (tiles, the reuse figure, diff) agrees with what the README says was kept and changed (quoted).

adapted from verify/TranslatedBellv5.v Module TM1 · detected from 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v line 5

17%of our lines identical to the template

1changed lines

239added lines (ours only)

937template lines dropped

1 / 1 / 37items identical / adapted / new

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

Adapted from busycoq's verify/TranslatedBellv5.v, Module TM1: block macro rules by es', repeated by induction and chained with follow. Changes: fixed five-block configurations instead of TM1's lists, and no invariant, so the proof ends with progress_nonhalt_simple as in verify/Bouncer_v2.v Module TM1. The long opening uses nested step counters as in verify/Bouncer_v3.v's multistep_c', cut into six pieces so that coqchk can re-check each computation. The file has 361 lines, every lemma top level.

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

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

ours 288 lines

17% identical · 1 changed · 239 added

template 986 lines

5% kept verbatim · 937 not in ours

our items 39

1 identical · 1 adapted · 37 new · 60 template-only

identicalchanged / adaptedours only (new)template only

Template part: lines 1–8 (shared header, before the first Module) + 10–1062 (body of Module TM1; the Module/End lines left out). Ours: lines 21–361 (header comment 1–20 left out). Line diff: Python difflib SequenceMatcher; inside a replaced block, line pairs at least 75% alike count as changed, the rest as removed + added.

Template-only names: RC, T, S1, S2, LC, L0, S3, S4, S5, Inc1, Incs1, Inc2, Incs2, Ov1, Incs12, Ov2_0, Ov2_1, Ov2_2, Ov2_3, S3_1, S3_0, S3_1_0, S3_0_0_0, S3_0_0_1, S4_0, S4_1, S4_O, S3_rh, S3_rh_0, S5_S, S5_O, RInc_1, mul2, S43_Incs, S43_Incs_O, RInc_2, RInc_2_O, RIncs_1, RIncs_2, RIncs_2_O …

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

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

template		ours
1	From BusyCoq Require Import Individual62.	22	From BusyCoq Require Import Individual62.
3	Require Import ZArith Lia.	24	Require Import ZArith Lia.
4	Require Import String.	25	Require Import String.
5	Require Import List.	26	Require Import List.
6	From BusyCoq Require Import ES_v3 DivModCases.	27	From BusyCoq Require Import ES_v3.
10	Definition tm := Eval compute in (TM_from_str "1RB0LA_1LC1LA_0RD0LB_0RE1RC_1LB0RF_1RD---").	29	Definition tm := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").
12	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).	31	Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
13	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).	32	Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).
15	Fixpoint RC ls :=
		34	(** G: the fixed 43-cell gadget at the left end.
16	match ls with
		35	Kr n a b c d = K(2n+1, 2a, 2b, 2c+1, 2d): F reads the 0 just left of G. *)
17	\| [] => 0inf
		36	Definition G : list sym :=
18	\| (true,a)::ls => [1] > [0;1]^^a > RC ls
		37	[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].
19	\| (false,a)::ls => [0] > [0;1]^^a > RC ls
		39	Definition Kr n a b c d :=
20	end.
		40	0inf <{{F}} G > [1] > [1;1]^^n > [0] > [1;1]^^a > [0;1;1;0] > [1;1]^^b
22	Fixpoint T (ls:list nat) :=
		41	> [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
23	match ls with
		42	> [0;1;1;0;0;1;1;0;1;1;1] > 0inf.
24	\| [] => []
		44	Ltac ES_v3.es_v3_pre ::= unfold Kr, G.
25	\| a::ls => (true,2+a)::T ls
		46	( Macro rules (write-up 3.3, 3.4)
26	end.
		48	S (12 trips): K(n,a,b,c,d) -> K(n+48, a-8, b+4, c, d+4),
28	Definition S1 a b c d r :=
		49	n odd, a even >= 10, b even >= 6, c odd >= 7, d even >= 2. *)
29	0inf <{{A}} [1;0] > [1;0;1;0;1;0;1;0;0]^^a > [1;0;1;0] > [1;0;1;0;0]^^b > [1;0;1;0;1;0;1;1;0]^^c > [1;0;1;0] > [1;0;1;1;0]^^d *> RC (T r).
		50	Lemma S_step n a b c d:
31	Definition S2 a b c d e r :=
		51	Kr n (5+a) (3+b) (3+c) (1+d) -->+ Kr (24+n) (1+a) (5+b) (3+c) (3+d).
32	0inf <{{A}} [1;0] > [1;0;1;0;1;0;1;0;0]^^a > [1;0;1;0] > [1;0;1;0;0]^^b > [1;0;1;0]^^(1+c) > [0] > [1;0;1;0]^^(1+d) > [0;1;0;1;0;0;0] > [1;0;1;1;0]^^e *> RC (T r).
34	Fixpoint LC ls l :=
⋯ 15 template-only lines (template 35–56), not in ours
57	S1 a b (1+c) d r -->*
58	S1 (1+a) (1+b) c d r.
59	Proof.	52	Proof.
60	es' a b c d & (RC (T r)).
		53	es' n a b c d.
61	Qed.	54	Qed.
63	Lemma Incs1 a b c d r:
		56	(** TE (138 trips): K(n,4,b,35,d) -> K(n+556, b-86, 82, d+51, 18), b even >= 88, d even >= 20. *)
64	S1 a b c d r -->*
		57	Lemma TE n b d:
65	S1 (c+a) (c+b) 0 d r.
		58	Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9.
66	Proof.	59	Proof.
67	gen a b.
		60	es' n b d.
68	ind c Inc1.
69	Qed.	61	Qed.
71	Lemma Inc2 a b c d e r:
		63	(** TO (147 trips): K(n,2,b,c,d) -> K(n+588, b+c-91, d+62, 35, 18), b even >= 82, c odd >= 37, d even >= 18. *)
72	S2 a b c d (4+e) r -->*
		64	Lemma TO n b c d:
73	S2 (2+a) b (2+c) (1+d) e r.
		65	Kr n 1 (41+b) (18+c) (9+d) -->+ Kr (294+n) (14+b+c) (40+d) 17 9.
74	Proof.	66	Proof.
75	es' a b c d e & (RC (T r)).
		67	es' n b c d.
76	Qed.	68	Qed.
78	Lemma Incs2 n a b c d e r:
		70	(** T6 (147 trips): K(n,6,b,c,d) -> K(n+592, b+c-91, d+62, 35, 18), b even >= 82, c odd >= 35, d even >= 18. *)
79	S2 a b c d (n4+e) r -->
		71	Lemma T6 n b c d:
80	S2 (n2+a) b (n2+c) (n+d) e r.
		72	Kr n 3 (41+b) (17+c) (9+d) -->+ Kr (296+n) (13+b+c) (40+d) 17 9.
81	Proof.	73	Proof.
82	gen a c d e.
		74	es' n b c d.
83	ind n Inc2.
84	Qed.	75	Qed.
86	Lemma Ov1 a b d r:
		77	(** T8 (135 trips): K(n,8,b,35,d) -> K(n+540, b-74, 86, d+47, 18), b even >= 88, d even >= 20. *)
87	S1 a (2+b) 0 (2+d) r -->*
		78	Lemma T8 n b d:
88	S2 (2+a) b 0 0 d r.
		79	Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9.
89	Proof.	80	Proof.
90	es' a b d & (RC (T r)).
		81	es' n b d.
91	Qed.	82	Qed.
93	Lemma Incs12 a b n rs:
		84	Lemma S_step' n a b c d:
94	S1 0 1 (1+a) (2+n4+b) rs -->
		85	Kr n (5+a) (3+b) (3+c) (1+d) -->* Kr (24+n) (1+a) (5+b) (3+c) (3+d).
95	S2 (3+n2+a) a (n2) n b rs.
		86	Proof. apply progress_evstep, S_step. Qed.
		88	Lemma TE' n b d:
		89	Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.
		90	Proof. apply progress_evstep, TE. Qed.
		92	Lemma TO' n b c d:
		93	Kr n 1 (41+b) (18+c) (9+d) -->* Kr (294+n) (14+b+c) (40+d) 17 9.
		94	Proof. apply progress_evstep, TO. Qed.
		96	Lemma T6' n b c d:
		97	Kr n 3 (41+b) (17+c) (9+d) -->* Kr (296+n) (13+b+c) (40+d) 17 9.
		98	Proof. apply progress_evstep, T6. Qed.
		100	Lemma T8' n b d:
		101	Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.
		102	Proof. apply progress_evstep, T8. Qed.
		104	(** S applied k times. *)
		105	Lemma S_iter k: forall n a b c d,
		106	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).
96	Proof.	107	Proof.
97	follow Incs1.
		108	induction k; intros.
98	follow (Ov1 (1+a) a (n*4+b) rs).
		109	- finish.
99	follow Incs2.
		110	- follow (S_step' n (4*k+a) b c d).
		111	follow (IHk (24+n) a (2+b) c (2+d)).
100	finish.	112	finish.
101	Qed.	113	Qed.
103	Lemma Ov2_0 a b c d e ls:
		115	( The double cycle (write-up 4)
104	S2 a (1+b) c d 0 (e::ls) -->*
		117	Ev N X = Even(2N+1, 8X+52), where Even(n,x) = K(n, x, (x+76)/2, 35, 18).
105	S3 (1+a) b [2+e;2+d2;c2] (T ls).
		118	DC: Even(n,x) -> Even(n+12x+808, x+32) by S^((x-4)/8), TE, S^((x-52)/8), TO. *)
		119	Definition Ev N X := Kr N (4X+26) (2X+32) 17 9.
		121	Lemma prog_eq c1 c2 c1' c2':
		122	c1 -->+ c2 -> c1 = c1' -> c2 = c2' -> c1' -->+ c2'.
		123	Proof. intros H E1 E2. subst. exact H. Qed.
		125	Lemma DC N X:
		126	Ev N X -->+ Ev (48*X+716+N) (4+X).
106	Proof.	127	Proof.
107	es' a b c d e & (RC (T ls)).
		128	unfold Ev.
		129	follow (S_iter (X+6) N 1 (2*X+29) 14 8).
		130	follow (TE' (24(X+6)+N) (4X) (2*X+11)).
		131	follow (S_iter X (278+(24(X+6)+N)) 0 38 (2X+43) 8).
		132	eapply prog_eq.
		133	1: apply (TO (24X+(278+(24(X+6)+N))) (2X) (2X+28) (2*X)).
		134	all: lia_refl.
108	Qed.	135	Qed.
110	Lemma Ov2_1 a b c d e f ls:
		137	( Opening (write-up 5)
111	S2 a (1+b) c d 1 (1+e2::f::ls) -->
		139	4,097,897 steps from the blank tape to K(1959,34,68,45,18), then 20 macro steps
112	S3 (2+a) b [f;e2;O;1+d2;2+c*2] (T ls).
		140	to Even(12863,212) = Ev 6431 20.
		142	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
		144	busycoq's list configurations (cconfig_step); cc_steps' nests two counters as
		145	multistep_c' does in verify/Bouncer_v3.v. *)
		146	Fixpoint cc_steps (n:nat) (x:cconfig) : option cconfig :=
		147	match n with
		148	\| O => Some x
		149	\| S n0 =>
		150	match cconfig_step tm x with
		151	\| Some x0 => cc_steps n0 x0
		152	\| None => None
		153	end
		154	end.
		156	Lemma cc_steps_spec n x y:
		157	cc_steps n x = Some y -> cconfig_to_config x -->* cconfig_to_config y.
113	Proof.	158	Proof.
114	es' a b c d e f & (RC (T ls)).
		159	gen x.
		160	induction n; cbn[cc_steps]; intros x H.
		161	- inverts H. apply evstep_refl.
		162	- pose proof (cconfig_step_spec tm x) as HE.
		163	destruct (cconfig_step tm x) as [x0\|]. 2: congruence.
		164	eapply evstep_step; eauto.
115	Qed.	165	Qed.
117	Lemma Ov2_2 a b c d e ls:
		167	Fixpoint cc_steps' (n1 n2 n3:nat) (x:cconfig) : option cconfig :=
118	S2 a (1+b) c d 2 (e::ls) -->*
		168	match n1 with
119	S3 (2+a) b [2+e;3+d2;2+c2] (T ls).
		169	\| O => cc_steps n3 x
		170	\| S n1 =>
		171	match cc_steps n2 x with
		172	\| Some x0 => cc_steps' n1 n2 n3 x0
		173	\| None => None
		174	end
		175	end.
		177	Lemma cc_steps'_spec n1 n2 n3 x y:
		178	cc_steps' n1 n2 n3 x = Some y -> cconfig_to_config x -->* cconfig_to_config y.
120	Proof.	179	Proof.
121	es' a b c d e & (RC (T ls)).
		180	gen x.
		181	induction n1; cbn[cc_steps']; intros x H.
		182	- exact (cc_steps_spec _ _ _ H).
		183	- destruct (cc_steps n2 x) as [x0\|] eqn:E. 2: congruence.
		184	eapply evstep_trans.
		185	+ exact (cc_steps_spec _ _ _ E).
		186	+ apply IHn1, H.
122	Qed.	187	Qed.
124	Lemma Ov2_3 a b c d e f ls:
		189	(** Run-length words: rl [(z1,o1); (z2,o2); ...] = 0^z1 1^o1 0^z2 1^o2 ... *)
125	S2 a (1+b) c d 3 (1+e2::f::ls) -->
		190	Fixpoint rl (xs : list (nat*nat)) : list sym :=
126	S3 (3+a) b [f;e2;O;2+d2;4+c*2] (T ls).
		191	match xs with
		192	\| [] => []
		193	\| (z,o)::t => [0]^^z ++ [1]^^o ++ rl t
		194	end.
		196	(** Left records: F reads the leftmost visited cell (a 0), and the word right of it. *)
		197	Definition LR (xs : list (natnat)) : Q tape := cconfig_to_config ([], rl xs, 0, F).
		199	Definition Kr_list n a b c d : list sym :=
		200	G ++ [1] ++ [1;1]^^n ++ [0] ++ [1;1]^^a ++ [0;1;1;0] ++ [1;1]^^b
		201	++ [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
		202	++ [0;1;1;0;0;1;1;0;1;1;1].
		204	Lemma Kr_cc n a b c d:
		205	Kr n a b c d = cconfig_to_config ([], Kr_list n a b c d, 0, F).
127	Proof.	206	Proof.
128	es' a b c d e f & (RC (T ls)).
		207	unfold Kr, Kr_list, cconfig_to_config.
		208	cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.
129	Qed.	209	Qed.
131	Lemma S3_1 a b c d ls rs:
		211	(** Left record at step 694,884. *)
132	S3 a b (2+d::ls) ((true,c)::rs) -->+
		212	Definition W1 : list (nat*nat) :=
133	S4 a b (d::ls) ((false,c)::rs).
		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.
		215	(** Left record at step 1,397,500. *)
		216	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.
		219	(** Left record at step 2,099,620. *)
		220	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.
		223	(** Left record at step 2,790,296. *)
		224	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.
		227	(** Left record at step 3,493,040. *)
		228	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.
		231	Lemma init1:
		232	c0 -->* LR W1.
134	Proof.	233	Proof.
135	uf; es.
		234	change c0 with (cconfig_to_config ([], [], 0, A)).
		235	unfold LR.
		236	apply (cc_steps'_spec 694 1000 884).
		237	vm_compute.
		238	reflexivity.
136	Qed.	239	Qed.
138	Lemma S3_0 a b c ls rs:
		241	Lemma init2:
139	S3 a b ls ((false,2+c)::rs) -->*
		242	LR W1 -->* LR W2.
140	S3 a b (c::ls) rs.
141	Proof.	243	Proof.
142	uf; es.
		244	unfold LR.
		245	apply (cc_steps'_spec 702 1000 616).
		246	vm_compute.
		247	reflexivity.
143	Qed.	248	Qed.
145	Lemma S3_1_0 a b c ls rs:
		250	Lemma init3:
146	S3 a b (O::ls) ((true,c)::rs) -->+
		251	LR W2 -->* LR W3.
147	S4 a b ls ((false,O)::(false,c)::rs).
148	Proof.	252	Proof.
149	uf; es.
		253	unfold LR.
		254	apply (cc_steps'_spec 702 1000 120).
		255	vm_compute.
		256	reflexivity.
150	Qed.	257	Qed.
152	Lemma S3_0_0_0 a b c d e ls rs:
		259	Lemma init4:
153	S3 a b (d2::e::ls) ((false,O)::(false,1+c)::rs) -->
		260	LR W3 -->* LR W4.
154	S3 a b (c+d*2::2+e::ls) rs.
155	Proof.	261	Proof.
156	uf; es.
		262	unfold LR.
		263	apply (cc_steps'_spec 690 1000 676).
		264	vm_compute.
		265	reflexivity.
157	Qed.	266	Qed.
159	Lemma S3_0_0_1 a b c d ls rs:
		268	Lemma init5:
160	S3 a b (1+d2::ls) ((false,O)::(false,1+c)::rs) -->
		269	LR W4 -->* LR W5.
161	S4 a b ls ((false,3+d*2+c)::rs).
162	Proof.	270	Proof.
163	uf; es.
		271	unfold LR.
		272	apply (cc_steps'_spec 702 1000 744).
		273	vm_compute.
		274	reflexivity.
164	Qed.	275	Qed.
166	Lemma S4_0 a b c ls rs:
		277	Lemma init6:
167	S4 a b (c2::ls) rs -->
		278	LR W5 -->* Kr 979 17 34 22 9.
168	S4 a b ls ((false,2+c*2)::rs).
169	Proof.	279	Proof.
170	uf; es.
		280	unfold LR.
		281	rewrite Kr_cc.
		282	apply (cc_steps'_spec 604 1000 857).
		283	vm_compute.
		284	reflexivity.
171	Qed.	285	Qed.
173	Lemma S4_1 a b c d ls rs:
		287	Lemma init:
174	S4 a b (1+c2::d::ls) rs -->
		288	c0 -->* Kr 979 17 34 22 9.
175	S3 a b (1+c*2::2+d::ls) rs.
176	Proof.	289	Proof.
177	uf; es.
		290	follow init1.
		291	follow init2.
		292	follow init3.
		293	follow init4.
		294	follow init5.
		295	apply init6.
178	Qed.	296	Qed.
180	Lemma S4_O a b rs:
		298	Lemma opening:
181	S4 a b [] rs -->*
		299	Kr 979 17 34 22 9 -->* Ev 6431 20.
182	S3 (1+a) b [] rs.
183	Proof.	300	Proof.
184	uf; es.
		301	unfold Ev.
185	Qed.
		302	follow (S_iter 4 979 0 31 19 8).
187	Lemma S3_rh a b c ls:
		303	follow (TO' 1075 1 4 8).
188	S3 a b (1+c::ls) [] -->+
		304	follow (S_iter 4 1369 2 45 14 8).
189	S4 a b (c::ls) [].
		305	follow (T6' 1465 15 0 8).
190	Proof.
		306	follow (S_iter 6 1761 3 45 14 8).
191	uf; es.
		307	follow (T8' 1905 16 11).
192	Qed.
		308	follow (S_iter 5 2175 2 40 41 8).
194	Lemma S3_rh_0 a b c ls:
		309	follow (T6' 2295 12 27 10).
195	S3 a b (O::c::ls) [] -->+
		310	follow (S_iter 12 2591 3 47 14 8).
196	S5 a b ls [3+c].
		311	follow (T8' 2879 30 23).
197	Proof.
		312	follow (S_iter 9 3149 0 40 53 8).
198	uf; es.
		313	follow (TO' 3365 20 38 18).
199	Qed.
		314	follow (S_iter 17 3659 3 55 14 8).
201	Lemma S5_S a b c ls rs:
		315	follow (T8' 4067 48 33).
202	S5 a b (c::ls) (rs) -->+
		316	follow (S_iter 13 4337 2 40 63 8).
203	S5 a b ls ((c::rs)).
		317	follow (T6' 4649 28 49 26).
204	Proof.
		318	follow (S_iter 22 4945 1 63 14 8).
205	uf; es.
		319	follow (TE' 5473 66 43).
206	Qed.
		320	follow (S_iter 16 5751 2 38 75 8).
208	Lemma S5_O a b c rs:
		321	follow (T6' 6135 32 61 32).
209	S5 (1+a) b [] ((1+c::rs)) -->+
210	S1 0 1 a (1+b) ((c::rs)).
⋯ 13 template-only lines (template 211–224), not in ours
225	follow100 S3_rh.
226	follow S4_1.
227	finish.	322	finish.
228	Qed.
230	Fixpoint mul2 ls :=
⋯ 766 template-only lines (template 231–1030), not in ours
1031	}
1032	}
1033	Qed.	323	Qed.
1035	Lemma nonhalt: ~halts tm c0.	325	Lemma nonhalt: ~halts tm c0.
1036	Proof.	326	Proof.
1037	eapply multistep_nonhalt with (c':=to_config (cfg3 _ _ _ _)).
		327	eapply multistep_nonhalt.
1038	1:{
		328	1: { follow init. apply opening. }
1039	follow init.
		329	apply (progress_nonhalt_simple tm (nat*nat) (fun p => Ev (fst p) (snd p)) (6431,20)).
1040	follow (Incs12 42 0 7).
		330	intros [N X].
1041	follow Ov2_0.
		331	exists (48*X+716+N, 4+X).
1042	epose proof (S3T_3 _ _ 9) as I1.
		332	apply DC.
1043	follow100 I1; clear I1; cbn[mul2 app].
1044	epose proof (S3T_2 _ _ 4 _ _ _ []) as I1.
⋯ 14 template-only lines (template 1045–1058), not in ours
1059	}
1060	exact BigStep.
1061	Qed.	333	Qed.
		335	(*
		336	1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (only D0 undefined; D is entered only by A1 = 1LD)
		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)
		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
		340	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)
		343	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
		345	k-fold: C> 1^(2k) --> (10)^k C> (2k steps); 0 (10)^k B> 000 --> 0 B> 000 1^(2k) (12k steps)
		347	rule from to domain steps trips
		348	S K(n,a,b,c,d) -> K(n+48,a-8,b+4,c,d+4) n odd, a even >= 10, b even >= 6, c odd >= 7, d even >= 2 84n+84a+77b+70c+63d+13628 12
		349	TE K(n,4,b,35,d) -> K(n+556,b-86,82,d+51,18) n odd, b even >= 88, d even >= 20 966n+952b+812d+455332 138
		350	TO K(n,2,b,c,d) -> K(n+588,b+c-91,d+62,35,18) n odd, b even >= 82, c odd >= 37, d even >= 18 1029n+1001b+987c+882d+458476 147
		351	T6 K(n,6,b,c,d) -> K(n+592,b+c-91,d+62,35,18) n odd, b even >= 82, c odd >= 35, d even >= 18 1029n+1008b+987c+882d+462814 147
		352	T8 K(n,8,b,35,d) -> K(n+540,b-74,86,d+47,18) n odd, b even >= 88, d even >= 20 945n+938b+784d+446893 135
		354	DC Even(n,x) --S^((x-4)/8)--> K(.,4,x+36,35,(x+32)/2) --TE--> K(.,x-50,82,(x+134)/2,18)
		355	--S^((x-52)/8)--> K(.,2,(x+112)/2,(x+134)/2,(x-16)/2) --TO--> Even(n+12x+808, x+32)
		356	n odd, x = 4 mod 8, x >= 52; 3x+201 trips
		357	(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)-->
		360	Even(12863,212) at step 153,126,993; then DC forever (x = 212, 244, 276, ...)
		361	*)

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

39 items in 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v (361 lines): 25 Lemma, 11 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 "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").	L29	identicalexcept the TM string
2	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].	L36	new
3	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.	L39	new
4	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).	L50	new
5	Lemma	`TE`	Lemma TE n b d: Kr n 2 (44+b) 17 (10+d) -->+ Kr (278+n) (1+b) 41 (35+d) 9.	L57	new
6	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.	L64	new
7	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.	L71	new
8	Lemma	`T8`	Lemma T8 n b d: Kr n 4 (44+b) 17 (10+d) -->+ Kr (270+n) (7+b) 43 (33+d) 9.	L78	new
9	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).	L84	new
10	Lemma	`TE'`	Lemma TE' n b d: Kr n 2 (44+b) 17 (10+d) -->* Kr (278+n) (1+b) 41 (35+d) 9.	L88	new
11	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.	L92	new
12	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.	L96	new
13	Lemma	`T8'`	Lemma T8' n b d: Kr n 4 (44+b) 17 (10+d) -->* Kr (270+n) (7+b) 43 (33+d) 9.	L100	new
14	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).	L105	new
15	Definition	`Ev`	Definition Ev N X := Kr N (4X+26) (2X+32) 17 9.	L119	new
16	Lemma	`prog_eq`	Lemma prog_eq c1 c2 c1' c2': c1 -->+ c2 -> c1 = c1' -> c2 = c2' -> c1' -->+ c2'.	L121	new
17	Lemma	`DC`	Lemma DC N X: Ev N X -->+ Ev (48*X+716+N) (4+X).	L125	new
18	Fixpoint	`cc_steps`	Fixpoint cc_steps (n:nat) (x:cconfig) : option cconfig := match n with \| O => Some x \| S n0 => match cconfig_step tm x with \| Some x0 => cc_steps n0 x0 … +3 lines	L146	new
19	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.	L156	new
20	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	L167	new
21	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.	L177	new
22	Fixpoint	`rl`	Fixpoint rl (xs : list (nat*nat)) : list sym := match xs with \| [] => [] \| (z,o)::t => [0]^^z ++ [1]^^o ++ rl t end.	L190	new
23	Definition	`LR`	Definition LR (xs : list (natnat)) : Q tape := cconfig_to_config ([], rl xs, 0, F).	L197	new
24	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].	L199	new
25	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).	L204	new
26	Definition	`W1`	Definition W1 : list (nat*nat) := ([(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.	L212	new
27	Definition	`W2`	Definition W2 : list (nat*nat) := ([(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.	L216	new
28	Definition	`W3`	Definition W3 : list (nat*nat) := ([(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.	L220	new
29	Definition	`W4`	Definition W4 : list (nat*nat) := ([(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.	L224	new
30	Definition	`W5`	Definition W5 : list (nat*nat) := ([(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.	L228	new
31	Lemma	`init1`	Lemma init1: c0 -->* LR W1.	L231	new
32	Lemma	`init2`	Lemma init2: LR W1 -->* LR W2.	L241	new
33	Lemma	`init3`	Lemma init3: LR W2 -->* LR W3.	L250	new
34	Lemma	`init4`	Lemma init4: LR W3 -->* LR W4.	L259	new
35	Lemma	`init5`	Lemma init5: LR W4 -->* LR W5.	L268	new
36	Lemma	`init6`	Lemma init6: LR W5 -->* Kr 979 17 34 22 9.	L277	new
37	Lemma	`init`	Lemma init: c0 -->* Kr 979 17 34 22 9.	L287	adapted
38	Lemma	`opening`	Lemma opening: Kr 979 17 34 22 9 -->* Ev 6431 20.	L298	new
39	Lemma	`nonhalt`	Lemma nonhalt: ~halts tm c0.	L325	new

4What a maintainer readsCheck: the rule table below is what the .v proves, and proof.md / README read cleanly for a maintainer.

submission/proof.md · informal proof (submitted copy)
submission/README.md · the package README
submission/discord.md · Discord draft (not posted)
proof.md (working copy) · differs from the submitted copy

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

1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF        (only D0 undefined; D is entered only by A1 = 1LD)

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)
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
Even(n,x)    = K(n, x, (x+76)/2, 35, 18)

R1   C> 1 1         --> 1 0 C>             2 steps    C1 E1
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
     k-fold:  C> 1^(2k) --> (10)^k C>   (2k steps);   0 (10)^k B> 000 --> 0 B> 000 1^(2k)   (12k steps)

rule  from            to                            domain                                          steps                          trips
S     K(n,a,b,c,d) -> K(n+48,a-8,b+4,c,d+4)         n odd, a even >= 10, b even >= 6, c odd >= 7, d even >= 2   84n+84a+77b+70c+63d+13628   12
TE    K(n,4,b,35,d) -> K(n+556,b-86,82,d+51,18)     n odd, b even >= 88, d even >= 20                         966n+952b+812d+455332        138
TO    K(n,2,b,c,d) -> K(n+588,b+c-91,d+62,35,18)    n odd, b even >= 82, c odd >= 37, d even >= 18            1029n+1001b+987c+882d+458476 147
T6    K(n,6,b,c,d) -> K(n+592,b+c-91,d+62,35,18)    n odd, b even >= 82, c odd >= 35, d even >= 18            1029n+1008b+987c+882d+462814 147
T8    K(n,8,b,35,d) -> K(n+540,b-74,86,d+47,18)     n odd, b even >= 88, d even >= 20                         945n+938b+784d+446893        135

DC    Even(n,x) --S^((x-4)/8)--> K(.,4,x+36,35,(x+32)/2) --TE--> K(.,x-50,82,(x+134)/2,18)
                --S^((x-52)/8)--> K(.,2,(x+112)/2,(x+134)/2,(x-16)/2) --TO--> Even(n+12x+808, x+32)
      n odd, x = 4 mod 8, x >= 52; 3x+201 trips

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)-->
      Even(12863,212) at step 153,126,993;  then DC forever (x = 212, 244, 276, ...)

5FamilyCheck: 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	this kill
W5-8b kill 28	`1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF`	✓Killed: never halts	parent link; = W5-8's table mirrored, run from state C; named in W5-8b's .v header; named in W5-8b's proof.md; named in W5-8b's notes.md · review · same machine as this kill? (same table mirrored, started in W5-8's C; different orbit; tables, pictures and numbers side by side)
W5-8c kill 29	`1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA`	✓Killed: never halts	parent link; = W5-8's table, run from state E; named in W5-8c's .v header; named in W5-8c's proof.md; named in W5-8c's notes.md · review · same machine as this kill? (same table, started in W5-8's E; different orbit; tables, pictures and numbers side by side)

6ChecklistCheck: every ✓ is computed; the two ○ are yours to decide; an amber ! is an optional check that did not finish.

✓
Machine string exact
the .v literal == holdout list line 228 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.9 s
✓
.v hash matches the checked hash
.v = checked sha256 beef54a54f62…; submission/ copy = checked sha256 beef54a54f62…
✓
No repo-local paths in the .v
comments name no path of ours (vendor/, machines/, tools/, rocq/, scripts/, reports/, atlas/, data/, journal/, /home/); busycoq's own verify/X.v is fine: none in the .v or the submission/ copy
✓
Public write-up is clean
tools/writeup_lint.py on submission/proof.md: 0 error(s)
○
proof.md reviewed by Dennis (Checkpoint B)
no Checkpoint B note from Dennis found
- notes.md L80: 2026-10-13: proof.md complete, status OPEN (Checkpoint B pending, non-blocking). check_proof.py checks every claim.
- proof.md L771: ## 10. Checkpoint B (Dennis)
- proof.md L783: - Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
- proof.md L794: - Open: Checkpoint B (non-blocking); formalization (§8).
○
Family posted together?
2 other kill(s) in the family: W5-8b, W5-8c; the Discord draft names 0 of them

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

Files

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

name	size	changed
notes.md ↓	10 KB	2026-10-13 05:28
proof.md ↓	66 KB	2026-10-13 04:57
how_proved.md ↓	1.7 KB	2026-10-14 10:51
status.json ↓	3.0 KB	2026-10-16 10:28
observe.json ↓	14 KB	2026-10-13 03:36
1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v ↓	12 KB	2026-10-13 05:16
img/	4 items	2026-10-13 03:34
rocq/	16 items	2026-10-13 05:17
scripts/	13 items	2026-10-13 03:59
submission/	6 items	2026-10-15 15:49
work/	17 items	2026-10-13 04:05
check_proof.py ↓	43 KB	2026-10-13 04:50

status.json in full

{
 "tm": "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF",
 "status": "KILLED_NONHALT",
 "stage": "done",
 "updated": "2026-10-13",
 "reason": "check_kill PASS, independently re-verified",
 "label": "W5-8",
 "confidence": "high",
 "siblings": [
  "1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF",
  "1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA"
 ],
 "family_note": "Same table (canon over all 6 starts, renaming + mirror): 740 line 418 = start C of this table, mirrored (renaming 214->418: C->A, A->B, B->C, D,E,F fixed); 740 line 636 = start E, not mirrored (E->A, A->E, B->C, C->D, D->F, F->B). Starts B and F reach the start-C run after 1-2 steps, so they are not separate holdouts. Running this table from C reaches Even(12857, 212) at step 153,013,640; from E it reaches Even(13299, 220) at step 163,638,058. One proof of S, TE, TO and the double cycle covers all three. Each list entry is a singleton group in 2026-10-07_eqv_1590.txt.",
 "checks": {
  "byte_exact_740": "line 214",
  "claims": "none: data/discord hit is mxdys's UBRRBA_TODO list (an acceleration to-do list, not a claim); sheet rows give only the class 'Bouncer + Chaotic Edge'",
  "upstream_9cf9e88": "not proved: no file in the 9cf9e88 verify tree contains any of the three list strings, or the table's canonical forms",
  "check_proof": "work/check_proof_seed1.log, work/check_proof_seed2.log, work/check_proof_full_seed1.log (196/196 each)"
 },
 "outcome": "never halts (check_kill PASS, independently re-verified; informal proof complete, skeptic round 1 passed)",
 "next": "post the Discord draft (submission/discord.md, not posted; fill in <LINK>, search #bb6 first); siblings 740 lines 418/636 need only their own openings + Perm/flip (proof.md 7.3)",
 "proof_md": "proof.md",
 "check": "check_proof.py 196/196 PASS: seed 1 and seed 2 default (55 s each), seed 1 --full (206 s); after the last prose pass DOC+COL re-run 69/69 PASS. Logs work/check_proof_seed1.log, work/check_proof_seed2.log, work/check_proof_full_seed1.log",
 "open_lemmas": [],
 "template": "verify/TranslatedBellv5.v Module TM1 (es' block macro rules + ind/follow); progress_nonhalt_simple as Bouncer_v2.v TM1; nested step counters as Bouncer_v3.v multistep_c'",
 "kill": {
  "file": "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v",
  "sha256": "beef54a54f6272e70cf2c6a90bd81a899416bd572ecc84431a685ed38cbacf48",
  "lines": 361,
  "check_kill": "PASS (fresh run 2026-10-13T12:23:55Z: compile 6.6 s native, coqchk pass 44.9 s, 0 assumptions; also rocq/check_kill_final.log (round 1) and the independent auditor run 2026-10-13T12:20:42Z, same sha256)",
  "submission": "submission/",
  "discord": "submission/discord.md, not posted (fill in <LINK>)"
 },
 "pr": "https://github.com/ccz181078/busycoq/pull/27",
 "pr_state": "merged",
 "pr_file": "verify/M_1RB1LD_0RC1RC_1LA1RE_HHH1LE_1RF0RC_0RB0LF.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, observe.json (the card), the kill files (tools/killreview.py) and the dashboard records · rebuild: python3 -B tools/card.py 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (the kill review: python3 -B tools/killreview.py 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF, which also renders a derived kill's same-machine pictures)