W6-1 · 1RB0LE_1RC---_0RD0RB_1RE0LA_1RF0LF_1LD1RF: informal proof (draft)

Internal draft for Checkpoint B (Wave 6, stage 2, 2026-10-14). Not a public write-up.

What the machine does

This machine is the SOBCv10 machine (upstream SOBCv10.v), mirrored and with its states renamed, started from SOBCv10's state D instead of A.

SOBCv10 is a counter machine. A tally next to a wall sends signals into a binary counter, one at a time. When the counter overflows, an exception turns the tally into a burst of n new signals. Each exception comes exponentially later than the one before.

From our start, the counter carries a small extra piece at its far end, called the tail. Every exception makes the tail longer. Four exceptions after the run joins SOBCv10's regime, a carry into the tail starts two nested exceptions. The second one sends the head off to the right end of the tape, and the machine becomes a translated cycler: every 919 steps it moves 3 cells, forever. So it never halts.

Everything below is written in SOBCv10's frame, with the wall on the left. Our machine is the mirror image, so in our own frame the cycler runs to the left.

0. Frame and notation

The state map from ours to SOBCv10 is A, B, C, D, E, F → D, E, F, A, B, C, together with a mirror. Under this map our start is SOBCv10's start in state D.

Words (SOBCv10 frame, read left to right):

A hash is one signal. It leaves the left end of the counter in state B moving right, and comes back in state F moving left. On its way it adds 1 to the counter, least significant digit first:

• B becomes A, and the carry moves on;
• A becomes B, D becomes A, E becomes D, and the carry stops.

A counter layout is a list of columns of digits separated by U U. The first column (the primary) has width P, the others widths w_1, ..., w_m. A column's digits sit at increasing powers of two, so column j starts at offset o_j = P + w_1 + ... + w_(j-1). W is the total number of digits.

1. Rules taken from SOBCv10.v

These are proved upstream for this table. Our proof uses them unchanged, or with a longer left side where the lemma is a side or segment lemma that does not read it.

During an exception the left side is SOBCv10's

exception_call_left r f  =  101 (0010)^(2r) (0100)^(2f+5)  [head]

with r calls still to come and f calls finished.

2. The opening: exceptions 1 to 5

Exceptions 1 to 4, exact. A hash-level simulation runs the machine exactly. Each returning hash at the wall is replaced by the proved left_emit_call, so a hash costs O(1) steps instead of O(u). It reproduces SOBCv10's own number sobc1_first_half = 13,631,486 on SOBCv10's start. On ours it gives:

At exception 4 the configuration is

W X^(2·n4+1) B>  B^30 C t C A A t t

(a) Exception 4. For m ≥ 2 and n = 3·2^(m-1) - 2:

W X^(2n+1) B> B^m C t C A^2 t^2   ->   W B> C A U^(2n) A^(m-1) D^2 A U E A

This was checked on the full tape for m = 2..5. At the real size m = 30 it was also checked exactly: the raw pass gives E^30 D A U E A, and n4 hashes into that word give A^29 D^2 A U E A.

cd. By exception_done_cd, C A U^(2n4) drains with 2(2^n4 - 1) hashes into A^n4 C A.

(b) Fossil run. For even m and p ≥ 1, the word A^p C A^m D^2 A U E A needs

H = 2^(p-1) (1292·2^m + 4)/3 - 1

hashes to reach the frontier B^(p+m+5) U B t.

(c) Exception 5 raw pass. B^w U B t becomes E^(w-1) U^3 A. This is law T2 below with k = 0.

(d) Exception 5 decode.

n5 = 2^p - 2 + 2^(p-2) (1292·2^m + 4)/3

hashes into E^(p+m+4) U^3 A give A^(p-2) digits_(m+6)(R) U^3 A t, with R = (140·2^m + 4)/3 + 4.

Entry. With m = 30 and p = n4, exception_done_ca then gives SOBCv10's post-ca state plus a tail:

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
col = 29 digits, value 391,468,375

The column meets SOBCv10's invariant: round_width_dominance, columns_schedule (width 2·14+1, value in [3, 2^29 - 6]) and columns_head_odd. The only difference from sobc1_round_invariant is the tail U^3 A t.

3. The tail and its three laws

The tail is U^(2k+1) y after the last column. Hashes pass U unchanged, so y acts as one more digit, with six levels:

A carry into the tail raises its level by one. A carry that arrives at level 4 (B t) is an exception trigger.

T1, timing

Let V be the counter's value: digits count A = 0, B = 1, D = -1, E = -2 at their powers of two, and the tail level counts at weight 2^W. Each hash adds exactly 1 to V. A trigger needs every digit at B and the tail at B t. So the trigger comes on hash number

5·2^W - V

SOBCv10's own count, without a tail, is 3·2^W - V.

Right after a raw pass, the counter word is E^(P-1) A for the primary, E^(w_j - 1) A for each middle column, and E^(w_m) for the last column, which has lost its top digit (see T2). Its value telescopes to 2 - 2^(W+1) + S, where

S = 2^(o_1) + ... + 2^(o_m)      (offsets of the non-primary columns)

So, with the tail at level λ after the raw pass, the next trigger comes on hash

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

T2, the raw pass

For 0 ≤ k ≤ 5 and any w ≥ 1, the raw pass turns

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

The last column loses its top digit and the U run grows by one pair. The left side is not read, so T2 holds inside a nested exception too. For k = 6 (U^13) the raw pass does not come back: see 5.4.

T3, the decode

Let L be the tail's effective level at post-ca: its level minus any deficit left in the last column. Then the exception's n is

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

where n_s is SOBCv10's round_next_half for the same columns and W counts the digits at post-ca. The n_s hashes decode exactly as in SOBCv10. The last column ends below 2^(w-1), so no carry reaches its top digit, which is the one the raw pass removed. The other (2 - L)·2^(W-1) hashes give 2 - L carries into the tail. If 2 - L < 0, the last column is instead left short by L - 2 levels (D or E digits).

The per-exception step

Put together:

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

4. Exceptions 6 to 9

From the entry (k = 1, L = 3):

In each row the last column stays inside SOBCv10's column_safe range. The columns born in each round are SOBCv10's z-columns, so SOBCv10's invariant covers them. Only the round parameters change, because n changes by T3.

5. The exit

Fix exception 9 after its raw pass. W is now the number of digits (the last column has 25), S is as in T1, and the tail is U^11 A t, level 3.

5.1 The decode trigger

By T1 with λ = 3, the trigger comes on call

h_t = 4·2^W - S - 2

By T3, n9 = n_s + 2·2^W. SOBCv10's decode of n_s ends at a column value c ≥ 0, so n_s = c - (2 - 2^(W+1) + S). Hence

n9 = h_t + c >= h_t

so the trigger really happens, with c calls still pending.

At that moment the counter is all B, the tail is U^11 B t, and the left side is exception_call_left c (h_t - 1). The trigger hash starts a nested exception E′.

5.2 The nested exception E′

The trigger hash makes a raw pass. By T2 with k = 5, the counter becomes the usual E/A word, the last column drops to 24 digits, and the tail becomes U^13 B t (level 4).

The pass returns to the left end of the counter in state F, with 101 in front of the old call region. Since

101 ++ X4^(2f+5)  =  1010 ++ V4^(2f+4) ++ 010     (as lists read away from the head)

this is SOBCv10's exception_pre_left (f+1) with a different far end. Here f = h_t - 1. exception_launch and exception_relaunches only touch the near end, so E′ has n′ = h_t calls. The far end (the c pending calls of exception 9) is never reached.

5.3 E″ fires before E′ runs out

E′'s calls feed its counter, now with W - 1 digits and the same S. By T1 with λ = 4, the next trigger E″ comes on E′ call

h'' = 3·2^(W-1) - S - 2

and

n' - h'' = 4·2^W - 3·2^(W-1) = (5/2)·2^W > 0

So E″ fires while E′ still has about (5/2)·2^W calls left.

5.4 E″ overflows, and only the right end matters

When E″'s trigger hash leaves, the configuration is

l  B>  B^P U^2 B^(w_1) ... U^2 B^24  U^13 B t  0^inf

where l is everything to the left (E′'s call region and all older blocks).

The hash walks right over the columns by raw_B_forward and raw_U_to_X; these lemmas hold for every left side. Then:

Lemma O (overflow). For every left side l and every w ≥ 1,

l  B>  B^w U^13 B t  0^inf

reaches, in 1208 + 14(w - 1) steps, a configuration whose last 70 written cells are

Y = 1000100010001000100010001000100010010001000100010001000100010010100100

with the head on the next cell in state B and blank beyond. On the way it never visits a cell left of its start, so l is untouched.

The condition w ≥ 1 matters. With no B before U^13, the head swings far to the left. Here w = 24.

5.5 The translated cycler

Lemma C. For every left part L,

L Y B> 0^inf    ->(919 steps)->    L 100 Y B> 0^inf

and these 919 steps never visit L or the first 3 cells of Y.

By induction the machine moves right forever, 3 cells per 919 steps, so it never halts. In our frame this is the mirror image: head in our state E, moving left.

6. Why the exit is robust

The exact levels in section 4 decide when the run leaves the SOBCv10 rounds, not whether it leaves.

• k grows by one at every exception, nested ones included.
• A nested exception never runs out of calls before its own trigger. If the outer exception has tail index k (level k - 1 after its raw pass), the inner one gets (8 - k)·2^W - S - 2 calls and needs (7 - k)·2^(W-1) - S - 2. The difference is (9 - k)·2^(W-1) > 0 for every k ≤ 5.
• A raw pass with k = 6 always ends in this cycler, if the last column has a digit.
• k ≥ 7 also does, even with no digit before the U run.

So if a level in section 4 were off by one, the exit would only move, at the latest to the raw pass of exception 11.

7. Status of each step

Formal work still needed:

• a tail-aware version of SOBCv10's round lemma, used four times;
• the opening families (a)-(d) as lemmas;
• T2 for k = 0..5;
• the nested launch;
• Lemmas O and C.

The upstream SOBCv10.v is 4,234 lines. Most of it would be reused, but the tail runs through the round invariant, so this is a large formalization.

AI assistance: written by Claude (Anthropic).