W6-1 · 740 line 10 · 1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF

Observe stage, 2026-10-14 (Claude, Wave 6). Claimed in coord/claims.tsv; Astra told (coord/mailbox/to-astra/20261014-*-claude-w6-1-claim-holdout10.md).

Pre-checks

• Byte-exact on data/holdouts/BB6_holdouts_740.txt (line 10).
• No claim: the sheet has it as "Shift-overflow bouncer counter" with an empty status; mxdys's UBRRBA list (data/discord/2026-08-24_mxdys_ubrrba_86.txt) is a to-do list, not a claim.
• Same table, other starts (canon up to renaming + mirror):
• from D: 1LB0RD_1LC0RC_1RA1LC_1LE0RB_1LF---_0LA0LE = SOBCv10.v (upstream, nonhalting hand proof);
• from B: 1RB---_0RC0RA_1RD0LF_1RE0LE_1LC1RE_1RA0LD = TCv1.v (decider);
• from C, E, F: not holdouts, not solved. No other start is on the 740 or 778 list.

Frames and words

The state map from ours to SOBCv10 is A,B,C,D,E,F -> D,E,F,A,B,C with a mirror. So our machine is SOBCv10's machine started in SOBCv10's D. Everything below is written in SOBCv10's frame (its wall on the left), because that is how its lemmas read. Our own frame is the mirror image: fossil and counters on the left, the tally growing to the right (Fig 2).

A hash is one signal: SOBCv10 B> at the left end of the word region (our <E), returning as SOBCv10 <F (our C>).

Mechanism (same as SOBCv10)

• The left part W X^u is a tally: every returning hash walks to the wall and back and adds one X (left_emit_call). Steps grow like u², which is why direct simulation sees so little.
• To its right sits a binary counter of A/B digits (least significant next to the head) that each hash increments. Its overflow carries are absorbed by marker words further right (D -> A grows the counter, C A U U -> D C A eats a U pair, ...).
• When the counter and everything behind it is all B and the carry reaches the edge t, an exception fires: the tally turns into exactly n = (u-1)/2 fresh hashes, which are fed into the rewritten counter (E^w A, a mixed-radix word), and the result is W B> C A U^(2n) output (exception_done). The C A U^(2n) block then needs 2(2^n - 1) hashes to drain (cd), so each exception makes the next one exponentially later.
• SOBCv10's own start passes 4 exceptions and then enters its round invariant (post_ca_state + sobc1_round_invariant), where each round adds one binary column.

Our opening, exactly (hash-level simulation)

Tool: work/rsim4.c (exact TM simulation; a returning hash at the wall is teleported by the proven left_emit_call, so a hash costs O(1) instead of O(u)). Checked on SOBCv10's own start: it reproduces sobc1_first_half = 2^23+2^22+2^20-2 = 13,631,486 as the n of its third exception (work/hashlevel_run_sobcv10_start.txt). Our run: work/hashlevel_run_ours.txt.

Between 3 and 4: cd drains 28 pairs, one more U pair is eaten, and the odd C A U A B B t turns into the frontier above (counter width 30).

Our opening, symbolically (families checked on small instances)

work/opening_checks.py, 40/40 PASS (work/opening_checks.out). Each family was run on small parameters and matched a closed form; the real parameters are m = 30, p = n4.

For m = 30, p = n4 this gives:

exception 5 output = A^(n4+2) B B A B A · B A B A B A B A B A B A B A B A B A B A B A B B B A B · U^3 A t

SOBCv10's generic exception_done_ca n5 pairs rest (pairs = n4/2 + 1) then gives

W X^(round_post_unary c p) B>  A^(round_primary_width c p)  U U  [col]  U^3 A t
c = (n5 - 6)/2,  p = n4/2 - 3 = 3·2^28 - 4  (half_parameter c = n5, half_parameter p = n4)
col = B B B A B A B A B A B A B A B A B A B A B A B A B B B A B   (29 digits, LSB first)

Check against sobc1_round_invariant

So the column fits perfectly, and the far-left fossil (our frame) is the one obstacle: the tape is binary_columns_word [col] ++ U^3 ++ A ++ t then blank, not binary_columns_word [col] then blank. This explains why ccz181078 proved SOBCv10/11/12 without this start.

Does the fossil matter? Each round ends with carries reaching the far end (binary_columns_to_frontier appends the edge t). A small round analog (work/rside.c on A^4 U^2 B A B A B U^3 A t) shows the fossil digit is flipped (A -> B) and the round's frontier becomes ... B^w U^3 B t instead of ... B^w t. So the fossil is a live one-digit pseudo-column with a U^3 separator, and it changes the frontier that SOBCv10's exception lemmas expect. SOBCv10's round lemma does not apply verbatim.

Lead for the next stage (crude round analog, work/round_analog_with_fossil.txt; the start W X^5 B> A^4 U^2 B B A B A U^3 A t does not satisfy the round's numeric relations). Across two exceptions the fossil went U^3 A t -> U^5 B -> U^7 D t. The U run grows by one pair per exception, and U is transparent to hashes (hash_U). The working guess is a tail U^(2k+1) x t with k growing by 1 per round and a one-digit x. This must be confirmed on true round states.

Rules validated (work/validate_rules.py, 10 random instances each, on our machine via mirroring)

emit 10/10, d_absorb 10/10, u_pairs 10/10, cd 10/10, all_A_to_exception 10/10, exception (canonical) 10/10 (work/validate_10.txt).

Cryptid check

No pseudo-random arithmetic. Every step is a binary counter or an exact exponential formula. The open question is structural (the fossil), not number-theoretic. Not a cryptid.

qsim

Block size 4, recursive rules on: 1.69e13 steps in 600 s, no rules proved (only chain steps), as the scout said (work/qsim_n4.jsonl).

Next

Study the fossil per round. Run hash-level analogs over 3-5 rounds with small parameters and find how U^k x t evolves: k, the digit x, and whether it ever feeds a carry back. Two outcomes:

• It has a closed per-round law. Then write proof.md for a generalized invariant: sobc1_round_invariant plus a tail state. This needs new frontier and exception lemmas for the tail (the delta against SOBCv10.v's all_A_frontier_to_exception_done and exception_done_to_next_post).
• It grows irregularly. Then STUCK.

Wave 6, stage 1 (2026-10-14)

Goal: find the far-end tail's per-round law (Claude, about 1 h of the 2 h budget).

Result: the law is closed, and it ends the SOBCv10 regime. Four more exceptions after the entry, a carry reaches the tail's edge in the middle of an exception. In every test that event turns the run into a translated cycler. So the machine looks non-halting, by a route quite unlike SOBCv10's.

Everything below is in SOBCv10's frame. Tools and outputs: work/tail/ (build: gcc -O2 -o rside ../rside.c; gcc -O2 -o fsim fsim.c; gcc -O2 -o tcyc tcyc.c; gcc -O2 -o cyccert cyccert.c).

The tail as one digit with levels

The tail is U^(2k+1) y after the last column. U passes hashes through unchanged, so y acts as one more digit. It has six levels:

A carry into the tail raises the level by one. A carry that arrives at level 4 is the exception trigger.

Three laws

T1, timing. Count the digits as A = 0, B = 1, D = -1, E = -2, with the tail level at weight 2^W (W = number of digits before the tail). Call the total V. Each hash adds 1, and the trigger can only come when everything is B and the tail is at level 4. So the trigger is hash number

5 * 2^W - V        (SOBCv10's own count is 3 * 2^W - V)

modelA.py: 80/80 random instances, including tails at levels -1 and 0.

T2, raw pass. The exception's raw return turns

B^w U^(2k+1) B t   into   E^(w-1) U^(2k+3) y,   level(y) = k - 1   (k = 0..5)

The last column loses its top digit, and the U run grows by one pair. For k >= 6 the return overflows the tail. rawlaw.py: 48/48 for k = 0..5 (1-3 columns, widths 2-9); 16/16 overflow cases for k = 6..9 end in the cycler below.

T3, decode. Let L be the effective tail level: the level minus any deficit left in the last column. By T1 and SOBCv10's frontier count,

n = n_s + (2 - L) * 2^(W-1)

Here n_s is SOBCv10's round_next_half for the same columns. The n_s part decodes exactly as in SOBCv10. Its last column ends below 2^(w-1), so nothing reaches the top digit, which is the eaten one. The extra part gives 2 - L carries into the tail. If L > 2, the truncated last column is instead left short by L - 2 levels (pre-state E/D digits).

modelD.py checks the whole exception (raw pass, launch, decode) against T2 plus a segment decode of n hashes on 25 random cases. 23 match; the other two are not decodes: one decode trigger (see below) and one n = 0.

Per exception, then:

L' = k + 1 - L,   k' = k + 1
last column: width w -> w - 1,  value v -> 2^(w-1) - floor(v/2)
the decode triggers  iff  (k - 1) + (2 - L) >= 5

The chain from the entry (tailchain.py)

column_safe holds for the last column in every row. The z-columns born in each round are SOBCv10's, so SOBCv10's invariant covers them; only the round parameters differ, because n differs.

The exit does not hinge on these exact numbers. Even if a level were off by one, k reaches 6 by exception 11 at the latest, and that exit (a raw-pass overflow) gives the same cycler.

The exit: a translated cycler

• Decode trigger. decodetrig2.py: 60/60 random cases (primary 1-6, 1-4 columns, k 0-5, n <= 600) and 30/30 with k = 4 (the exception-9 case). decodetrig3.py: 8/8 with 3-4 columns and n up to 4,246. All reach the same cycler. For a fixed column layout its start time grows only by about 8 steps per extra unit of n (n = 2,887 vs 3,292: 11,636,681 vs 11,639,921).
• Minimal pending calls. mintrig.py: 10 layouts, each with the trigger on the last or second-to-last decode hash (n = trigger + 1 or + 2): 20/20 reach the same cycler, at the same step up to 8 per unit of n.
• Raw-pass overflow (k >= 6). 16/16 reach the same cycler.
• The cycler (cyccert.c, cycverify.py). Head in state B at the right end of

1000100010001000100010001000100010010001000100010001000100010010100100

with blank to the right. Every 919 steps it moves 3 cells right and never reaches more than 67 cells back. Checked over 2,000 periods with random junk to the left. In our frame it is the mirror image, a cycler running left.

How the toys get there (trigtrace.py and sweeps2.c, k = 4, n = 900, columns 2, 2, 3, 2). This is not a short epilogue: the trigger starts a second counter phase.

1. The trigger's return turns x x pairs into D going left as far as the 1 0 marker, then comes back.
2. Phase P1, 256 long sweeps. Each sweep runs from the 1 0 marker to the right end, ticks a counter made of the old columns (now written in B D / U C / B U / U A patterns), takes 2 v from the pending-call block on the left, and adds 2 x.
3. Phase P2, about 200 shorter sweeps, with the left block frozen.
4. The counter runs out at the right end, and the 919/3 cycler starts there.

P1's length (256) is the same for n = 874 ... 2,000. At n = 874 the v block runs out exactly at P1's end. That run takes another path through the wall and still reaches the same cycler (sweeps2_n900.out shows the n = 900 run).

P1 law so far (p1fit.py, k = 4, n = trigger + 300): P1 = 2^(W-1) sweeps, W = P + sum of the column widths at post_ca. The layouts tested were 2 | 2,2,3,2 (1,024), 2 | 2,2,2,2 (512), 2 | 2,2,3 (256), 2 | 3,3 (128), 2 | 2,4 (128) and 3 | 2,2,3,2 (2,048). So for k = 4 (the exception-9 case) P1 is one full cycle of the truncated columns. P1 depends on k. For 2 | 2,2,3,2 it is 1,024, 3,072 and 4,096 for k = 4, 2 and 1, so

P1 = (5 - k) * 2^(W-1)

This is what T1 and T2 predict if the decode trigger acts like an ordinary trigger for the tail. Its return grows the U run to U^(2k+3) and leaves the tail at level k, and the counter then needs 5 - k full cycles to trigger again. So the run after a decode trigger looks like a short series of nested triggers, each growing the U run, until a raw pass overflows (k >= 6).

In exception 9 (k = 4) that is one cycle, then a trigger with U^13, so k = 6: overflow. P2, which comes before the cycler in the toys, is not explained yet. P1 uses 2 v per sweep. In the 2 | 2,3,2 runs (W = 9, P1 = 256) the v block at the trigger is 2n - 1,239 = 2^W - 3 + 2 * (pending calls). So it is just enough for P1, except for the last sweep or two when no calls are pending; that run takes the wall path and still reaches the cycler. Whether 2^W - 3 + 2 * (pending) holds in general is not yet checked. P2 (131 ... 1,855 sweeps) has no fitted law yet.

At the real sizes this is a race between the P1/P2 counter (old columns, huge widths), the x fuel (finished calls) and the v block (pending calls). Every small case ends in the cycler, including the boundary ones, but the race is not computed.

What this changes

• There is no tail-aware infinite round invariant. The SOBCv10 rounds stop at exception 9, so the stage-0 plan (generalize sobc1_round_invariant) is dropped.
• Not a cryptid: every step is counter arithmetic with a fixed exit.
• Proof route: opening (families (a)-(d)), then 4 explicit tail-aware SOBCv10 rounds (exceptions 6-9), then the decode trigger in exception 9, then the second counter phase (P1, P2), then a translated-cycler lemma (window above, period 919, shift 3).

Still open

• Families (a)-(d) at the real sizes (m = 30, p = n4) are still extrapolations.
• T1-T3 are checked on small instances only:
• T1 is a counting argument;
• T2 is six concrete raw-return lemmas, k = 0..5 (only k = 1..4 are used);
• T3 follows from SOBCv10's round_output_required plus a carry-shift lemma for the last column.
• The run after the trigger is a second counter phase (P1, P2 above). At the real sizes it needs its own law, a parametric sweep lemma per tick, and the race against the v and x blocks. This is the hardest new part, and the one place a different ending (another exception, or a halt) could still hide.

Wave 6, stage 2 (2026-10-14)

Goal: explain what happens after the decode trigger in exception 9, then write proof.md (Claude, about 1 h 30 of the 2 h budget).

Result: the exit is closed. Stage 1 read it as two "sweep phases", P1 and P2. They are two nested exceptions, and each one follows the same laws as the rounds. The second one overflows in a purely local way into the 919/3 cycler. proof.md is written (informal, full chain from blank to the cycler).

Tools and outputs: work/s2/ (build: gcc -O2 -o phase phase.c; gcc -O2 -o ywin ywin.c; gcc -O2 -o rside2 rside2.c).

Correction to stage 1

• What stage 1 called P1 is exception 9's own call phase (its decode). Its length (5 - k)·2^(W-1) is just T1.
• What it called P2 is the call phase of the nested exception E′ that the decode trigger starts.
• The "v block" and "x block" are SOBCv10's exception_call_left: pending calls (0010)^(2r) and finished calls (0100)^(2f+5). These are the same period-4 pattern, shifted by one cell, which is why the tokens looked swapped.

phase.c prints a tokenized tape at every long turn and groups runs by the left signature. Traces: t1.out (2 | 2,3,2) and t2.out (2 | 2,3,3).

The exit, step by step (SOBCv10 frame)

After a raw pass of an all-B counter, the word is E^(P-1) A, then E^(w_j-1) A per middle column, then E^(w_m) for the truncated last column. Its value is 2 - 2^(W+1) + S, with S = sum of 2^(offset) over the non-primary columns. So by T1, with tail level λ, the next trigger is on hash

h(λ) = (7 - λ)·2^W - S - 2

1. Decode trigger. Exception 9 (λ = 3) triggers on call h_t = 4·2^W - S - 2. By T3, n9 = h_t + c, where c ≥ 0 is SOBCv10's decoded column value, so the trigger always happens, with c calls pending.
2. E′. The trigger's raw pass is T2 with k = 5: the tail becomes U^13 B t and the last column loses another digit (25 → 24). The return finds 101 ++ X4^(2f+5) = 1010 ++ V4^(2f+4) ++ 010, which is exception_pre_left (f+1) with another far end. So E′ has n′ = f + 1 = h_t calls, and exception 9's pending calls are frozen behind it.
3. E″. E′'s counter has W - 1 digits and λ = 4, so E″ fires on E′ call h″ = 3·2^(W-1) - S - 2. That is (5/2)·2^W calls before E′ would run out.
4. Overflow (k = 6). E″'s hash walks right over the all-B counter (raw_B_forward, raw_U_to_X). From l B> B^w U^13 B t 0^inf (w ≥ 1) the machine reaches the cycler window Y in 1208 + 14(w - 1) steps and never visits l.
5. Cycler. L Y B> 0^inf → L 100 Y B> 0^inf in 919 steps for every L, never visiting L.

Checks (all PASS)

A side fact: U^13 B t with no digit before it does not reach the cycler, because the head swings far to the left. U^15 and longer do. In the real run the last column still has 24 digits at E″, so this case does not occur.

Robustness

The levels in the chain (3, -1, 4, 0) decide when the run leaves the rounds, not whether it leaves:

• k grows by one per exception, nested ones included.
• An inner exception always reaches its own trigger: it gets (8 - k)·2^W - S - 2 calls and needs (7 - k)·2^(W-1) - S - 2.
• A raw pass at k = 6 always overflows into the cycler.

So the exit comes by exception 11 at the latest. Stage 1's decodetrig2 (60/60, k = 0..5) agrees.

Status

• proof.md is written. The informal proof is complete as a chain.
• Still model-level: the four tail-aware rounds (exceptions 6-9) at real sizes, and families (b) and (d) at p = n4. These use closed forms checked on small instances and need induction proofs.
• Formalization is large: a tail-aware copy of SOBCv10's round machinery (4,234 lines upstream), plus the opening, T2 (k = 0..5), the nested launch, and Lemmas O and C.
• Not a cryptid.

Formal planning stage (2026-10-14)

Goal (Dennis answered 'plan'): put the exit in Rocq, state the tail-aware round lemma, and price the full formalization (Claude, one 2 h stage). Plan: rocq/plan.md.

Setup: rocq/cc.sh copies a file into rocq/build/ and compiles it with coqc 8.20.1 (one coqc at a time, only if fewer than 2 run system-wide). The library is the unmodified upstream SOBCv10.v (vendor 0940bb9, identical to cdaf693), compiled as W61.SOBCv10: 84 s, 0.8 GB.

Proved: rocq/W61Exit.v (366 lines, no Admitted, compiles in 2 s)

• T2, k = 0..5: base cases by direct computation (98-910 steps, left side never read), then induction on the column and on the layout (raw_tail_columns). All six base outputs agree with the stage-1 law.
• Lemma O: B U^13 B t gives 1010 Y B> 0^inf in 1208 steps (overflow_base), then any all-B layout (overflow_columns).
• Lemma C: L Y B> 0^inf gives L 100 Y B> 0^inf in 919 steps for every L (cycler_step, cycler_nonhalt). With O: exit_nonhalt.
• Nested launch: [1;0;1] *> exception_call_left c f = pre_left_far (S f) far (nested_pre_left), launch and relaunch with any far end, nested_launch, and E′'s counter run to all B (nested_counter, nested_required).
• nested_exit: from exception 9's trigger configuration, if nested_required es e <= f the machine never halts. Print Assumptions: funext only, which the baseline allows.

Stated: rocq/W61Plan.v (4 Admitted, compiles in 2 s)

• tail_round: the tail-aware round lemma, used three times.
• tail_round_trigger: the exception-9 round.
• opening and entry_pre.
• Proved from these: the four-round chain sobc_D_nonhalt (levels 3, -1, 4, 0 come from the lemma's level law; entry_level = 3 by computation), the Perm/flip bridge, and nonhalt : ~ halts tm61 c0 for our table string.
• Print Assumptions nonhalt lists exactly the four open statements.

The precondition tail_round_pre is a draft. It holds at the entry by hand and is consistent with the four rows of proof.md section 4.

Estimate

About 10 stages of 2 h (range 9-12). By stage:

• R1-R2: counter phase to the trigger with a signed last column and the tail, and T1 as an identity.
• R3-R4: T3, the decode with deficit digits, against round_output_required.
• R5: next post state and keeping the precondition.
• R6: the trigger round.
• R7-R8: the opening families and the entry facts.
• R9: inline SOBCv10 into one kill file, check_kill, write-up.

Main risk: the T3 decode with D/E digits, outside SOBCv10's A/B odometer lemmas. Fallback: explicit lemmas for the four rounds.

2026-10-16: completed funded spike

The exact blank-start theorem now passes all three unchanged kill checks, with completed kernel replays and source SHA256 cd0bfee325f897047164a4cc11325ca3e30d2acfadedf4c2abecec0a859327ca. The proof connects the opening to three returning rounds, a nested overflow, and the 919-step translated cycle. The finite safe-column budget replaces the unbounded draft invariant. Earlier proof and status are retained under rocq/. Public package: submission/proof-package.zip. The kill is locally verified; upstream submission and acceptance are separate milestones.