1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB: never halts (informal proof, OPEN)

• Machine: 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB, viewer https://bbchallenge.org/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB
• Sheet: Results row 918, class "Sync bouncer counter"; no status, notes, links or Discord thread.
• Written for: the string itself (no mirror, no renaming).
• Status: complete at the informal level, OPEN for formalisation.
• Every rule is either (a) a window lemma, checked by one finite run that never reads outside its window, so it holds in every context; (b) a parametric rule with its proof written out as a chain of (a) and earlier rules; or (c) a finite table that is checked exhaustively: the tail table T(f) of §4.2, 16,384 entries.
• What is not written out by hand: the 16,384 entries of T(f) and the TAILFRONT/closure facts derived from them (§4.5). These are finite computations, re-run by check_proof.py check 5 and check 6. Formalising them is the hard part of the lemma plan (§9).
• Evidence: check_proof.py (§8), 9 checks.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

     0    1
A   1RB  0LF
B   0RC  ---        halting transition: B reads 1
C   1RD  0RA
D   1LE  0RC
E   0LA  0LE
F   1LE  1LB

0. Overview

The tape right of the head is a binary counter written in three tokens, 00, 01 and Z = 100. A digit is b Z 01 Z^g, where b is 00 (bit 0) or 01 (bit 1) and g is the gap to the next digit. The head bounces off the left end, and every bounce adds 1 to the counter (rule Inc, §2).

At the right end of the counter there is a block of gap-1 digits (the R block) followed by a finite-state "tail" W. When the counter overflows, the carry runs into the tail. The tail answers in one of two ways, decided by a finite table: - S (silent): the counter wraps to 0 and nothing else happens. - N: the whole left part of the tape freezes into a "wall". The machine then spends a long pause eating the wall two increments at a time (§3), rebuilding every gap exactly and possibly inserting new digits.

The proof has four layers: 1. Window lemmas and the parametric counter rules (§2–§3). 2. The overflow: a right sweep, the tail table, a return sweep whose parity decides N or S, and a parametric rule for the tail's growing end (§4). 3. A finite fact about the tail (TAILFRONT): its 2-bit front unit cycles 10 → 01 → 11 → 00 → 10, and S can only happen at 11 (§4.5). 4. Linear arithmetic on the counter parameters: an interval invariant at normal-mode overflows that holds whatever the tail chooses at each 11 slot (§5).

1. Notation and families

1.1 Tape notation

• 0^inf u X> v 0^inf: state X reads the first cell of v. u <X v: state X reads the last cell of u.
• Window lemma u <X v → <Y u'v' (or → u'v' Y>): started with the head on the last cell of u (or the first cell of v), the run stays inside the |u|+|v| cells and leaves them on the stated side in state Y. Such a lemma holds in every context.
• Inner record (IR): A reads a 0 that it reached moving left, and the cells from the head on read (001)^p 00 0b10001. All macro rules go from one IR to the next. Note that (001)^p 00 = 00 Z^p.
• Z = 100. A digit is d(b) = 0b10001 = b' Z 01 with b' = 0b. A counter is D_G(v) = d(b_0) Z^(g_1) d(b_1) Z^(g_2) ... d(b_(N-1)), with v = Σ b_i 2^i (LSB leftmost).
• Zn(g) := (010)^(g+1) is a zone: a gap g frozen into the wall.

1.2 The right counter RC and the tail

• At every configuration we use, the counter has this form:
• k ≥ 0 large-gap digits d_0..d_(k-1), with gaps G = (g_1..g_k), every g_i ≥ 7;
• then the gap-2 digit, followed by the gap Z^2;
• then the R block U^q, where U = 01100 = 01 Z and q = 2r + H. In digit terms this is r gap-1 digits 0110001100 plus a half digit H ∈ {0,1}.
• The number of counter digits is N = k + 1 + r + H.
• The tail is W(f, e) := F(f) (0e_1)(0e_2)...(0e_m) 01, where F(f) = 0x0y0z10001 0?0?10001 0?1000?10001 0?0?1000?10001 0?1000?1000?1000?1000?10001 (75 cells).
• f is the 15 bits at the ? places, read left to right; x, y, z are the first three of them.
• The end unit has m ≥ 0 bits e_1..e_m and the end marker 01.
• The front unit is (y, z).
• L* := the tails with x = 1 and H = y.

1.3 Families

• K_N(a; D; RC) := 0^inf A>(001)^a 00 D RC (normal mode, lead a).
• K_P(Wall; p; D; RC) := 0^inf Wall A>(001)^p 00 D RC (pause mode, inner lead p).
• X(a; G; r, H; f, e) := K_N(a; all bits 1; ...) with the counter of §1.2 and a tail in L*. This is a normal-mode overflow configuration: 0^inf A>(001)^a 00 [0110001 Z^(g_i)]_(i=1..k) 0110001 Z^2 U^(2r+H) W(f, e).
• The invariant set is the configurations X that satisfy INV (§5.3).

2. Window lemmas and the counter

2.1 Window lemmas (check 2: exact result, exit and step count)

Shift rules, by induction from R4, L1 and L4: C> Z^n → (010)^n C> (3n steps), (010)^n <E → <E Z^n (3n), Z^n <F → <F (001)^n (3n). R2 followed by R4^a is the old shift A> (001)^a 00 → (100)^a 10 C>.

2.2 Rule Inc_L (check 3)

Inc_L. For every left half-tape L, every a ≥ 0 and every counter D_G(v) with v + 1 < 2^N:

L A>(001)^a 00 D_G(v) T → L <F (001)^a 00 D_G(v+1) T, in 6a + 6S_j + 24j + 7 steps.

Here j = the number of trailing 1 bits of v (b_0..b_(j-1) = 1, b_j = 0) and S_j = g_1 + ... + g_j. The head never reads L before the last step, so L is arbitrary. T is arbitrary too, because the run never reads past d_j.

Proof, in order: 1. R2, R4^a. 2. For i = 0..j-1: R3 on d_i, then R4^(g_(i+1)). 3. R5 on d_j. 4. For i = j-1 down to 0: L1^(g_(i+1)), then L2 on the processed d_i. 5. L1^a, then L3.

The step total is 2 + 3a + Σ(7 + 3g) + 3 + Σ(3g + 17) + 3a + 2. In this argument j ranges over 0..N-1, and the proof is by induction on j (the carry depth), like Climb/E_stmt in CounterClass3v2 TM1.

2.3 Rule Inc

Inc. K_N(a; D_G(v); T) → K_N(a+1; D_G(v+1); T) for v + 1 < 2^N, in 6a + 6S_j + 24j + 9 steps.

Proof: Inc_L with L = 0^inf, then END. 0^inf 00 <F → 0^inf <A 01 leaves A reading a 0 that it reached moving left, with 0 01 (001)^a 00 = (001)^(a+1) 00 on its right.

3. Pause rules (check 4: exact whole tape at the next IR, exact steps)

Each pause rule has the shape Inc_L, then (if two increments) B1 and Inc_L again, then a left-end lemma that ends at the next IR. In every rule b_0 = 0 (v even), so the first Inc_L has j = 0 (6p + 7 steps). j and S below belong to the second increment.

D_(g,G)(2u) is the counter with a new LSB digit 0 at gap g in front of the old digits, so its value is 2u.

In ZX/ZXN the second Inc_L ends with F on the last cell of a wall that ends ...010 010 100 100 (ZX) or ...0 100 10100100 (ZXN). In both cases the last 12 cells are 010010100100, and ENDZX (22 steps, L4 twice inside it) turns them into 000100011001. A then reads the 13th cell from the end, which is 0, so this is an IR. That needs h ≥ 3 (ZX) or n ≥ 2 (ZXN). The right side reads 0 000100011001 (001)^p 00 d_0... = 00 0010001 Z^(p+2) d_0..., because 1001 (001)^p 00 = Z^(p+2). ZXP2 ends with BN on the last 6 cells 010010 of (100)^n 10 plus the 00 of the first 001. A then reads the middle cell of block n−1, so n ≥ 2 is needed.

The domains above are wider than what the run needs: Y and the walls are arbitrary words of the stated shape. The check ran them with random walls, random p ≤ 200, gaps ≤ 60 and ≤ 6 digits.

4. The overflow

4.1 Right sweep (OvR)

Start from X(a; G; r, H; f, e), or from the second increment of a P-cycle in pause mode (left context (100)^(n-1) 1000 after B1). The carry passes every digit:

R2, R4^a, [R3, R4^(g_i)] for i = 1..k, R3 (gap-2 digit), R4^2, then (R6, R4)^q over the R block.

C now stands on the first cell of F(f), and every token to its left is processed: 00→10, 01→10, Z→010.

4.2 The tail table T(f) (check 5)

For each of the 16,384 fixed parts f with x = 1, run the window C> F(f) (75 cells): - For f ≠ 1^15 the head leaves the window on the left, in state σ(f) ∈ {E, F}, without reading the end unit. Counts: y = 0: F (8192); y = 1: E (6581) or F (1610). - For f = 1^15 the head leaves on the right in state C after 73 steps (CF1). This is ENDCARRY, §4.4.

So T(f) is a finite set of window lemmas C> F(f) → <σ(f) F'(f). They hold for every m, every end-bit setting and every left context.

4.3 Return through the R block, and the boundary

The q processed units 10010 are restored one by one from the right: UE turns E into F, and UF turns F into E. Both write 00100, and UF also turns the first token of the unit to its right into 01. UF needs that token to be 00, and it is: the unit to the right was just restored, or F'(f) starts with 00 when σ = F (check 5, all f). The case analysis: UF at unit i runs only when unit i+1 was restored by UE, or when i = q and σ = F. BN runs only when unit 1 was restored by UE. The full composition is check 6.

After the q units the mode is σ(f) if q is even, and the other state if q is odd. Call it μ.

• μ = F → N. The head is on the processed Z Z of the gap-2 digit, with 00 on its right. BN gives <A 00010001. A reads the last cell of the processed gap-2 digit, which is 0: an IR with lead 0.
• From normal mode this is rule NO: X(a; G; r, H; f, e) → 0^inf (100)^a 101001 [Zn(g_i) 1001]_(i=1..k) 01 A> 00 RC'. This is just the processed left part read as a wall: (100)^a 10 [1001010 (010)^(g_i)]_i 100101.
• From pause mode it is rule PO: 0^inf (100)^n 1 A>(001)^p 00 D(2^N-2) RC → 0^inf (100)^n Zn(p) 1001 [Zn(g_i) 1001]_i 01 A> 00 RC'. This comes from Inc_L(j = 0), B1, then OvR with left context (100)^(n-1) 1000.
• μ = E → S. BS restores the gap-2 digit. Then [L1^(g_i), L2] for i = k..1, then L1^a and L3 bring F to the cell left of the lead, as in Inc_L.
• From normal mode, END gives rule SILENT: X(...) → K_N(a+1; D_G(0); RC') with the gap-2 digit kept. The counter wraps and there is no pause.
• From pause mode, END gives rule SILENTP: (100)^n 1 A>(001)^p 00 D(2^N-2) → (100)^(n-1) 1 A>(001)^(p+1) 00 D(0), for n ≥ 1.
• In both cases RC' is the restored R block followed by F'(f) and the untouched end unit. Parsed again (with its bits set, as at the next overflow), it reads U^(2r'+H') W(f', e) with m unchanged. The emission is e = (r'+H') − (r+H).

Class rule: N ⇔ μ = F. Check 6 recomputes this class for every f and compares it with the full simulation.

4.4 ENDCARRY (f = 1^15; check 7)

After CF1, C reads the end unit (0e_1)...(0e_m) 01. Let j = the number of leading 1s of e, with j := m + 1 when all m bits are 1 (the end marker 01 then counts as one more 1, and R7 writes a new marker on the blank cells, so m grows by 1).

R6^j, R7, then the processed tokens are restored right to left by alternating L3 (E→F, gives 00) and L3F (F→E, gives 01). The mode at the left end of the end unit is E for even j and F for odd j. Then PEN or PFN, then §4.3 with q = 2r + 1 (H = y = 1): - j even: N, end bits become (10)^(j/2) 1 rest, f' = 100100010001010, H' = 0; - j odd: S, end bits become (01)^((j+1)/2) rest, f' = 110000100100101, H' = 1. PFN leaves x = 0, and the UF on the H unit sets x = 1 again. - The emission is e0 in both cases.

4.5 TAILFRONT and closure of L* (check 6, exhaustive)

For every tail in L* and every r, a, G, in normal or pause context, the overflow is N or S with exactly the forms above. The new tail is again in L*, with m' = m except in the ENDCARRY growth case. The front unit and the emission follow:

TAILFRONT:   10 -N,e0-> 01 -N,e1-> 11 -N,e0-> 00 -N,e1-> 10,     11 -S,e0-> 10

S occurs only from front unit 11. The finite part (f ≠ 1^15) is the T(f) table plus the parity rule of §4.3, and check 6 runs it for all 16,384 f at two (r, a, G) settings. The f = 1^15 part is ENDCARRY.

Independence from r, a, G and from the left context follows from the decomposition: T(f) is a window lemma, and everything else is parametric. Check 6 also compares PO/SILENTP with NO/SILENT on 200 random tails: the new RC is the same.

5. Macro dynamics and the invariant

5.1 Quantities at a configuration X(a; G; r, H; f, e)

• R := r + H, N = k + 1 + R, M = 2^N;
• Γ := Σ_(i=1..k) (g_i − 1)·2^(i−1);
• c := 2^(k+R) − 2^(k+1) − 2Γ − 4;
• s := a − c, κ := c − M/4.

5.2 One overflow and its pause, in closed form (proof.md rules only)

After NO with emission e: R' = R + e and M' = 2^e·M. - The first ZX (p = 0) creates the gap-2 digit. The zones are then rebuilt innermost first: for each zone, (g − 2) P010 cycles, then ZX (ZXN for the last one). Every gap is restored exactly. - After ZXN the counter value is v_0 = 2^(k+2) + 4Γ, the wall is (100)^(a−2) 1 and the lead is 0. - The pause then runs P100 cycles (+2 each). The next overflow slot comes after c' = (M' − 2 − v_0)/2 cycles; for e = 0 this is c' = c + 3. - If c' ≤ a − 2, the slot is reached in pause mode (a PO slot) with p = c', wall a − 2 − c'. Otherwise WX ends the pause and Inc runs to the next normal-mode overflow.

After PO at inner lead p with emission e: the zones of G are rebuilt as above. Then the zone Zn(p): (p − 2) P010 cycles, then ZXP1 and ZXP2, which inserts the new gap p − 1. The wall drops by 3. The value is 2(v_G + 2(p−2) + 2) + 2.

The four paths between consecutive normal-mode overflows, starting from front unit f. Each is a composition of the rules above (algebra below, all in terms of M and s):

The algebra: - S: SILENT gives lead a + 1 and counter 0. Then M − 1 Incs reach the next overflow at a + M, with G and R unchanged. - NO e0: p = c + 3, so PO#1 has wall s − 5 and inner lead p = c + 3. - PO#1 (e1): G'' = (c+2) ∪ G, R'' = R + 1, M'' = 4M. Using 2p = M − 2^(k+2) − 4Γ − 2, the value after ZXP2 is v_1 = 2M − 6. The wall is s − 8 and the lead 0. - The next slot comes after (4M − 2 − v_1)/2 = M + 2 cycles. - If s − 8 < M + 2: WX gives lead s − 7 and value v_1 + 2(s − 7). The next overflow is at a'' = 2M + 12 − s. With the new gaps, c'' = M + 2 (so κ'' = 2) and s'' = M + 10 − s. This is P1. - Otherwise PO#2 is reached at p = M + 2 with wall s − M − 10. Its front unit is 11. - S at PO#2 (SILENTP): p = M + 3, wall s − M − 11, value 0. The next slot is 2M − 1 cycles away, more than the wall, so WX gives lead s − 7 and value 2(s − M − 10). Then a'' = 6M + 12 − s and s'' = 5M + 10 − s. This is P1S. - e0 at PO#2: gap M + 1 is inserted, M''' = 8M, value 8M − 18, wall s − M − 13. The next slot is 8 cycles away: PO#3 at p = 8 with wall s − M − 21. Its front unit is 00, so the outcome is e1. - PO#3 (e1): gap 7 is inserted, M4 = 32M, value 16M − 18, wall s − M − 24. The next slot is 8M + 8 cycles away, more than the wall, so WX follows. Then a'' = 17M + 40 − s, c'' = 8M + 8 (κ = 8) and s'' = 9M + 32 − s. This is P3.

5.3 The invariant

INV at a configuration X: κ ∈ {2, 8}, all gaps ≥ 7, tail in L*, and

• f = 11 and 24 ≤ s ≤ M/4 + 2, or
• f = 10 and s ∈ [8, M − 14] ∪ [M + 24, 2M].

Which path runs (front unit and s decide; at a 11 slot both choices are covered):

Closure (images of the interval end points; every map has slope ±1; check 9b, exact, N = 8..400):

Side conditions that keep every rule inside its domain (check 9c, using M ≥ 256 and c = M/4 + κ ≥ 66): - NO: a = s + c ≥ 74 ≥ 2. - PO#1: p = c + 3 ≥ 69 and wall s − 5 ≥ 3. - PO#2: p = M + 2 and wall s − M − 10 ≥ 14. - PO#3: p = 8 and wall s − M − 21 ≥ 3. - SILENTP: wall ≥ 14 ≥ 1. - New gaps c + 2 ≥ 68, M + 1 and 7 are all ≥ 7, so every ZX zone has ≥ 3 blocks. - The rebuild never overflows. Let slack_i = the number of P-cycles left before the overflow slot after the i-th zone. Then slack_i = (slack_(i+1) + 2g − 3)/2. The final slack is c' ≥ 69, so every earlier slack is ≥ g − 1: the P010 cycles and the ZX of zone g fit. No carry reaches the tail during a rebuild. - S inside a pause happens only at PO#2. PO#1 and PO#3 have front unit 01 or 00. After SILENTP the wall (< M) runs out before the next slot (2M − 1 cycles).

Check 9a compares the closed forms with the event-level model (scripts/deepen3_macro.py, built from the rules of §2–§4 only) on random front-unit sequences: every transition matches, with no other path. Check 9d runs a DFS over all front-unit sequences.

6. Initial segment (check 8)

The first configuration in X ∩ INV is reached by direct simulation from the blank tape in 92,299 steps:

0^inf A>(001)^121 00 0110001 Z^28 0110001 Z^2 (0110001100)^5 01100 W(111111011110101, 010)

So a = 121, G = (28,), r = 5, H = 1, R = 6, N = 8, M = 256. The tail is in L* with m = 3, x = 1, H = y = 1, and the front unit is 11. Further c = 66, s = 55 ∈ [24, 66] and κ = 2.

Earlier all-ones normal-mode records exist (steps 230 … 17,206). Some are X-configurations outside INV, for example step 5,786 with G = () and s = 3. The proof does not use them: the initial segment is the exact 92,299-step run.

7. Conclusion

• Coverage. Every member of the invariant set takes one of the paths S, P1, P1S, P3, whatever the tail chooses at each 11 slot. Each path is a finite composition of rules (Inc, SILENT, NO, PO, SILENTP, P100, WX, P010, ZX, ZXN, ZXP1, ZXP2), each applied inside its domain (§5.3). Each path lands in the invariant set again. So the run never leaves the rule system.
• Progress. Every rule takes at least 2 steps, so each path takes at least 1 step: progress_nonhalt_cond applies with P = INV.
• Halting. The only halting transition is B reading 1, and B is entered only by A0 (1RB) and F1 (1LB). A halt would need the pattern A> 0 1 or a 1 directly left of an F that reads 1.
• Every rule above is an exact composition of window lemmas, finite table entries (T(f)) and parametric chains of them, and each of these runs to its stated end without halting (checks 2, 3, 5).
• So no halting transition is ever executed on the path from the blank tape: the initial segment (check 8) is an exact halt-free run, and after it only rules are used.
• Sanity reading: A0 and F1 fire only inside the window lemmas and the T(f) runs, and in each of these finite runs the following B reads 0 (it never halts). The typical cases are R2 (A0 on the left cell of a 00 token) and B1 (F1 on the 1 of a wall's 01 end, whose left neighbour is 0).

8. Evidence: check_proof.py

Run as python3 -B check_proof.py [--quick]; the log is work/check_proof.full.log.

The earlier stages also have this evidence, listed in notes.md: - rules 1050/1050 (scripts/deepen_rules.py); - the macro model reproduces the real run exactly to step 555,048,797; - 40,000 overflows of the RC chain; - closure for all bit settings with m ≤ 8 (scripts/deepen3_closure.c).

9. Lemma plan (Rocq)

No family template applies (SBCv2_6x2 tm108 was ruled out in the observe pass). The nearest pattern is CounterClass3v2.v, Module TM1: a hand-written multi-level counter with sweep lemmas, an E_stmt j induction on carry depth (E_all), Climb/Climbs, and Mac_* macro lemmas. Plan:

1. Tape words. Define Z, digits, D_G(v) as a function of a list of (bit, gap), Zn, U, and W(f, e) as list Sym. Prove lpow-style rewriting lemmas, copying lpow_* from TM1.
2. Window lemmas (§2.1): each is one es. The shift rules follow by ind on R4, L1 and L4.
3. Inc_L: induction on the carry depth j over the digit list. The statement is quantified over l (left side) and r, like TM1's E_stmt.
4. Pause rules: short follow chains (Inc_L, B1, Inc_L, END / ENDZX / BN).
5. Overflow, split as in §4: - OvR by follow/ind over digits and units; - T(f): the hard part, 16,383 window lemmas; - the R-block return by induction on q with a mode parameter (UE/UF); - BN/BS; - ENDCARRY by induction on j (L3/L3F alternation).

Options for T(f), cheapest first: - (a) Prove one generic lemma forall f in L*\{1^15}, exists ... by a boolean checker over Fin 2^14 evaluated with vm_compute/native_compute, using a verified step function on lists. A home-made checker must be proved sound against TM.step, so this is a medium-size Rocq development. - (b) Split F(f) into its five units and prove per-unit sweep lemmas over tokens. This would replace the table with about 40 lemmas, but the decomposition has not been worked out. The tail's units are made of the same tokens, and T(f) behaves like a mixed-radix counter with carries, but the per-unit lemmas are not yet derived. - (c) 16k separate es lemmas, generated. Probably too slow. 6. TAILFRONT and closure: another finite fact over f, derived from the T(f) results plus the parity rule. It is proved together with (5a), or (5b). 7. Macro arithmetic: a Definition of the invariant on (a, G, R, f, e) as in §5.3, with the path lemmas as Mac_*-style compositions. lia handles the linear parts; powers of 2 enter as M (keep M = 2^N abstract and record only M ≥ 256, M divisible by 4). Never run CTL/NG-style searches inside Rocq. 8. init by solve_init (92,299 steps), then nonhalt via progress_nonhalt_cond, with P = INV plus the family shape.

10. Gaps (what a reviewer should still look at)

• T(f) and TAILFRONT are verified by exhaustive computation, not by hand. This is legitimate for a finite fact, but in Rocq it needs (5a) or (5b).
• The R-block alternation and the boundary lemmas were derived by hand (§4.3), and check 6 confirms them for all f at two parameter settings plus 200 random pause-context cases. The written induction over q is short, but it is only sketched here.
• The closed-form path algebra of §5.2 was derived by hand and checked against the event-level model (check 9a: every transition exact). The event model itself uses the rules of §2–§4 and was checked against the real run in the earlier stages (exact to step 5.55e8).
• No step-count closed form for NO/PO/SILENT/SILENTP: it depends on the T(f) step count. It is not needed: progress only needs ≥ 1 step per rule.

Review log

• 2026-10-10 (informal_proof stage, first version).
• Built from the deepen-round results. New in this stage:
  • the token view and the full window-lemma set (§2.1);
  • Inc_L with a parametric proof;
  • every pause rule as an Inc_L/B1/END chain (ZX/ZXN share the 22-step ENDZX, and ZXP2 uses the overflow's BN);
  • T(f) is a context-free window lemma table: the head never reads the end unit unless f = 1^15. This replaces the round-3 "locality" observation with a proof by finite run;
  • the N/S decision is the parity of the UE/UF alternation over the R block (check 6: class = parity prediction for every f);
  • ENDCARRY decomposed into CF1, the L3/L3F alternation and PEN/PFN;
  • the path closed forms S/P1/P1S/P3 derived by hand (§5.2), including κ' = 2 after P1/P1S and κ' = 8 after P3.
• Corrections to round 3:
  • The first configuration in the invariant set is at step 92,299 (a = 121, r = 5, H = 1), not "the step-36,124 state". The round-3 START is the macro state of the first overflow after step 36,124, and it is the same configuration.
  • The ENDCARRY S case leaves x = 0 after PFN; the UF on the H unit restores x = 1.
• Open: the formalisation route for T(f) (§9 step 5). Checkpoint B not yet reviewed.