/machines/1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---/notes.md · raw

W5-1 · 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (740 line 349)

Observe stage, 2026-10-13. Sheet class: Bell eats counter (results.csv row 1038: class only, no status, no Done By; also listed in classifications.csv under "Bell eats counter"). Wave 5 pick W5-1.

Checks

Byte-exact: tools/holdouts.py contains data/holdouts/BB6_holdouts_740.txt finds it at line 349; it is on all 26 snapshots since 2024-06-14 (holdouts.py lookup).
No claim: no hit in data/discord/*.txt; the sheet row has only the class.
Upstream: holdouts.py solved says "no completed proof". The only byte-exact mention is Eqv_v3.v Module TM518 (as tm', eqv: halts tm c0 <-> halts tm' c0). That route is closed for us: Eqv_v3.v imports BBinf (reports/targeting.md forbids it). The upstream HEAD 9cf9e88 checkout has no other file with the string or with TM518's tm (the RWLAccHaltv1 / CPS / RWL hits share only a suffix and are different machines).
Siblings (canon, all 6 starts, renaming + mirror): only start A is on the 778/740 lists. Starts B and F are in eqv groups / Eqv_v3 but on no list; C, D, E run off in 2 steps. The 1590-machine eqv file pairs {349, TM518 tm} and, separately, {W4-2, TP} (TP below). No 740 sibling.

The mechanism in one paragraph

349 is W4-2's table with one cell changed, seen in a mirror and started in W4-2's F. Write TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC (W4-2 = ..._1LA1LF, so only F1 differs: 1RC instead of 1LF). Then mirror_rename(TP, F518) == 349 with F518 = (A->F, B->A, C->B, D->C, E->D, F->E), exactly as W4-2's proof.md 7.3 found for TM518 tm. In TP only A1 = 1LF enters F, and A1 writes 1 on the cell to the right of F. So when TP's F reads a 1 at cell p, cell p+1 is 1, and

TP:   x 1 <F 1 r   --F1 (1RC)-->  C reads p+1 = 1 --C1 (1LA)--> A reads p = 1 --A1 (1LF)-->   x <F 1 1 r   (3 steps)
W4-2: x 1 <F 1 r   --F1 (1LF)-->                                                              x <F 1 1 r   (1 step)

Same tape, same state, same head. TP from 0^inf F> 0^inf is therefore W4-2 from F with every F1 stretched into three steps (the detour), and 349 from blank is its mirror image. In 349's own letters the detour is 1 A> 1 x --(A1 D1 B1)--> 1 1 A> x where TM518 tm does it in one A1 = 1RA step.

Everything of W4-2's proof carries over unchanged: the configuration family, phi, the rules R1-R5, the macro rules S0-S3/P0-P4, the invariant I, Lemma S and Lemma C. Only step counts change (+2 per detour). The start is W4-2 proof.md 7.3: K('',0,1) = (std,0,1) at step 14, then S0 to (std,2,2) at step 73, which satisfies I.

Configurations and rules (349 orientation; validated on the 349 table itself)

K'(w,n,m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w 0^inf, with w written from the cell B reads (offset 0) to the right. This is the mirror of W4-2's K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf (A -> B by F518). phi, std, pk, decode: exactly W4-2's (offset d = bit d).

rule	from -> to	steps	validated (direct 349, seeds 1+2)
init	`0^inf A> 0^inf` -> K'('',0,1)	14	exact
init-S0	K'('',0,1) -> K'(std 2, 0, 2)	59 (step 73)	exact (ORB)
R1 bounce, n >= 1	K'(w,n,m) -> K'(phi w, n-1, m+1)	L'(w) + 10n + 7	1200/1200
R2 overflow, q even	K'(w,0,m) -> K'(x, m+1+q/2, 0), phi(w) = 0^q 1 x	L'(w) + q + 8	1200/1200
R3 reset, q odd, x = 00x' or empty	K'(w,0,m) -> K'(x', 0, m+(q+3)/2)	L'(w) + q + 14	1200/1200
R4 halt, q odd, x starts with 1	halts (F1)	after L'(w) + q + 8	1200/1200
R5 nested, q odd, x starts with 01	no rule (never met inside the macro rules)		(291+ seen)
detour	`1 A> 1 x` -> `1 1 A> x` (A1 D1 B1)	3	lockstep 2 x 3e7 W4-2 steps, 479 detours

L'(w) = 1 if the first cell of w is 0; else 2e+3+2·p11, where (e, e+1) is the first adjacent 00 pair of w (0^inf counts) and p11 = the number of adjacent 11 pairs among cells 0..e-1 (one detour each).

Macro rules (W4-2 proof.md 3.4, closed forms unchanged), from a clean overflow state (typ,N,m) = K'(typ(N),0,m) to the first clean one with N' >= 1; checked by direct 349 runs from constructed and random states (seeds 1+2): S0 86/86, S1 177/177, S2 81/81, S3a 81/81, S3b 86/86, P0 83/83, P1 108/108, P2 157/157, P3 81/81, P4a 81/81, P4b 85/85; states outside every rule (4) behave as W4-2's abstract executor says.

Whole-run checks: - 349 from blank = mirror of TP from F, state by state and cell by cell: 2,000,000 steps (MIR). - TP from F = W4-2 from F with F1 -> F1 C1 A1, exact, 30,000,000 W4-2 steps; TP steps = W4-2 steps + 2·479; every F1 read finds a 1 on its right (EXP). - The overflow states of the direct 349 run from blank equal the macro-rule orbit (std,0,1) -> (std,2,2) -> (pk,5,3) -> (std,6,5) -> ... for 140 macro steps, to step 30,355,388 (ORB). - I holds along 1,000,000 macro steps from (std,2,2) (final m = 2,573,515; rule mix S1 485k, P2 485k, P4b 20.6k, S3b 9.1k, P1 50, S0 4, P3 3, P0 2). - scripts/observe_checks.py: 28/28 PASS with seed 1 and seed 2 (work/observe_checks_seed{1,2}.log, ~20 s each). - Long run: tools/sim.py 1e9 steps, no halt, span -457..1866 (2,324 cells), 1,157 ones. 400 overflow configurations to step 674,711,540 (img/counter_rows.png): 191 std, 194 pk, 13 dirty, 2 empty. - compress (direct, record-aligned, 1e8): the right-record skeleton is 0^inf (10)^a (01)^b 1^c A> 0^inf with a+b constant inside a cycle (the bounce moves one 01 from the n-block to the m-block); qsim 2e5 loops (1.5e7 steps) shows the same (10)^a (01)^b blocks. work/compress_track_1e8.txt, work/qsim_2e5loops.jsonl.

Template check: W4-2's .v (1,217 lines) lemma by lemma, on TP

TM-level lemmas: TA0, TA1, TA2, TF0, TF1, TF2, TF3, TB (the left step), RS, OVe, OVo, init0. Everything else (PA/PF relations, Gap/Sweep/F_inc/F_carry, INC_, BS_ macro rules, I, Cov_/C_, step_std/step_pk/ step_I) is arithmetic over these or a composition of PA_spec/RS/OV, and carries over verbatim.
Which use F1: TA2 (A1 then F1), TF2 (F1 then F0), TF3 (F1, F1). RS reads F only as F0; OVe/OVo never reach F.
TA2 holds on TP as stated: the cell right of F's 1 is the E-cell A1 just wrote (detour C1 reads it).
TF2, TF3 need the right side to start with 1: restate as [1;0] *> l <{{F}} [1] *> r -->+ ... and [1;1] *> l <{{F}} [1] *> r -->+ ..., and phi_spec's PF clause as PF e o e' o' -> forall r, WS e o <{{F}} [1] *> r -->+ WS e' o' {{B}}> [1] *> r. Every entry into PF (PA2 via TA2, PF1 via TF1, PF3 via TF3) already has [1;1] *> r on the right, so the induction goes through; PA_spec (the only thing the rest uses) is unchanged.
init: F;; tape0 -->* K 2 0 0 2 (= St (false,2,2)), 73 steps, no detour before step 121 (esx).
Reduction to 349, as #24 does it: Perm (flip tm349) tmP f with f = (A->F, B->A, C->B, D->C, E->D, F->E), flip_halts (Flip.v) + perm_halts (Permute.v): halts tm349 c0 -> halts tmP (F;; tape0). Both lemmas are in the framework (no BBinf).
Estimated .v delta: ~40 changed/added lines on W4-2's 1,217; W4-2's compile was 66 s native.

Cryptid check (ground rule 6)

Not a cryptid. The branch taken in each cycle depends on bit patterns of N, but W4-2's invariant I is closed under every branch using linear bounds and two parity facts (W4-2 proof.md 7.2). The detour changes no branch.

Confidence: high

Every regime reached from blank is covered: the run is exactly W4-2 from F with stretched F1 steps (an exact, step-by-step simulation, not a statistical fit), W4-2's proof (check_kill PASS) contains the induction from any state in I, and (std,2,2) at step 73 is in I. The only new formal pieces are three low-level lemmas, a start and a 3-lemma reduction.

proof.md as a delta of W4-2's (Lemma E = detour, start from F, conjugacy), check_proof.py from scripts/observe_checks.py, then the .v (W4-2 copy + the changes above) and check_kill.sh.

Kill

2026-10-13: KILLED_NONHALT. 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v (1,278 lines, sha256 32cbc5c1…4e88) proves Lemma nonhalt: ~halts tm c0. against unmodified busycoq 0940bb9c, Individual62 only. It is W4-2's .v with the table as tmP (F1 = 1RC), TF2/TF3/phi_spec's PF clause restated with [1] *> r on the right, initF (73 steps from F to St (false,2,2), solve_initF), nonhalt_F, and the conjugacy perm_349 : Perm (flip tm) tmP f349 + flip_halts + perm_halts. Comments aside, 16 of W4-2's code lines replaced and 43 added. - check_kill PASS three times on the same sha256: formalizer 09:08:08Z (rocq/check_kill_r1.log), independent auditor 09:10:39Z, fresh packaging run 09:13:45Z (compile 64.1 s native, coqchk -norec pass 27.2 s, 0 assumptions; only warning: the second TM_from_str literal, tmP). - Package: submission/ = the .v, proof.md (public write-up rewritten from proof.md; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh run, verbatim, so it has absolute local paths), README.md, discord.md (not posted; 1,485 chars before <LINK>). - Posting: with or right after W4-2's announcement; W4-2's discord.md third paragraph still says row 1038 is "Not formalized yet" and needs cutting or a one-line pointer to this message.