#2 kill review

#2 · kill review1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- Bell eats counter (sheet Results row 1035) · template SOMDCv6.v TM7, which differs only in A1

✓ Killed: never halts Lemma nonhalt: ~halts tm c0. · check_kill PASS 17/17, 0 axioms · check_kill.txt 11:54 PDT · re-run for this page 12:00 PDT (compile 3.82 s, coqchk 1.06 s) · not posted · no Checkpoint B notes on file

1Confirm the processA · timeline: what ran, in what order, what each stage found.

2Glance at the artifactsB · artifact table: every file, what it is, who reads it.

3Read deeperC · pictures first, then D · proof.md and E · the .v with margin notes.

4JudgeF · checklist: the checks a maintainer runs, and what they may push back on.

Correct vs reviewable. The kill rests only on the .v: it compiles against unmodified busycoq, states ~halts tm c0 for the exact holdout string, and uses no axioms (check_kill checks all of this; see F). The informal proof, the pictures and the simulations explain it but are not part of that guarantee. Reviewable is a separate question: can a maintainer read the file and see why it works? Section F lists what may come up.

AProcess: what we did

Targeting picked #2 on Oct 9. Everything else ran overnight, between 00:06 and 04:51 on Oct 10 (PDT). The proof stages overlapped: Rocq prep and formalization started while proof.md was still a draft (Fig A).

Fig AWhen each stage ran

agent work (bar = start to end) Dennis check_kill PASS on the final .v

TimesPDT, 2026-10-10; 1 minute = 5 px in both parts; 02:30–03:20 omitted (no #2 proof work)Sourceworkflow records in ~/.claude/projects/-home-dennis/…/workflows (agent first and last message), session messages (Dennis), check_kill timestamps (UTC 11:45:36 formalizer; 11:46:58 audit, saved as check_kill_audit.json; 11:48:20 bundle; 11:51:12 orchestrator)

Stage	When	What happened	Key finding	Artifacts
Targeting	Oct 9	Ranked #2 of 20 pilots: it differs only in A1 from two machines mxdys proved in SOMDCv6.v (TM7 `…1RB0RC…`, TM8 `…1RB0LC…`). Risk "medium": mxdys stopped short of these two, so A1 probably breaks his rule set.	Closest template: SOMDCv6.v `Module TM7` (line 1626).	targeting.md §4.2 row 2
Observe	00:06–01:36	Simulated to 1e9 steps and fitted rules. The tape at each sweep boundary is `S(r) = 0^∞ 11 D> r 0^∞` over digits L=110, 0=000, 1=100.	Our sweep map = TM7's plus "+1 to the rest of the word at each L entered". Fits 208/208 sweeps; TM7's map alone fits 1/208. Confidence high.	observe.json notes.md machine page (index.html)
Checkpoint A	01:22 → 03:31	Dennis objected to the first picture pair: "it seems like ours does the “walking” and TM7 does the extra bouncing/zigzagging". A skeptic re-checked with its own C simulator (all 156,622 A1 events to 1e9), then the pictures were redone as aligned pairs from the same start.	Mechanism confirmed, 11 corrections. Among them: the caption "TM7 eats silently" was false, and the old pair did not "show the whole difference" (same step window, different phases). One case was missing: a drain pass entering an L also fires +1 (115/208 sweeps; without it the map fits 95/208). Dennis then answered Q1–Q3 yes and spotted the extra 1 after the first eat.	notes.md § Checkpoint A eat_pair.png sweep_pair.png
Informal proof	03:33–04:25	Wrote proof.md by extending TM7: Inc premise in the two L clauses, then TM7's domain argument.	TM7's domain lemma did not carry over: the domain is not closed (170 words of ≤ 11 digits fail). Fix: two zero-pass end clauses Z0/Z1 and a generalized domain lemma RIncs_nxt' with j pending +1s. All simulation checks pass.	proof.md check_proof.py
Rocq prep	03:33–04:12 (parallel)	Un-wrapped TM7 into a standalone file and swapped in our string.	TM7 standalone compiles in 3.8 s and passes check_kill with TM7's string. With our string only the two L bullets of RIncs_spec break; the new segment facts are proved by `esx`. Also found the domain counterexample `LLLL10LL1L1`; its own fix (a 3-sweep invariant, §3.5) was not used.	rocq-plan.md TM7_toplevel.v probe_segments_2.v
Formalization	03:55–04:46 (1 round of max 4)	Started from TM7 while proof.md was being written (told to re-read it as it changed).	proof.md's §3.3 case table matched the Coq cases one to one. check_kill PASS at 04:45:36.	rocq/log.md the .v
Skeptic 2 + revise	04:25–04:47	Adversarial review of proof.md as a busycoq maintainer would read it, then a revision.	Sound; 5 minor gaps (wrong clause counts, understated formal status, "verbatim" claim, A1 wording, an unlisted functionality assumption). All fixed; listed in proof.md's Review log.	proof.md § Review log
Audit + re-runs	04:46–04:51	An independent agent re-ran check_kill (--json), checked the string against the 778 list and read the .v end to end; the bundle step and the orchestrator each re-ran check_kill.	17/17 checks pass; string at line 301 of the 778 list; nothing suspicious. In all 4 PASS runs on sha256 `3b29083b…` (formalizer, audit, bundle, orchestrator); notes.md and the ledger each count 3 of them. Later the same day a comment-only header edit took out the repo-local paths (code unchanged); the file is now sha256 `e434537e…`, and check_kill.txt and the page re-run are fresh PASS runs on it.	notes.md § Kill overnight-ledger.md
Bundle	04:47–04:51	Made `submission/`.	The .v (same sha256), proof.md with its status lines updated, check_kill.txt (fresh run 04:48:20), README, and a Discord draft of 1,371 characters counting the `<LINK>` placeholder (1,365 without it). Not posted.	submission/ README discord.md

BArtifacts

Every file that matters for #2, grouped by stage. "Reader" is who it is for. The green row is the kill itself.

Artifact	What it is	Why it matters	Reader
Picked and observed
reports/targeting.md	Pilot memo; §4.2 row 2 is #2.	Why this machine: one transition from a proved template.	Dennis
observe.json	Observer's structured record: summary, mechanism, figure labels, 40 history rows, rules.	Feeds the card and the explorer's machine list.	tooling
notes.md	Running log: observation, candidate rules, Checkpoint A answers, kill record.	The narrative of record. Rendered: notes.html.	Dennisagents
check_rules.py	Observe-stage rule checks (sweep map vs the real machine).	Source of 208/208 and the L-entry checks.	agents
machine page (index.html)	The Checkpoint A card, Figs 1–5.	Shows Q1–Q3 with your answers.	Dennis
img/eat_pair.png	Card Fig 1: one eating pass, ours vs TM7, same start S(L⁴1L1), every step.	Shows the +1 passes (blue) are the only difference while eating.	Dennis
img/sweep_pair.png	Card Fig 2: one full sweep each.	Shows the drain-enters-L case (pass 5).	Dennis
img/sweep_ours.html · sweep_tm7.html	Zoomable viewers of those two sweeps.	Hover for step, state and cell.	Dennis
img/default_site_1e4.png, records_1e9.png, blaze_1e7.png	Card Figs 3–5: site view, records to 1e9, Blaze 1e7.	Context only; not used by the proof.	Dennis
img/viewer.html	bbchallenge-style viewer of the first 10,000 steps (card Fig 3).	Context only.	Dennis
scripts/compare_tm7.py	Regenerates the aligned pictures and their event counts.	Reproducibility of Figs 1–2.	agents
explorer preset p2-vs-tm7	Interactive: #2 and TM7 from S(L⁴1L1); dashed line = first difference.	Spot-check any step yourself.	Dennis
Proof (informal)
proof.md → rendered	The informal proof (working copy: raw; submission copy: raw).	What a maintainer reads to understand the .v. §3.3 is the new idea.	maintainerDennis
check_proof.py	Simulation checks for every claim of proof.md, plus a partial Rocq compile (--rocq).	Evidence, not proof. Default run: ALL PASS in 7 s (run for this page).	agents
Formal proof
rocq-plan.md	Template anatomy of TM7, what breaks, risks, size estimate.	Found that TM7's domain is not closed for #2. Its 3-sweep plan was superseded by proof.md's Z0/Z1 fix.	agents
rocq-scratch/TM7_toplevel.v	TM7 un-wrapped from its Module (261 lines).	Base of the diff; passes check_kill with TM7's string.	agents
rocq-scratch/probe_segments_2.v	8 probe lemmas for the new pass segments.	First proof that the +1 pass is an ordinary h visit.	agents
rocq-scratch/py/*.py	Domain experiments: rincs, domain_facts, joint, margin, margin_cond.	Ruled out "safety margin" invariants.	agents
rocq/work.v · rocq/compile.sh	Formalizer's work file and compile wrapper.	work.v = the kill file minus its header and rule-table comments, plus one unused Ltac (nxt_inc).	agents
rocq/log.md	Formalization log: what compiled, pitfalls, the kill run.	Round 1 was enough.	agents
1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v → annotated	The kill. 599 lines, top-level `Lemma nonhalt: ~halts tm c0.` (raw: .v).	The only artifact the kill rests on.	maintainerDennistooling
atlas/rocq-notes.md	Tactics log; sections "SOMDCv6 TM7 template (for #2)" and "Machine #2 … formalization round 1".	Lessons for the next variant (zero-cost representation clauses).	agents
vendor/busycoq/verify/SOMDCv6.v	The template: TM7 at lines 1626–1871 (rendered: tm7.html).	What the maintainer will compare against.	maintainer
compare.html	Our .v vs TM7 side by side: the three machines, similarity per item, full aligned diff, proof structure (built by compare/build.py).	How much of TM7 we kept, item by item. Its counts use its own line matching (difflib, blank lines ignored), so they differ from the GNU diff counts on this page.	Dennismaintainer
Verification and packaging
tools/check_kill.sh	The kill gate: 17 checks (pin, string, statement, forbidden words, assumptions, coqchk, …).	Encodes the kill criteria in CLAUDE.md.	tooling
data/holdouts/2026-10-07_778.txt	The current holdout list; our string is line 301.	A kill counts only if the string is on it.	tooling
submission/	What you would post: the .v (same sha256), proof.md, check_kill.txt, README.md, discord.md.	Self-contained package.	Dennismaintainer
submission/check_kill.txt	Full check_kill output, run 11:54 PDT.	Attach or quote when posting.	maintainer
submission/discord.md	Draft post, 1,371 characters counting the `<LINK>` placeholder; replace it with the .v URL.	The post itself.	Dennis
status.json	`KILLED_NONHALT`, stage done.	Feeds the dashboards.	tooling
reports/overnight-ledger.md	One line per orchestrator action, with times.	Timeline source.	Dennis

CThe proof in pictures

Eight figures, in the order the proof uses them. Abstract figures are computed from the relation R by this page's build script; machine figures are simulations of the real table. Open in explorer: #2 vs TM7 from S(L⁴1L1) ↗

Fig 1The boundary configuration S(r)

At every sweep boundary the tape is a wall 11, the head in state D on the next cell, then the word r written in 3-cell digits, then blank. Busycoq calls it S' r.

0^∞

D▸

0^∞

wall

digit L

digit 0

digit 1

TapeS(L⁴ 1L1) = 0^∞ 11 D> 110 110 110 110 100 110 100 0^∞; constructed (the start of card Figs 1–2 and of the explorer preset); never visited from blankCells−2 … 20, head on cell 0Colorswhite = 1, black = 0; red outline + D▸ = head in state D about to read that cell; blue bar = L digit

Fig 2The +1 pass (Inc): what A1 = 0RF adds

An h pass (enter in B, leave in C) over a word adds 1 to it: read the 0/1 digits as a little-endian binary number, skip L. At A1 both machines write 0 and step right. TM7's next state C turns back at once (C0 = 0LC); ours goes to F (F0 = 0RB), which starts one such pass over everything to the right and comes back to exactly where TM7 is right after its A1 step. Inc is the relation, Inc_spec the machine fact.

before: 1 1 L 011L0= 1·1 + 1·2 + 0·4 = 3

after: 0 0 L 100L1= 0·1 + 0·2 + 1·4 = 4

Inc clause	proof.md	reads	writes
Inc_d1	I1	1	0 and carry into the rest
Inc_d0	I2	0	1, stop
Inc_ld	I3	L	L, keep going
Inc_nil	I4	end	1 (append)

Startconstructed: 1 B> 100 100 110 000 0^∞ (the 1 on the left is arbitrary; the pass never reads it)Rowsevery step, 0 … 19 (= 6j+1 with j = 3 digits before the first 0); label = step, state, rule just firedWindowcells −1 … 12, 1 cell = 15 pxColorswhite = 1, black = 0, red box = head; A1 never fires inside the pass

eat_pair — Fig 3The sweep relation R (busycoq `RIncs`): 12 clauses

clause	Coq name (line)	mode	count	reads	writes	then	vs TM7
X1	RIncs_hx_ld 72	hx (eater)	any k	L	L	eater, k+1, on rest + 1	adapted + Inc premise (TM7 line 1664)
X2	RIncs_hx_d0 81	hx (eater)	any k	0	L	eater, k+1	copied from TM7 same text
X3	RIncs_hx_d1 77	hx (eater)	any k	1	L	drain, k	copied from TM7 same text
C1	RIncs_h1_ld 85	h1 (drain)	k ≥ 1	L	L	eater, k, on rest + 1 (restart)	adapted + Inc premise (TM7 line 1676)
C2	RIncs_h1_d1 90	h1 (drain)	k ≥ 1	1	L	drain, k−1 (the 1 absorbs a pass)	copied from TM7 same text
C3	RIncs_h1_d0_0 94	h1 (drain)	k odd	0	0	drain, (k−1)/2	copied from TM7 same text
C4	RIncs_h1_d0_1 98	h1 (drain)	k even ≥ 2	0	1	drain, (k−2)/2	copied from TM7 same text
R0	RIncs_h1_rh_0 102	h1 (drain)	k = 0	end	1	done	copied from TM7 same text
R1	RIncs_h1_rh_1 105	h1 (drain)	k odd	end	0	drain, (k−1)/2, still at the end	copied from TM7 same text
R2	RIncs_h1_rh_2 109	h1 (drain)	k even ≥ 2	end	1	drain, (k−2)/2, still at the end	copied from TM7 same text
Z1	RIncs_h1_z1 113	h1 (drain)	k = 0	1 (last)	L	done: 1 100 0^∞ = 110 0^∞	new not in TM7
Z0	RIncs_h1_z0 116	h1 (drain)	k = 0	0 (last)	1	done: 1 000 0^∞ = 100 0^∞	new not in TM7

Fig 4R at work: one sweep from S(L⁴ 1L1), ours vs TM7

Each row applies one clause. Ours adds +1 to the rest at every L (X1, C1). After the first eat, ours' rest is 1L11 where TM7's is 1L1: that is the extra 1 you spotted at Checkpoint A. The drain pass that re-enters the L adds +1 again (11 → 001), so ours eats two more digits.

ours → S(L⁹ 111)

#	mode, k	reads	clause	writes	rest after (orange = changed by +1)
1	hx, 0	L	X1 +1	L	LLL0L01
2	hx, 1	L	X1 +1	L	LL1L01
3	hx, 2	L	X1 +1	L	L0L11
4	hx, 3	L	X1 +1	L	1L11
5	hx, 4	1	X3	L	L11
6	h1, 4	L	C1 +1	L	001
7	hx, 4	0	X2	L	01
8	hx, 5	0	X2	L	1
9	hx, 6	1	X3	L	—
10	h1, 6	end	R2	1	—
11	h1, 2	end	R2	1	—
12	h1, 0	end	R0	1	—

TM7 → S(L⁷ 101)

#	mode, k	reads	clause	writes	rest after (orange = changed by +1)
1	hx, 0	L	X1	L	LLL1L1
2	hx, 1	L	X1	L	LL1L1
3	hx, 2	L	X1	L	L1L1
4	hx, 3	L	X1	L	1L1
5	hx, 4	1	X3	L	L1
6	h1, 4	L	C1	L	1
7	hx, 4	1	X3	L	—
8	h1, 4	end	R2	1	—
9	h1, 1	end	R1	0	—
10	h1, 0	end	R0	1	—

Whatderivations of R(hx, 0, L⁴1L1, ·) for both relations (abstract, computed)Checkthe real machines agree: S(L⁴1L1) → S(L⁹ 111) in 421 steps (ours) and S(L⁷ 101) in 237 (TM7), simulated for this page; same as card Fig 2Colorsclause chips as in Fig 3; orange outline = digit changed by the +1

Fig 5Why Z0 and Z1: without them the domain is not closed

TM7's proof needs: if r can be swept, so can its output. With only the +1 change this fails. Z1 and Z0 add no machine behaviour: each says two spellings of the same tape are equal.

Z1: stray 1, then digit 1

stray

0^∞

= digit L

0^∞

Z0: stray 1, then digit 0

stray

0^∞

= digit 1

0^∞

rLLLL10LL1L1

sweep(r)LLLLL1LLLLLLL111

without Z0/Z1stuckdrain with 0 passes left at the last digit 1: no clause

with Z1LLLLLLLLLLLLLL011L

The real machine agrees: S(r) → S(sweep r) in 543 steps, then → S(L¹⁴ 011L) in 1,295 steps (simulated for this page). Over all words of ≤ 11 digits: without Z0/Z1, 71,865 words can be swept and 170 of them have an output that cannot; with Z0/Z1, 76,738 words can be swept and every output can be swept again (recomputed here; proof.md §3.3). Z0/Z1 were never used in the first 3,000 sweeps from blank (simulation, not proof; proof.md §7).

Leftcells of the two identities (z1_eq line 133, z0_eq line 138)Rightthe counterexample from rocq-plan.md §3.5 and proof.md §3.3Colorscells: white = 1, black = 0; chips: blue = L

Fig 6The domain lemma key, run on that example

key follows two sweeps at once: the first over r (count k), the second over the first's output (count q), one digit per row. The second sweep's +1s land on the first's output. Lemma A (RIncs_Inc) says that is the same as the first sweep run with j extra passes, so the pair is tracked by numbers alone. Inv says q is large enough; it holds on every row. Row 6 shows the j +1s at work: the first writes 1 but the second reads 0, because K = k+j = 9 is odd. At the end, End_x finishes the second sweep, and its last step needs Z1.

digit	first sweep: mode, k	reads	clause	writes	j	second sweep: mode, q	reads	clause	Inv(tp,k,j,tq,q)
1	hx, 0	L	X1	L	0	hx, 0	L	X1	✓
2	hx, 1	L	X1	L	1	hx, 1	L	X1	✓
3	hx, 2	L	X1	L	2	hx, 2	L	X1	✓
4	hx, 3	L	X1	L	3	hx, 3	L	X1	✓
5	hx, 4	1	X3	L	4	hx, 4	L	X1	✓
6	h1, 4	0	C4	1	5	hx, 5	0	X2	✓
7	h1, 1	L	C1	L	3	hx, 6	L	X1	✓
8	hx, 1	L	X1	L	4	hx, 7	L	X1	✓
9	hx, 2	0	X2	L	5	hx, 8	L	X1	✓
10	hx, 3	L	X1	L	6	hx, 9	L	X1	✓
11	hx, 4	0	X2	L	7	hx, 10	L	X1	✓
12	hx, 5	0	X2	L	8	hx, 11	L	X1	✓
13	hx, 6	1	X3	L	9	hx, 12	L	X1	✓
end	h1, 6	end	R2	…	10	hx, 13	10001	End_x: K = k+j = 16 ≤ 2q+2 = 28 ✓. The second sweep finishes: X3 C3 C4 C4 Z1 → writes L011L; the last step is Z1.

Whatkey's induction (one row per case, as in the Coq proof) on r = LLLL10LL1L1; first sweep R(hx,0,r,·), second R(hx,0,sweep r,·)Checkevery row asserts Inv and that R(tp, k+j, rest) equals what the second sweep reads (Lemma A)Colorsclause chips as in Fig 3; orange outline (second sweep's reads column) = digit the pending +1s changed, so it differs from what the first sweep wrote

Fig 7BigStep on the real machine: each sweep ends one cell further left

BigStep (TM7's text): if R(hx,0,r,r') then S(r) -->+ S(r'). The pass h' turns 1 D> r into <C r', then 3 steps (C1, D0, D0) rebuild the wall one cell to the left.

step 5: S(1)

0^∞

D▸

0^∞

wall

step 16: S(L1)

0^∞

D▸

0^∞

wall

step 91: S(LLL11)

0^∞

D▸

0^∞

wall

The wall rule at the end of the first sweep, steps 13–16:

Startblank tapeRowssteps 5, 16, 91 (the first three sweep boundaries); below: steps 13–16, every stepWindowcells −3 … 16 (top), −3 … 8 (bottom)Colorswhite = 1, black = 0, red = head; bars: grey = wall 11, blue = L digit

Fig 8How nonhalt is assembled (lines 560–575)

c0 (blank tape)

state A, all 0

→

start

c0 -->* S(L1) in 16 steps, by computation (esx), line 557

→

P(L1)

witness: R(hx,0,L1, LLL11), built by hand from X1 (with Inc), X2, X3, R2, R0, lines 566–569. LLL11 is the real step-91 word.

→

for every r with P(r)

BigStep: S(r) -->+ S(r') (one or more steps)

domain: P(r')

so the run never stops making progress

→

~halts tm c0

progress_nonhalt_cond (TM.v 632): ~halts from S(L1); multistep_nonhalt (TM.v 584): back to c0. Line 560.

Lemmasframework: multistep_nonhalt and progress_nonhalt_cond in vendor/busycoq/verify/TM.v; ours: start, BigStep, domainDifference from TM7TM7 starts at S(1) (step 5), builds the witness with repeat ec and calls RIncs_nxt inline

Dproof.md, rendered

Read it here: review/proof.html (the submission copy). Map of its sections to the .v:

§	title	what it says	formalized by
1	Families and notation	Digits, +1, S(r), the passes h and h', R.	Digits ld, d0, d1, Passes hR, hR', hL, h, h', RD, H, toRC, S', Inc
2	Rule table	Inc (I1–I4), R's 12 clauses, the machine-level pass rules, the worked example (Fig 4).	Inc, RIncs, Rule-table comment
3.1	Every clause is an exact run	Soundness of each clause; the new X1/C1 segments; Z0/Z1 as identities.	z1_eq, z0_eq, Inc_spec, seg_hx_ld, seg_h1_ld, RIncs_spec
3.2	Sweep	S(r) -->+ S(r') (Fig 7).	BigStep
3.3	The domain is closed	Why Z0/Z1 are needed (Fig 5); Lemma A, Total_1, End_1, End_x; the key lemma and its case table (Fig 6).	Inc_total, Inc_fun, RIncs_Inc, RIncs_nxt_1, End_1, End_x, Inversion helpers, Inv, key, domain
3.4	Progress	Each sweep is at least 4 steps.	(no lemma: follows from the others)
3.5	The halting transition F1	Never reached, since every rule is an exact run.	(no lemma: follows from the others)
4	Initial segment	Blank → S(1) in 5 steps (the .v starts at S(L1), step 16).	start
5	Conclusion	multistep_nonhalt + progress_nonhalt_cond (Fig 8).	nonhalt, domain
6	Mapping to SOMDCv6 TM7	Item-by-item comparison; section E below is the computed version.	—
7	Evidence	Simulation tables (check_proof.py). Not part of the kill.	—
—	Review log	The skeptic's 5 minor gaps and their fixes.	—

Two copies exist. submission/proof.md (rendered above) says "fully formalized". The working proof.md still says §3.3 and nonhalt are informal; only its status lines are stale. One wording trap in both: in §5 and §6, "I1 passed twice" means the Coq hypothesis named I1, not Inc clause I1.

EThe .v, annotated

Read it here: review/v.html: line numbers, highlighting, a margin note per item, lines that differ from TM7 shaded. Also: diff vs TM7 (9 hunks, +415 / −77 by GNU diff -u) and TM7 with its own line numbers.

Fig EWhere the 599 lines come from

copied 80

adapted 113

new 359

other 47

copied from TM7 same text as TM7 (16 items)adapted TM7's text with edits (4 items) new no TM7 text (21 items) other: 43 blank, 3 Scope, 1 section-comment line

Of the 113 adapted lines, 34 differ from TM7 (shaded in v.html); the rest are TM7's text. So about 159 of the 599 lines are TM7's text (not counting the 47 other lines). Of the 359 new lines, 287 belong to the domain proof (proof.md §3.3); key alone is 158.

Whatlines of 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v by item tag; TM7 itself is 246 lines (SOMDCv6.v 1626–1871)Tagscomputed by comparing each item's text with its TM7 source; an item with no TM7 source is new

lines	item	tag	in plain English	proof.md	TM7 (SOMDCv6.v)
1–8	Header comment	new	Which machine, which template, the one-line idea, where the informal proof is, the AI-assistance line, and what was checked (busycoq commit, Coq version, the Print Assumptions result).	—	—
10–14	Imports	copied from TM7	The five Require lines of SOMDCv6.v's shared header.	—	1–5
17–20	Ltac esc	copied from TM7	Proves a concrete segment or side goal by running the machine (bounded computation).	—	8–11
22	Ltac ec	copied from TM7	Shorthand for econstructor, used to build R derivations.	—	13
24–25	Ltac am	copied from TM7	Proves the halving pattern of a 0-digit (every 2 passes in, 1 out) from two small computed facts.	§3.1	15–16
27	Definition tm	adapted	The machine. The only change from TM7's line is the string: A1 = 0RF instead of 0RC.	—	1627
28–29	Notations -->* and -->+	copied from TM7	Multi-step arrows for this tm.	—	1628–1629
31–33	Digits ld, d0, d1	copied from TM7	The three 3-cell digits: L = 110, 0 = 000, 1 = 100.	§1	1631–1633
34	Notation w1ld	new	The 4-cell word 1 110 (stray 1, then an L) that a drain pass meets in C1. Declared before Open Scope nat, where a list literal would be read as list nat.	§3.1 C1	—
35–39	Passes hR, hR', hL, h, h'	copied from TM7	h enters in state B and leaves in C (a drain pass, and also our +1 pass). h' enters as 1 D> (the eater).	§1 Passes	1634–1638
41–42	Inductive RD, H	copied from TM7	Digit names LD, D0, D1, and the two modes: hx = eater, h1 = drain (with a stray 1 in front).	§1	1640–1641
44–50	Fixpoint toRC	copied from TM7	Turns a digit list into the right half-tape: the digits' cells, then 0^inf.	§1	1643–1649
52–56	Definition toH'	copied from TM7	The cell in front of the word: nothing for the eater, the stray 1 for the drain.	§1	1651–1655
58–62	Definition toH	copied from TM7	The first pass of each mode: the eater pass h' for hx, nothing extra for h1.	§1	1657–1661
64–69	Inductive Inc	new	Inc r r': r' is r + 1, reading the 0/1 digits as a little-endian binary number and skipping L. Clauses in proof.md's names: Inc_nil = I4, Inc_d0 = I2, Inc_d1 = I1 (carry), Inc_ld = I3.	§2 Inc	—
71–118	Inductive RIncs (the sweep relation R)	adapted	R(mode, k, r, r'): 12 clauses. 8 are TM7's text. X1 (hx_ld) and C1 (h1_ld) gain an Inc premise and continue on the incremented rest. Z1 and Z0 are new zero-pass clauses.	§2 R	1663–1701
120–131	Ltacs cat3, tr1, wal, tr2	copied from TM7	cat3 peels one 3-cell digit off the side; tr1/tr2 split off a first pass; wal pushes k identical passes through a fixed segment.	—	1703–1714
133–136	Lemma z1_eq	new	As tapes, 1 100 0^inf = 110 0^inf. This identity is all that clause Z1 says.	§3.1 Z1, Z0	—
138–141	Lemma z0_eq	new	As tapes, 1 000 0^inf = 100 0^inf: the identity behind Z0.	§3.1 Z1, Z0	—
145–156	Lemma Inc_spec	new	Machine fact: one h pass over the cells of r leaves the cells of r + 1. One computed segment fact per digit.	§3.1 Inc_spec	—
158–164	Lemma seg_hx_ld	new	Eater enters an L: the cells 110 stay 110, and the passes sent on to the right become h (the +1 pass), then h', then k+1 drain passes. In TM7 the leading h is absent.	§3.1 X1	related: 1724
166–172	Lemma seg_h1_ld	new	A drain pass meets 1 110: the same output shape, h ++ h' ++ h^(1+k).	§3.1 C1	related: 1728–1730
174–221	Lemma RIncs_spec	adapted	Soundness: every R derivation is an exact run of the machine at the pass level (sideRLs). One bullet per clause. Bullets 1 and 4 (X1, C1) chain seg_*_ld with Inc_spec; the last two (Z1, Z0) rewrite with z1_eq/z0_eq; the other 8 are TM7's.	§3.1	1718–1756
225–233	Lemma Inc_total	new	Every word has a +1.	§3.3 table	—
235–239	Lemma Inc_fun	new	The +1 is unique. The only functionality fact the domain proof uses.	§3.3 table	—
241–242	Lemma RIncs_eqk	new	Helper: change the count of an R fact to an equal number, so clauses with counts like 1+k*2 apply after lia.	—	—
244–247	Ltac inc_nil	new	Helper: an Inc [] _ hypothesis can only be Inc [] [D1]; invert it.	—	—
249–267	Lemma RIncs_Inc (Lemma A)	new	Lemma A: one more pass after a sweep's k passes = +1 on its output. Each clause maps to the same clause with count k+1, except C3/C4 swap on a carry, R0/R1/R2 shift, Z1 becomes C2 and Z0 becomes C3.	§3.3 Lemma A	—
269–281	Lemma RIncs_nxt_1 (Total_1)	copied from TM7	A drain with any count q at the right end always finishes.	§3.3 Total_1	1758–1770
283–303	Lemma End_1	new	If the right end with count m wrote w, then a drain arriving at w with any q >= m reads w to the end.	§3.3 End_1	related: 1796–1813
305–317	Lemma End_x	new	The same for an eater arriving at w: any q with m <= 2q+2 suffices.	§3.3 End_x	related: 1796–1813
319–358	Inversion helpers (7)	new	What an R fact must look like given its first digit, one lemma per case. inv_h1_d0 has three outcomes (odd count, even count, or Z0). TM7 used inverts inline instead.	§3.3 proof	—
360–367	Definition Inv	new	How many passes the second sweep needs, given the first sweep's mode and count (tp, k), the j pending +1s, and the second's mode and count (tq, q). With j = 0 it is exactly TM7's condition.	§3.3 Inv	related: 1785–1790
369–526	Lemma key (proof.md's RIncs_nxt')	new	The domain lemma. If the first sweep is defined on r, and a second sweep reads its output after j pending +1s with enough passes (Inv), the second sweep is defined too. Induction on the first derivation: one bullet per clause (12).	§3.3 Key lemma	related: 1783–1835
528–535	Lemma domain	new	The instance used: a sweep's output can be swept again (key at k = j = q = 0).	§5	related: 1863–1865
540	Notation lh	copied from TM7	The left part 0^inf 1: everything left of the wall's second 1.	§1 Family	1839
542–543	Definition S'	copied from TM7	The boundary configuration S(r) = 0^inf 11 D> <r> 0^inf.	§1 Family	1841–1842
545–555	Lemma BigStep	copied from TM7	One sweep: R(hx,0,r,r') gives S(r) -->+ S(r'). RIncs_spec supplies the pass, sideRLs_1 and follow10 run it, es does the 3-step wall.	§3.2	1844–1854
557–558	Lemma start	new	The blank tape reaches S(L1) (step 16), by computation. TM7 stops one sweep earlier, at S(1) (step 5).	§4	related: 1858–1859
560–575	Lemma nonhalt (the theorem)	adapted	multistep_nonhalt to S(L1), then progress_nonhalt_cond with P r := exists r', R(hx,0,r,r'): BigStep makes the step and domain keeps P. Differs from TM7 in the start, a hand-built witness for P, and the domain call.	§5	1856–1869
579–599	Rule-table comment	new	The rule table in the comment block that busycoq proof files end with.	§2	—

FReviewer checklist

What a busycoq maintainer checks, and how you can check it yourself. Run this once in a WSL shell, then each command below:

cd ~/projects/bb6-hunt && T=1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---

check	why	command	expected (and today's result)
It compiles against unmodified busycoq, states the right theorem, and uses no axioms	check_kill: pinned busycoq (0940bb9c), byte-exact string, top-level `nonhalt : ~halts tm c0` with absolute names, no forbidden words, `Print Assumptions` within the baseline, coqchk.	tools/check_kill.sh "machines/$T/$T.v" "$T"	`RESULT: PASS -- this is a kill`, 17 `[PASS]` lines. Today (12:00 PDT): PASS, compile 3.82 s, coqchk 1.06 s, 6.1 s wall in all (output).
The string is a current holdout	Maintainers check the machine is still open.	grep -nx "$T" data/holdouts/2026-10-07_778.txt	`301:1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---` (the list has 778 lines). Also search #bb6 and the sheet for a claim before posting (targeting code A).
The theorem statement	The two lines a maintainer reads first.	sed -n '27p;560p' "machines/$T/$T.v"	line 27: `Definition tm := Eval compute in (TM_from_str "1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").` line 560: `Lemma nonhalt: ~halts tm c0.`
The file you post is the file that passed	Same bytes in machines/ and submission/.	sha256sum "machines/$T/$T.v" "machines/$T/submission/$T.v"	both `e434537eca67d99f…` (matches check_kill.txt).
What changed vs TM7	A maintainer compares with the template (mxdys's SOMDCv6.v).	diff -u "machines/$T/rocq-scratch/TM7_toplevel.v" "machines/$T/$T.v" \| less	9 hunks, +415 / −77 lines (this command, GNU diff); same thing rendered: diff.html. Section E tags every item.
Spot-check the one rule change on the real machine	That A1 = 0RF really is "one +1 pass, then where TM7 is".	python3 -B "machines/$T/check_rules.py" --lentry	CLI: L entry ours/TM7, eater/drain, 1393/1393 each (0.5 s, run for this page). Visually: explorer preset ↗, the two runs agree until the dashed line (A1); press d for the diff view.
The informal claims hold on samples (optional)	Evidence only; not needed for the kill.	python3 -B "machines/$T/check_proof.py"	ALL PASS in about 7 s (run for this page). `--full` takes longer and adds the Rocq partial check.

Reviewability: what a maintainer may push back on

My read of the .v and of submission/proof.md, as a maintainer might read them; "how likely" is my guess. None of these affect correctness, and none are applied.

how likely	issue	details	possible fix	where
fine as is	Header comment cites no repo paths	Lines 1–8 name the template as `verify/SOMDCv6.v` (busycoq's own layout), the informal proof as the accompanying write-up (proof.md), and the check as busycoq commit, Coq version and the `Print Assumptions` result. Until the 2026-10-10 comment-only edit they named `vendor/busycoq/verify/SOMDCv6.v`, `machines/…/proof.md` and `tools/check_kill.sh`.	None.	lines 1–8
likely	proof.md has internal and stale lines	Only matters if you post `submission/proof.md` with the .v (the README lists it). Line 3: the "Submission copy…" note. Line 74: "the extra 1 Dennis noticed" at "the Checkpoint A picture pair". Lines 89 and 236 cite `check_proof.py` ("in this directory"), which is not in `submission/`. §5 line 203 uses `c' = S(1)` while the .v starts at S(L1); only line 210 corrects it. Line 115 says Z0/Z1 "are never used on the run from blank", which is simulation evidence (3,000 sweeps). Lines 97 and 221 prove Z0/Z1 by `sideRLseq_O` (line 97: "via `applys_eq`"); the .v uses `rewrite z1_eq. constructor.` (lines 219–220). The Review log (lines 263–275) describes our skeptic process, `RSpec2.v` and notes.md.	Drop line 3, the Dennis aside and the Review log; drop the check_proof.py references or ship the script; say "not used in the first 3,000 sweeps"; describe Z0/Z1 as the .v does; for §5 see "start" below. Optional: "one step after its A1" (line 93, also the Discord draft) reads better as "right after its A1 step".	proof.md
maybe	Length: 599 lines vs TM7's 246 (2.4×)	`key` alone is 158 lines. Repeated text inside it: h1_d0_0 = h1_d0_1 (20 lines each), rh_0 = rh_1 = rh_2 (3 each), hx_d1 and hx_d0 differ in one line (7 each). TM7 compresses its case analysis with `solve_v1`/`solve_v2`.	Optional: merge the identical bullets (e.g. `1-2:` goal selectors or a local Ltac). Not tried.	key
maybe	The start differs from TM7 without need	`start` goes to S(L1) and the witness for P is built by hand (lines 557–569). rocq-plan.md §3.5 picked S(L1) for an invariant that also required r to be a sweep output; the final invariant does not. TM7's text (`S' [D1]`, `1: esx.`, `2: repeat ec.`) also works here: I compiled that variant in a scratch copy today (4.0 s, Print Assumptions closed; not run through check_kill).	Use TM7's lines; then nonhalt differs from TM7 only in the domain call, and proof.md §4/§5 (which use S(1)) are correct as written, so the S(L1) notes (lines 199 and 210) can go.	nonhalt
maybe	Generic names	`key`, `domain`, `start`. proof.md calls key `RIncs_nxt'`; TM7's is `RIncs_nxt`.	Rename key to RIncs_nxt' so the parallel with TM7 is visible.	key
fine as is	Rule-table comment at the end	Same fenced comment block that upstream files end with (e.g. `1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v`).	None.	table
fine as is	Imports and helpers	Exactly SOMDCv6.v's header; check_kill's allowlist accepts them. Copied items are byte-identical to TM7 (computed in E).	None.	E
local only	Stale lines in our own notes	Working proof.md says "partly formal"; notes.md still has "Informal proof: Not started" and empty "Formalization log"/"Outcome" sections. notes.md § Kill ("1,371 characters plus `<LINK>`") and the discord.md header ("1,371 characters before the link") both count the placeholder already (1,365 without it). Not in the post.	Housekeeping only.	notes

Before posting

Run the first four checks above (about a minute).
Search #bb6 and the sheet for the string (targeting code A). Targeting also suggested asking mxdys whether SOMDCv6 was tried on this machine (code B); with a proof in hand that is optional.
Your read of proof.md is effectively Checkpoint B. If you have notes, fold them into both proof.md copies (notes.md § Kill says so too). If you post proof.md, fix its "likely" row above first.
Fill <LINK> in the Discord draft (1,371 characters with the placeholder; Discord's limit is 2,000).
If you take any fix from the table above, re-run check_kill on the edited file and copy it into submission/ again (the sha256 will change).

Built by review/build.py from the files above; every line number, count and derivation on this page is computed and asserted there. Stage times come from the workflow records and are hand-entered.