1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---: never halts? (informal proof, STUCK on one lemma, cryptid-like)

• Machine: 1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---, viewer https://bbchallenge.org/1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---
• Sheet: Results tab, no status, notes or sources; struck in Direct Simulation col D (simulated to 1e15). Not in either Discord list; no thread. Trio twins #21 1RB0LC_1LA0RE_0RD0LA_1RE1RA_0LD1RF_0RB--- and #22 1RB1RC_0LA1RF_1RD0LE_1LC0RB_0RA0LC_0RD--- (see notes.md).
• Written for: the string itself (no mirror, no renaming).
• Status: STUCK, and not a non-halting proof. The rule table is complete. Every rule is checked by simulation, and the right sweep is derived. The right-part invariant is proved, and so is the clause P_k that replaces the old O1 (§3.1). One lemma is open and fatal: the absorption safety predicate Safe (§3.3, formerly O2) has no known inductive strengthening. Safety at absorptions comes down to the left counter avoiding a sparse set of values at sparse times. On the real trajectory the narrowest miss was 2 sweeps from a configuration that halts (§3.4). This meets the cryptid protocol (§5.3) and is flagged for Dennis.
• Rule derivations still owed (major): the left turnaround L and the absorption rules ABS1/ABS0/ABSO1 are checked, not derived (§2.3, §2.4).
• AI assistance: written by Claude (Anthropic) under Dennis's direction. Checkpoint B pending, non-blocking. The review of 2026-10-10 is in §9.

     0    1
A   1RB  0LC
B   1LA  0RE
C   0RD  1LF
D   1LC  1LB
E   0LD  0RB
F   0LA  ---        halting transition: F reads 1

0. Where each piece stands

1. Notation and family

Tokens. Cell strings 0 = 00, 1 = 10, O = 100, I = 110. Every token ends in a 0 cell. A token word has a unique parse: a 1 followed by an odd run of 0s starts 1, an even run starts O, and 11 starts I. O and I are called markers; as bits, 0, O are 0 and 1, I are 1.

The background block is B = 10110 = 1 I. Its partner is C = 11010 = I 1. A right-counter digit is I (bit 1) or O (bit 0). The right end is T = 11 0^inf.

Family (a "departure").

Dep(w; g; d_1..d_k; G_1..G_k) := 0^inf  w  E>  (1 I)^g  d_1 (1 I)^G_1  d_2 (1 I)^G_2 ... d_k (1 I)^G_k  T

• w is a token word (the left word), written left to right; w = u t with t its last token. w may be empty (§2, strip).
• D = d_1..d_k is a little-endian binary counter (d_1 least significant); G_i is the gap after d_i.
• On cells: 0^inf w E> (10110)^g d_1 (10110)^G_1 ... d_k (10110)^G_k 11 0^inf.
• Derived quantities: H_0 = g − d_1 and H_i = G_i − d_(i+1) for 1 ≤ i ≤ k (with d_(k+1) := 0). At an absorption, h_1 := H_1.
• Sweeps to the next absorption: τ := 2g − 1 − d_1 (g after strip). One GEN sweep lowers τ by 1, each strip raises it by 2, and an absorption is exactly a departure with τ = 0 (g = 1, d_1 = 1).

Strip (re-reading, no steps). If w = x I 1, the tail I 1 is a C block. The returning F turns it into B (W5), so Dep(x I 1; g; ..) behaves exactly like Dep(x; g+1; ..) in the next sweep. All rules below are stated for stripped words (w not ending in I 1). A strip can leave the empty word (O 1 →GEN I 1 → ''; ABS1 on O 1 1 gives I 1 → ''). It does so only while raising g to ≥ 2, so the next sweep is a GEN.

2. Rules

In busycoq comment-block style. E> = head in state E on the next cell; <F = head in state F on the previous cell (busycoq {{E}}>, <{{F}}).

1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---

start from Dep(10O011; 2; 1 1; 1 0)                         (step 2,033, §4)

inc   (right counter +1, d_1..d_(j-1) = 1, d_j = 0 first zero):
        d_1..d_(j-1) := 0, d_j := 1; if j >= 2: g := g-1, G_(j-1) := G_(j-1)+1
      all ones: every digit := 0, g := g-1, append two digits 0 with gaps 0
inc_L (left word "+2"; w = u t, u = v 1^k with k maximal):
        v = ''   -> 1 0^k t                     (left edge grows by one token)
        v = x 0  -> x 1 0^k t
        v = x O  -> x I 0^k t
        v = x I  -> inc_L(x) O 0^(k-1) t 1   (k >= 1);   inc_L(x) O 1   (k = 0)
        inc_L('') = 1 0                         (also covers w = '' after a strip)

GEN   (g >= 2, or d_1 = 0):   Dep(w; g; D; G) --> Dep(inc_L(w); inc(g, D, G))
ABS1  (g = 1, d_1 = 1, w = u 1, w not ending in O 1; u may be empty):
        Dep(w; 1; D; G) --> Dep(drop_last(inc_L(inc_L(w))); inc(G_1 + 2, d_2..d_k, G_2..G_k))
        (u empty: w = 1 -> 1 1 -> 1 0 1 -> w' = 1 0)
ABS0  (g = 1, d_1 = 1, w = u 0):
        u = v 0 1^k (k >= 1)     ->  w' = v 1 0^(k-1) O 1 1
        u = 1^k (k >= 1)         ->  w' = 1 0^(k-1) O 1 1         (left edge: the 0 is blank tape)
        u = v 0 1^k 0 (k >= 0)   ->  w' = v O 0^(k+1) 1 1
        u = 1^k 0 (k >= 0)       ->  w' = O 0^(k+1) 1 1           (left edge)
        Dep(w; 1; D; G) --> Dep(w'; inc(G_1 + 1, d_2..d_k, G_2..G_k))
        undefined ("ABS0?") when the token in front of the 1-run is a marker
ABSO1 (g = 1, d_1 = 1, w = x O 1):
        (0, D', G') := inc(1, D, G);  Dep(w; 1; D; G) --> Dep(inc_L(x); 1; 1 d'_2..d'_k'; G')

inc and inc_L are total on their domains. ABS0 is the only partial rule. Code: scripts/deepen/model3.py, linc.py (Python), scripts/review/absmodel.c (C).

2.1 Token window lemmas

A window lemma w → w' runs the stated number of steps without reading a cell outside w (the last step may move the head onto a neighbour), so it holds in every context. Each is checked by an exact finite run (check A); for these finite runs that check is the proof.

2.2 Right sweep (derived)

• Pass. From x_1 = 1: W1 on x_1, then for each next token W2 (if I) or W1 (if 1). The carried 1 always sits just left of E. The pass rotates the token segment by one: E> x_1 x_2 .. x_m → x_2 .. x_m x_1 E>. On blocks: R1 E> B^n → C^n E>, 17n steps (n uses of W1+W2).
• Turn. At the first digit O: W3. At T: W4.
• Return. F re-pairs from the right: W5 on each I 1, W6 on each unpaired I (a carried digit). On blocks: R2 C^n <F → <F B^n, 9n steps.
• Composed (check B, exact output and step count on random parameters):

R3–R5 are exactly inc on (g, D, G). F ends on the last cell of w (a 0), or on blank tape if w is empty.

2.3 Left turnaround L (checked, not derived)

L. Let w be a stripped word in the domain: the empty word, or first token not 0, last token 0 or 1, and markers pairwise ≥ 3 tokens apart. Let ρ be any right context whose first two cells are 1, 0, i.e. one that starts with a 1 token or an O token. Then:

0^inf w <F ρ   -->   0^inf inc_L(w) E> ρ

• The head reads no cell right of w, except on an I-crossing with t = 0 (tail I 1^k 0). There it reads exactly the two cells 1, 0 of ρ and restores them.
• In GEN, ρ = (1 I)^g ... (g ≥ 1). Inside ABS, ρ starts with O, the cleared d_1 (§2.4). Both satisfy the precondition.
• The precondition is sharp. With an I (cells 110) right of w, every one of the 1,735 t = 0 I-crossing words of length ≤ 9 comes out differently from inc_L.
• Check C: all 13,184 domain words of length ≤ 9, the empty word included, give exactly inc_L(w) with three contexts ρ (1 I, O 1 I, 1 O). Outside the domain (adjacent markers, I 1 I) the machine differs on 17,066 of 101,504 words.
• A random review run (8,000 words of up to 60 tokens with up to 11 markers, at spacing 3 and at spacing 4) was also all exact.

Mechanism (from traces): - start. F0 0LA puts A on the bit cell of t. A short gadget restores t. It leaves A on the bit cell of the token left of t, with that token's 0 cell holding a temporary 1. The gadget takes 7 steps for t = 1 (F0 A1 C0 D0 C0 D1 B0) and 9 for t = 0 (F0 A0 B0 A1 C0 D0 C0 D1 B0). - carry. On a 1 token, A runs a 6-step loop (A1 C0 D0 C0 D1 B0) and moves one token left; the passed token becomes 11. - stop. At 0: A0 1RB, and the token becomes 1. At O: it becomes I. At the left edge: a new 1 token. - return. E and B run right (E1 0RB, B1 0RE), clearing each 11 to 00. E stops on the first cell after w. - I-crossing. At I, C1 1LF creates F on the last cell of the token left of the I (a 0), and the turnaround restarts on x. Then the return writes O 0^(k−1) t 1.

Steps: 8k + 13 for marker-free words, where k is the number of trailing 1s of u (check C). Words with markers: no formula is derived yet.

Owed (major). The start/carry/stop/return/crossing pieces as window lemmas, with an induction on the carry length and a recursion on the I-crossing. Until then, L is a checked statement, not a lemma.

2.4 Departure rules

• GEN = right sweep (R3/R4/R5 with a = g ≥ 1; g ≥ 2 or d_1 = 0 leaves (1 I) next to w) + L. Derived from R3–R5 and L, so it is only as good as L.
• ABS1, ABS0, ABSO1 (g = 1, d_1 = 1): R4/R5 with a = 1 returns F with O (the cleared d_1) directly right of w. Then come L (context O), W3 (E> O → <F I), a second L, and an absorption tail in which E departs into I. Only the first part is derived. The whole rule is checked:
• random instances to the next departure (check D: GEN 1,362, ABS1 724, ABS0 610, ABSO1 542; at spacing exactly 3: GEN 1,285, ABS1 636, ABS0 292; edge cases ABS1 on w = 1 and GEN on '', 300 each; all exact);
• lockstep on the trajectory (check F: 50,280 sweeps to 1e8; deepen.json: 1,096,578 sweeps to 1e10, 0 mismatches).
• Owed (major). Each ABS rule as a chain of proved multisteps: R4/R5 (a = 1), then L (context O), then W3, then L, then the tail lemmas, which still have to be extracted. When all rules are exact proved multisteps, §5's separate "F reads 0" argument is no longer needed.

3. Invariant and coverage

INV(w, g, D, G) := INV-R ∧ P_k ∧ INV-W ∧ Safe ∧ X, where X is the missing clause that would make Safe inductive (§3.4). Without X this is not an invariant.

3.1 INV-R and P_k (right part), proved

INV-R: - k ≥ 1 and g ≥ 1; - G_k = 0; - H_i ≥ 0 for 1 ≤ i ≤ k; - H_1 ≥ H_2 ≥ … ≥ H_k; - H_i ≥ 1 for 1 ≤ i ≤ k−3.

P_k (replaces O1): k ≥ 2, or (k = 1, D = [1], and (g ≥ 2 or the last token of w is 1)).

• H1 (one inc, carry stopping at digit j):
• H_0 drops by 1 iff j = 1 (d_1 set). Otherwise g−1 and d_1: 1→0 cancel.
• For 1 ≤ i ≤ j−2, digits i and i+1 both shift, so G_i is unchanged; d_(i+1) goes 1→0, so H_i gains 1.
• H_(j−1): G_(j−1)+1 and d_j: 0→1 cancel.
• Above j nothing changes.
• Overflow clears every digit, so H_i gains 1 for i ≤ k−1. The new digits have H_k = H_(k+1) = H_(k+2) = 0.

So inc never lowers any H_i (i ≥ 1). Equivalently, H_i counts the clears of digit i+1. - H2. For i ≥ 1, H_i − H_(i+1) never decreases: every clear of digit i+2 is also a clear of digit i+1. At overflow the new tail is …, H_(k−1)+1 ≥ 1 > 0 = H_k = H_(k+1) = H_(k+2). So the chain H_1 ≥ … ≥ H_k is kept. - H3. The last gap never changes while it is last, and overflow appends gaps 0 and 0, so G_k = 0. g drops only on a carry through d_1, which needs g ≥ 2 in GEN, so GEN keeps g ≥ 1. Strip only raises g. - Absorption (ABS1 c = 2, ABS0 c = 1). The new right part is inc(G_1 + c, d_2.., G_2..), so indices shift by one: new H_i = old H_(i+1), then H1 applies. The H clauses are kept. For g: - k ≥ 2: new g = G_1 + c − d_2 = h_1 + c ≥ 1 (if d_2 = 1 the inc carries and g = G_1 + c − 1; if d_2 = 0 it sets d_1 and g = G_1 + c). - k = 1: by P_k, D = [1] and (g ≥ 2, which is not an absorption, or t = 1). With t = 1 the rule is ABS1 or ABSO1. ABS1 gives inc(G_1 + 2 = 2, [], []) = (g = 1, D = 00, G = 00), so k = 2. ABSO1 never lowers k. - So ABS0 never runs with k = 1. That case would really give g = 0, a configuration outside the family; the review checked that the model and the machine agree there, 259 of 259. - P_k is kept (one step): - k only drops at an absorption, by one. - An absorption at k = 2 with d_2 = 0 gives k = 1, D = [1] and g = G_1 + c (G_2 = 0). ABS1 has c = 2, so g ≥ 2. ABS0 outputs a word ending in 1 1. Either way P_k holds. - An absorption at k = 2 with d_2 = 1 overflows to k = 3. - From k = 1, D = [1]: a GEN overflows to k = 3. An absorption has t = 1 (above), so it is ABS1 (k → 2) or ABSO1 (k → 3). - Strip only raises g. - At the start k = 2. - Check E: exhaustive one-step check on all words of ≤ 7 tokens and right parts with k ≤ 4, G_i ≤ 4, g ≤ 4 satisfying INV-R: 2,358,665 transitions at spacing ≥ 4 and 3,047,785 at spacing ≥ 3, 0 failures. ABS0? cases are left to Safe. - H4 (interval). From an absorption with (h_1, d_2, c), the next absorption comes after exactly Δ = 2(h_1 + c) − 1 + d_2 + 2s sweeps, where s is the number of strips in the interval. This follows from τ (§1): after the absorption τ = 2(h_1 + c) − 2 + d_2, and each strip adds 2. The earlier statement without 2s was wrong whenever a strip occurs; strips are common (check F: 438 of 438 intervals match the corrected formula). - H5. H_i ≥ 1 for i ≤ k−3 is kept: - inc only raises H; - overflow raises every old H_i (i ≤ k−1) by 1 while k grows by 2; - absorption shifts indices down by 1 while k drops by 1. - T (transient tails). After ABS1 the next two sweeps are GEN: - d_2 = 0: the new state is (G_1+2, d_1 = 1) → GEN gives (G_1+1, d_1 = 0) → GEN. - d_2 = 1: G_1 ≥ 1 by H_1 ≥ 0. The new state is (G_1+1, 0) → GEN gives (G_1+1 ≥ 2, 1) → GEN.

This removes the transient tails x I 0, x O 1 and x I 1 that ABS1 can leave before any absorption sees them: … O 1 1 → … I 1 (strip); … I 0 1 → x' O 1 → x' I 1 (strip); … I 1 1 → x' I 0 → x'' O 1 → x'' I 1 (strip). - Removed: the old claims "h_1 ≥ 2 implies next h_1 ≥ 1" and the next-h_1 formula. Both are false when an overflow comes before the next absorption. Counterexample, checked on the machine: Dep(1010; 1; 10; 2,0), ABS0, then the next absorption is Dep(101I01; 1; 110; 1,0,0), with h_1 = 0 and k = 3. P_k makes them unnecessary.

3.2 INV-W (word shape)

INV-W: w is empty (only right after a strip, with g ≥ 2), or: - the first token is not 0; - the last token is 0 or 1; - markers are pairwise ≥ 3 tokens apart. This was 4 before the review. The rules are exact at spacing 3 (check D: L exhaustively, the departure rules on random words with markers exactly 3 apart). The trajectory keeps ≥ 4, so the weaker clause loses nothing and removes the spacing-3 unsafe values from Safe.

This is L's domain (§2.3). - GEN. inc_L never moves a marker: O→I, I→O and the I-crossing all rewrite in place. The left-edge case shifts all indices uniformly. The I-crossing keeps the marker at its index and ends the word in 1. The left edge always gets a 1 (inc_L('') = 1 0). A trailing I 1 is stripped; by the spacing, the token before it is not a marker. Kept. - ABS1. It applies when the last token is 1 and the tail is not O 1 (that is ABSO1, and I 1 was stripped). Two inc_L keep the markers in place. Dropping the last token leaves the x I 0/x O 1/x I 1 transients of T, which are not absorption inputs, or a word ending in 0/1. w = 1 gives 1 0. Kept, with T. - ABSO1. inc_L(x) is a GEN-type step on x. Kept. - ABS0 creates a marker O. In the case v 0 1^k it sits at position 3 from the right. In the case v 0 1^k 0 it replaces the 0 in front of the 1-run. ABS0 keeps INV-W only if that 0 exists (not a marker) and no other marker is within 2 tokens of the new one. This is part of Safe.

3.3 Safe (formerly O2): a predicate on one configuration

Between absorptions only GEN acts, and it touches w only through inc_L (and strip, which adds 2 to τ). So the next absorption is determined by (w, τ) alone:

Safe(w, τ):  repeat { strip w (τ += 2 per strip); if τ = 0 stop; w := inc_L(w); τ := τ − 1 }
             at the stop: last token 1, or (last token 0 and abs0(w) is defined and leaves markers >= 3 apart)

Safe(w, 2g − 1 − d_1) is a decidable property of a single configuration. With INV-R, P_k and INV-W it guarantees that the next absorption has a rule and that its image again satisfies INV-R, P_k and INV-W. On the trajectory it holds at every interval (check F: 440 of 440 to 1e8; with spacing ≥ 4 also 440 of 440).

It is not inductive. After an absorption the next interval has length Δ' = 2(h_1 + c) − 1 + d_2 + 2s, and Safe for it depends on the low bits of the new word at a time set by the right counter. INV-R, P_k, INV-W and Safe together do not exclude a failure. The review gives configurations satisfying all of them that halt, for example Dep(1O100; 1; 11; 2,0) (halts at step 940) and Dep(1001001O1100; 1; 10; 2,0) (step 1,436). Of 323 random starts failing only the O2 clause, 85 halted within 2e6 steps.

What is proved about markers: - Case-(i) markers (tail O 1 1) cycle O11 → I01 → I11 → x' O11 with t = 1 until the next absorption, which is therefore ABS1. Then T removes them within two sweeps. - Crossing period. A marker at position p from the right (t = position 1) has a (p−2)-bit counter below it. A full cycle O → I → crossing takes 2^(p−1) − 1 sweeps once t = 1, and any I-crossing sets t = 1. So a marker with 2^(p−1) − 1 < Δ cannot be present at an absorption with t = 0. In practice only leading markers (index 0) reach a t = 0 absorption. - Unsafe values. For a word M s t with a leading marker M and an m-bit segment s (u = M s), ABS0 is unsafe exactly when: - s = 1^m or 1^(m−1) 0: abs0 is undefined; - s = 0 1^(m−2) 0 or b 0 1^(m−3) 0: the new O lands 1 or 2 tokens from M.

As fractions of 2^m these are ≈ 1, 1/2 and 1/4, 3/4 (spacing 4 would add 1/8, 3/8, 5/8, 7/8).

3.4 Why Safe is open, and what the data say

Mechanism of the dangerous events (model, scripts/review/absmodel.c): - A leading O is born when ABS0 meets u = 1^(m−1) 0 (u = 2^m − 2). The left edge then acts as a 0 and the word becomes O 0^m 1 1. - Its segment then counts the sweeps. The first t = 0 absorption after the birth (when the birth is followed by one ABS1 with even Δ) sees a segment of Δ_1/2 + Δ_2 ≈ 1.5 Δ, compared with the maximum 2^m − 1 = u_c + 1. So the margin is about u_c − 1.5 Δ. - At marker-free ABS0 events the ratio u/Δ_next stays in a narrow band: [1.6060, 2.0006] for every Δ ≥ 2^9, and [1.6067, 2.0000] for Δ ≥ 2^15 (1e10 sweeps). Case-(ii) events (u even) reach ratios above 1.95 1,205 times to 1e9 sweeps. - Leading-O births to 1e10 sweeps, as (sweep, u_c/Δ_next): (340, 1.667), (400,022, 1.620), (1,332,801, 1.775), (6,315,092, 1.630), (19,421,581, 1.859), (73,470,546, 1.912), (1,118,233,557, 1.960), (5,112,107,104, 1.833). The birth at ratio 1.960 is close to the 3/4-point edge (2.0), but no t = 0 absorption saw that marker.

Margins. The only ABS0 events with a marker present to 1e10 sweeps (five) follow births above. Each has a leading O, and the margins are in sweeps to the nearest unsafe word, forward/back, spacing ≥ 3:

The 2-sweep miss is a real near-halt. At step 86,265 the machine stood at Dep(O111000; 1; 111100; 9,4,2,0,0,0). The same configuration with the word two sweeps further on, O111100 = O 1^(m−1) 0 0, halts 18,861 steps later (scripts/review/unsafe_probe.c). The words O111000, O111010 and O111110 run for 2e8 steps. In random right contexts, M 1^(m−1) 0 0 halted 40 of 40 times. The spacing-violating patterns ran 3e6 steps without halting, but they leave the model.

Why a margin argument does not close it. A band proof would remove the ≈ 1.5 Δ coincidence, since 1.6066 > 1.5. But: - the 3/4 point corresponds to u_c ≈ 2.0 Δ, which is the top edge of the band; - later t = 0 absorptions in the same leading-marker episode see segments ≈ (2 − 2^(−j)) Δ (one more halving per intervening ABS1; heuristic, not checked event by event), and 1.75, 1.875, … lie inside the band.

So safety needs u_c to avoid a set of O(1)-wide targets at the roughly one birth per doubling of Δ. No structural reason for this is known. The trajectory survives because births are rare and each hits a target with probability about c/Δ.

4. Initial segment

c0 = 0^inf A> 0^inf -->(2,033 steps) Dep(10O011; 2; 1 1; 1 0), i.e. 0^inf 1000100001010 E> 10110 110 10110 110 11 0^inf. This is direct simulation; check G replays it with an independent simulator and compares the tape cell by cell. It is the first departure at step ≥ 2,000. Earlier departures have D empty or G = 0,0,0 (step 2,343 still has G_1 = 0, which INV-R allows).

INV at the start: - INV-R: k = 2, g = 2, G_2 = 0, H_1 = 1 − 1 = 0, H_2 = 0. The H5 clause is empty. - P_k: k = 2. - INV-W: 1 0 O 0 1 1, one marker, last token 1. - Safe: the first interval is safe (check F).

5. Conclusion

5.1 What would finish the proof

1. A clause X such that INV-R ∧ P_k ∧ INV-W ∧ Safe ∧ X is preserved by every rule. This is the fatal gap. The search should start from §3.4: a quantitative relation between the left counter u and the next intervals Δ, Δ', … at each leading-marker birth, strong enough to keep every t = 0 absorption of the episode off the unsafe values.
2. L and the ABS rules as proved multisteps (major; §2.3, §2.4).

With 1 and 2, progress_nonhalt_cond (P := INV) gives non-halting. Every departure rule takes ≥ 13 steps (L alone takes ≥ 13), and by §3 every departure in INV has an applicable rule whose image is in INV.

5.2 Halting transition

F1 is the only ---. F is created only by C1 (1LF): in the turns W3/W4, in L's I-crossing, and in the ABS tails. In W3–W6 and R2, F only moves onto the last cell of a token, which is 0. This argument covers the window lemmas and R1–R5 only. It does not cover L or the ABS tails. For those it must come from their derivation as exact multisteps (owed), which will make it unnecessary. The 2-sweep near-halt in §3.4 shows that F does read 1 just outside the Safe domain.

5.3 Cryptid assessment (protocol triggered; flagged for Dennis)

The old "not a cryptid" claim is withdrawn. The rules themselves are counter increments and fixed rewrites. The halting question, however, is whether a deterministic coupled system avoids a sparse target set: - the left counter (+1 per sweep, halved at ABS1, rewritten by ABS0); - the right counter, whose absorption times Δ ≈ 2h_1 grow like √(sweeps).

Safety is decided by the low bits of u at absorption times. The smallest margin observed is 2 sweeps, at h_1 = 8. Later margins (4 events up to h_1 = 35,748) are 7–13 % of Δ, but no structural lower bound is known.

Heuristic: about one leading-O birth per doubling of Δ, each failing with probability O(1/Δ), so the expected number of failures beyond the simulated range is O(Σ 2^−m), which is tiny. The machine is therefore "probviously" non-halting, but the argument is probabilistic. Per CLAUDE.md the rules are written out (§2, executable in scripts/review/absmodel.c and scripts/deepen/model3.py) and the machine is flagged; stop or continue is Dennis's call. A Rocq rule reduction in the AntiHydra style (the formal half of the protocol) has not been written.

6. busycoq lemma plan

• Nearest templates.
• vendor/busycoq/verify/BECv7.v: Inductive RD, bin_inc (little-endian increment, l.419), and sideRLs for passes over digit lists. Reuse them for D and the R-sweep.
• 1RB1RE_1LC1LE_1LD1LC_1RB0LD_1RF0RB_---0RA.v: progress_nonhalt_cond with a list invariant.
• Our kill #11 (machines/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---/): a binary counter with merges and a three-phase INV.
• For the cryptid route: verify/AntiHydra.v (rule reduction only).
• Plan. 1. Inductive tok := T0 | T1 | TO | TI with cells : tok -> list Sym; the left word as list tok (reversed for <*); the right part as list (bool * nat) (digit, gap). 2. W1–W6 by execute; R1/R2 by ind; R3–R5 by induction on the digit list (as BECv7's bin_inc). 3. L: an inductive relation incL w w' mirroring the five cases (big-endian, with recursion at TI), and the turnaround lemma by induction on the carry length plus the recursion. The right context is a parameter whose first two cells are 1, 0. 4. ABS1/ABS0/ABSO1 as follow chains: R4/R5 with a = 1, L, W3, L, then the absorption tail lemmas (to be extracted). 5. Definition INV from §3 (with X), init by execute (2,033 steps), and nonhalt by multistep_nonhalt + progress_nonhalt_cond.
• Blocked on X for step 5. Steps 1–4 are worth doing only if Dennis decides to continue (§5.3).

7. Evidence (python3 -B check_proof.py, full mode; --quick is smaller). Full mode: SUMMARY PASS 36/36

Longer horizons: - 1e10 steps lockstep (deepen pass, deepen.json): 1,096,578 sweeps, 0 mismatches. The review's independent lockstep run to 1e10 (1,096,579 sweeps, full-tape comparison) found every INV-R/H5/INV-W clause and abs0-definedness intact. - Trajectory numbers (corrected): h_1 = 111 at the absorption at step 100,870,169 and h_1 = 161 at step 300,628,504 (the old "≈ 80 at 3e8" was wrong). The review counted h_1 = 241 near 1e9 and 522 near 1e10. Rule counts to 1e10 (review): GEN 1,094,494 / ABS1 1,561 / ABS0 524. - Abstract model (scripts/review/absmodel.c, pure model, no machine steps): 1e10 sweeps = 199,990 absorptions (ABS0 49,833, ABS1 150,157, ABSO1 0), with no ABS0?, k = 1 or spacing < 4. There are 5 ABS0 events with a marker, all leading O, as the review's independent run also found. Margins are in §3.4. Run: gcc -O2 -w -o absmodel absmodel.c && ./absmodel 1e10 0 4 (about 9 min). - Scripts: scripts/review/ (absmodel.c, pk_check.py, unsafe_probe.c, and pre-review copies of proof.md and check_proof.py).

8. Checkpoint B notes (Dennis)

(none yet)

9. Review log

2026-10-10, skeptic review → revision (this file).

Validation after the revision: check_proof.py full mode SUMMARY PASS 36/36 (was 25/25; 11 checks added).