W5-7 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---

740 list line 700. Sheet class "Shift-overflow bouncer counter" (sheet row: no status, no notes, no "done by").

Stage 1: Observe (2026-10-13)

Outcome: GO for a HALT proof. The machine is SOBCv6.v TM3's table started in TM3's state B. TM3's own rules (all proved in Rocq for that table, so they hold verbatim here) drive 194 complete counter cycles from step 847. In the 195th overflow an increment carries off the far end of the counter and the machine halts (F reads 1). Halting time: a power tower of height about 195 (not computed exactly).

Checks

• Byte-exact: grep -nx finds it at line 700 of data/holdouts/BB6_holdouts_740.txt (also 778 list line 738; eqv-1590 file line 1328).
• Claims: none. data/discord/2026-08-24_mxdys_ubrrba_86.txt lists it on mxdys's UBRRBA_TODO list (a to-do list, not a claim). Sheet results row is empty apart from the class.
• Upstream hits are equivalences only: vendor Eqv_v3.v TM637 (1RB0RE_0LB1RC_1LD1RA_1LA0LE_0RC0RF_0LC--- ↔ 700); upstream HEAD Eqv_RegularPairs.v TM101 (1RB0RF_0RC1RD_0LD---_1LE1RA_1LA0LF_0RD0RC, 778 line 695 ↔ 700) and Eqv_WordPairs.v TM98 (1RB---_1LC1RE_1LA0LD_0RE1LC_1LC1RF_1RB0RD, 778 line 160 ↔ 700). The eqv-1590 group also has 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LB---. A verdict for 700 settles these partners through the equivalences; none of them is on the 740 list.
• Direct sim: no halt to 10⁹ (span −12..28,793 at 10⁹; the run is then inside the third counter fill). qsim: 200,000 loops = 1.75·10¹⁰ steps, no halt, no rules found. compress.py track (10⁷, records): skeleton … 1^a (111100)^b 1^c (001)^d A> 0^inf with d growing by 2 per record pair = the right part growing.

Same table as TM3

State map ours → TM3: A→B, B→C, C→A, D→E, E→D, F→F, no mirror (checked by brute force over all renamings). So our blank start = TM3 started in B. canon() per start state: our start C = TM3's start A (proved halting in SOBCv6.v); starts B, D, E, F are on no list. No 740 sibling shares the table.

Notation (TM3's, in our state names)

• Left part = counter Lmp x: a list of words, W0 = 001, W1 = 111 (paper order), x[0] next to the head.
• Parsing from the head: W0 = separator; W1 b = a digit pair with bit b (W1 W0 = 0, W1 W1 = 1). Least significant digit next to the head.
• Right part RC n = 1 (011)^n 01 0^inf. TM3's l <| r = l <D 010 r; l |> r = l A> r.
• P-config: Lmp x <D 010 RC 1.

Rules (all from SOBCv6.v TM3; table-specific, so they apply unchanged)

So one cycle is P x → P y with y = (W1 W0)^((c−1)/2) · W1 W1 · LOv(ones(x))[1:]: the counter fills, the right part's length becomes (c−1)/2 new zero digits, and the counter is re-read with a shift. c grows like 2^(previous c): shift-overflow.

From blank

• First P-config of the chain at step 847: x = 1000111011 (head side first).
• Step 2136: x = 10101100110101011 (count 5 consumed). Step 38,573: x = (10)^25 11 0 10 10 0 1 1 0 0 0 0 1 1 1 0 1 1 (count 51). Both predicted by the model and found in the direct run (exact tape match).
• Cycle 2 count = 1,308,622,847 → the next block (10)^654,311,423. From cycle 3 on every new block is astronomically long.

The long run (model: work/model/fast.py, cross-checked)

• Blocks (10)^k / (11)^k with k ≥ 6.5·10⁸ are treated as "BIG" (they lose at most one pair per cycle; 194 cycles never empty them). Only zero/non-zero of block lengths matters to the structure.
• Exact list model (tm3model.py) = direct sim; run-length model (rle.py) = exact model on 3000 random lists; stack model (fast.py) = rle.py through 110+ cycles; and fast.py's predicted next P-config is reached by direct simulation of instantiated tapes (BIG → 1..3 pairs) at cycles 3, 10, 30, 60, 100, 150, 190, 193 (ovbig.out).
• Shape: near the head the list freezes into segments between BIG blocks (110 | 1000011 | 100100011 | 10000010011 | …, one more per cycle, each 2 symbols longer); the far tail (≈ 100–200 symbols) keeps changing and looks irregular.
• Cycle 194 (the 195th overflow after step 847): LOv reaches far token 10 (a W1W1 pair) with v = 1 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1, so it must increment 0^11 11 11 11 → carry off the far end. Direct sim of the instantiated tape halts (F reads 1) 64 cells from the far end, for every instantiation tried (3 Python + 2 C runs, BIG = 1, 2, 3 pairs, RC 2..5), and the far 15 tokens alone already reproduce it (halt at cell 60 from the far end, 1,392..2,797 steps) (trunc.py, Fig 4).
• No cycle before 194 hits any failure case (count parity, misaligned pair, LOv starting with W1, far-end carry).

Template comparison (SOBCv6.v Module TM3, lines 1164–1736)

• Reusable unchanged after renaming E→D, B→A in notations: LInc, LOv, LIncs (+ _spec, _lpow), RC, RIncs, Incs, Ov, Lmp', step_rec's skeleton, P.
• New: init (blank → P x at step 847, or 2136 / 38,573), 194 step_rec iterations instead of 2, and a halting tail at the far end instead of TM3's near-head direct run.
• TM3's abstract LOv_rec fails at our cycle 4 ("W11 block sees W1"). That is an artifact of TM3's layout (explicit pairs on both sides of the abstract block): in our layout (explicit pairs on the far side) every (11)^BIG block in 194 cycles sees W0 W0, TM3's case. LInc does meet (10) blocks (992 times BIG, 4 small): needs an LInc_rec case W10 → W1 W1 · W10(k−1) with a lower bound (k ≥ 2) carried in the representation.
• 0 times (11) blocks in LInc; 0 misaligned pairs.

Cryptid check (ground rule 6)

Not a cryptid: the fate is decided by a finite deterministic computation on lists (194 cycles, list ≤ 38,502 items) that ends in a halt. The far tail looks irregular, so there is no closed-form invariant, but none is needed for a HALT proof.

Plan for the proof (next stage)

1. Copy TM3's module with our TM string and renamed states.
2. Representation with lower bounds: e.g. W10 l / W11 l = [W1;W0]^^(l+n) / [W1;W1]^^(l+n), l ≤ ~200; LIncs_rec / LOv_rec / LInc_rec with the block cases above; step_rec in our layout.
3. init by solve_init to step 847 (or start from the explicit list at 38,573).
4. 194 step_recs by vm_compute (list up to ~38.5k items).
5. Halting: an inductive "overflow halts" predicate mirroring LOv (deep part halts ⇒ whole halts; W1W1 with deeper W1 · x' and a far-end carry in x' ⇒ halts), its _spec by induction, and a boolean checker; the base case = the far-end configuration of Fig 4.

Files: work/model/ (all model scripts and logs), work/sim_1e9.jsonl, work/qsim.jsonl, work/compress_track.txt.

Kill (2026-10-13)

KILLED_HALT. The machine halts, so the kill statement is Lemma halt: halts tm c0. (line 797 of the .v) and the oracle is tools/check_kill.sh --halt. The computed task asked for KILLED_NONHALT; the default (nonhalt) mode of check_kill fails on this file by design, so status.json says KILLED_HALT, as for C2-552.

• Kill file 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---.v: 838 lines, sha256 30ba9693…6786, adapted from SOBCv6.v Module TM3 (same table renamed; ours A B C D E F = TM3 B C A E D F, started in TM3's B). Imports Individual62, BinaryCounter_v2, NatMod, SimplTape, Longitudinal, Eqb.
• Chain of the proof: init : P x2' (38,573 steps, solve_init) -> iter_spec over 192 step_rec cycles (final_check_ok : final_check 192 = true by vm_compute) -> LIncs_rec_spec + Incs -> doom_rec_spec (walk0/walk1/doomed_pow) -> far_halt (1,368 steps, solve_halt, r symbolic) -> halts_evstep.
• Fresh check_kill --halt on the final file (2026-10-13T11:35:43Z): PASS, exit 0, all 17 checks; compile 25.6 s with -native-compiler yes; coqchk -norec finished in 43.3 s; Print Assumptions halt = functional_extensionality_dep only (baseline). Same sha256 as the formalizer's PASS (rocq/check_kill.out) and the independent audit run.
• Holdout string byte-exact: 740 list line 700 (also 778 list line 738).
• Halting time: a power tower of height about 195 (estimate from the cycle law, not computed, not proved).
• Equivalence partners (status.json eqv_partners) are settled through busycoq's equivalences: Eqv_v3 TM637 and TM636 (pinned commit), Eqv_RegularPairs TM101 and Eqv_WordPairs TM98 (upstream HEAD). Not formalized here.
• Package in submission/: the .v (identical copy), public proof.md (rewritten from the internal proof.md; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh run, verbatim, so it contains absolute local paths), README.md, discord.md (1,701 characters before <LINK>; not posted).