1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA: never halts (informal proof, STUCK)

• Machine: 1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA, pilot #16, viewer https://bbchallenge.org/1RB0LC_1RC0RA_1RD0RF_0LE---_1LB1LA_1LD1RA
• Sheet: Results row 650, "Chaotic Fractal Others", no notes, no Discord thread.
• Written for the string itself, started in A on the blank tape.
• Status of this document (stage informal_proof, skeptic rounds 1 and 2 applied, 2026-10-12): not a proof; status STUCK. The rules are sound, but no inductive invariant is known.
• Rules: every rule is stated exactly. The machine-level and bouncer-level rules come with derivations, and every macro rule is checked by exact simulation (§9). An independent skeptic re-check confirmed them (422,018 right-end transitions, 2.6e10 steps; round 2: 400 more transitions of new kinds, 1.0e8 steps).
• Invariant: H*c4 (§5) is not inductive, on long right ends or on short ones.
  • Long right ends: a family of members goes to a window right end. The family grows with the level: 1 member at S = 83, 60 at S = 168, at least 96 at S = 339 (§8 G2).
  • This round derives the window start: it is the Clean formula (§4.4, check L1). With it, the window cases with δ = 0 are ruled by the existing rules, except one case with two walls.
  • One new corner rule, RightEndP2W, is validated (check M1). With it, δ = 1 for S even is ruled.
  • The remaining cases run into a V1 right end with walls. Its restart writes a left word outside the grammar of §2 (check L3).
• Closure, short right ends (≤ 1 real wall): open. The clause for them is a look-ahead (Hs_4), and it is not inductive. Wider boxes give at least 110 + 12 + 450 leaks (§5.5, §8 G1).
• Derivations: Lemma T, the growth step G, the collapse C and CP are fitted, not derived. The CP sketch only shows that CP is equivalent to H1 at the successor (§5.2).
• Checks: check_proof.py. Sections A-L: SUMMARY PASS, 36 checks, 0 fail, 1,239 s. Section M, run separately: 2 checks, 0 fail. There are also 12 OPEN lines that measure the gaps. Log: check_proof_full.txt. Predicate and boxes: scripts/inv4.py. Round-2 boxes and the window rule: scripts/round2.py.

0. What the machine does

The tape is one bouncer that runs between two growing regions.

• Left-turn frame. The head is in A, reading the 0 just left of the active word Y. To its left is either
• a stack of "walls" X plus a run (10)^P, or
• the blank edge.

To its right are Y, a run (010)^d and a list Z of pending chunks. - Each round trip sweeps right across Y to the (010)-run, eats two (010) units, and sweeps back. - Each trip takes (10)^2 off P, or, at the blank edge, extends Y to the left. - The run that the eaten units feed grows by 2. - When d runs out, the next chunk merges into Y, or (with d = 1) is eaten. - When P runs out at a wall, one of two things happens: - the bouncer pushes its whole Y as a new chunk and restarts on the wall (Push); - or it absorbs walls by a binary carry (Absorb). - When d and Z are both gone (a "right end"), the rightmost (10)^ak-run feeds a Jacobsthal staircase: busycoq's FractalType4 TM5 lemma P. The staircase lays out the next (010)^d-run, and the old Y becomes the new wall stack.

Halting needs the right sweep to meet the pattern B> 0 0 1 (§6). In the grammar this happens only when an odd (10)-run inside a chunk gets eaten. A parity invariant excludes that, but the invariant also has to carry linear facts that link the walls to the staircase level (§5).

1. Rule table

      0     1
A    1RB   0LC
B    1RC   0RA
C    1RD   0RF
D    0LE   ---
E    1LB   1LA
F    1LD   1RA

This is FractalType4.v Module TM5 (1RB0RE_1RC0RF_0LD---_1LA1LE_1RA0LB_1LC1RE) with TM5's states A,B,C,D,E,F renamed to B,C,D,E,A,F (check A1). TM5 starts in its own A, which is our B. So TM5 is this table started in another state. Its lemmas Inc1, Incs1, P, P_S and P_S' carry over verbatim after the renaming (checks C1-C3).

2. Notation and families

Words are written left to right. Two head markers are used: - <S: the head is in state S, reading the last cell of the word to its left; - S>: the head is in state S, reading the first cell of the word to its right.

Block names: - (10): pair; - (011010): six-block; - (010): triple; - (101): wall cell triple.

Staircase levels. S_0 = 0 and S_{j+1} = 2 S_j + 3 if S_j is even, 2 S_j + 2 if S_j is odd. This gives 0, 3, 8, 19, 40, 83, 168, 339, 680, 1363, ... For n ≥ 1, Sof(n) is the largest level ≤ n − 1.

Active word. Y = (10)^a0 (011010)^b1 (10)^a1 ... (011010)^bk (10)^ak, with k ≥ 0. It is written Y = [a0, b1, a1, ..., bk, ak]. B = Σ b_i and A = Σ a_i. A "segment-less" Y is [a].

Chunk. C = (011010)^B1 (10)^A1 ... (011010)^Bm (10)^Am (010)^c. Chunks are listed nearest first in Z. A chunk with c = 0 is glued to the next one. Zero inner runs glue their neighbours ((011010)^b (10)^0 (011010)^b' = (011010)^(b+b')). Both are tape identities.

Walls. X = (10)^p1 (101)^q1 ... (10)^pm (101)^qm, listed far to near. An interior wall with p = 0 is glued to its left neighbour (normX).

Families. Two kinds of left-turn frame:

P-mode  F_P(X, P, Y, d, Z) := 0^inf X (10)^P <A Y (010)^d Z 0^inf      (a0 = 1, P >= 1)
edge    F_E(Y, d, Z)       := 0^inf <A Y (010)^d Z 0^inf

Virtual frames. These are P-mode frames with P ∈ {0, 1} next to a wall. They are not left-turn frames of the machine: the cell two left of the head is a wall cell. They occur only inside composite rules (§4.3):

V1 := 0^inf X (10)^p (101)^q (10)^1 <A Y (010)^d Z 0^inf
V0 := 0^inf X (10)^p (101)^q <A Y (010)^d Z 0^inf

Right end. A frame with d = 0 and Z empty, written R = (mode, X, P, Y). Three kinds exist in the rule set: - an E hub 0^inf <A Y 0^inf; - a P-mode right end without walls, 0^inf (10)^P <A Y 0^inf; - a P-mode right end with walls, 0^inf X (10)^P <A Y 0^inf, X nonempty.

The rules of §4.4 handle all three. The third kind does occur: from long Level hubs (e.g. [35,13,30,14,18,2,40]) and on the short chain from the E hub [79,12,32] (§8 G1). The invariant of §5 admits only the first two kinds (clause H0), so "right ends in the invariant have no walls" is a clause to be preserved, not a fact about the rules.

Base. K0 := F_E([85, 7, 46], 0, -) = 0^inf <A (10)^85 (011010)^7 (10)^46 0^inf, reached at step 46,734 (§7).

3. Machine-level and bouncer-level rules

3.1 Shift rules (L0; each proved by es on one block, then ind n)

Right sweep. From a left-turn frame, A0 writes 1 and moves right. The sweep then runs R1 over (10)^a0, takes A0 at the last 0, then alternates R3 and R2 over Y. The swept word has the same exponents and reads (10)^a0 (110110)^b1 (10)^a1 ... (10)^ak 1, shifted one cell left.

Right turn and left sweep. The turn T1 converts two triples. The left sweep (R4, R5, R6 and boundary gadgets) restores the six-blocks.

3.2 Trip lemmas (L1; proof: right sweep, T1, left sweep, then left turn; checks D1/D2 test that the target is the next left-turn frame and that the step count is exact)

• Edge mode. The left turn extends the blank edge by one (10) per trip. A trip plus the next right-sweep start gives a0 + 2.
• P-mode. The left turn takes (10)^2 from P and builds one more six-block in the first segment.
• k-fold forms (ind k): d+2k -> d, with a0+2k or (P−2k, b1+k), and ak+2k. The step counts add up to Σ_j (10 + 20B + 6(A+4j)) and Σ_j (22 + 20(B+j) + 6(A'+2j)).
• Merge is a tape identity, not a rule. When d = 0, the frame F(…, Y, 0, C Z) is F(…, Y C', c, Z), where C' is C without its triples.

3.3 Staircase (TM5 lemmas, renamed; checks C1-C4)

• C1 checks that P(a) holds exactly for a ∈ {0, 3, 8, 19, 40, 83} among a ≤ 130.
• The recursion of P_S/P_S' is the level recursion. So P(S_j) holds for every level, by induction on j from P(3).
• C2 re-checks P(S) for every S ≤ 1400 in 4 left contexts, and confirms that l is never read.

4. Macro rules (exact transitions between frames)

Every rule is an exact run of the machine (no halting, ≥ 1 step). It is a composite of §3 lemmas and finite gadgets.

How the rules are checked: - All of them at once, as scripts/macro_sim3.py step (the executable form of this section): E1 runs every frame of a small grammar box, and E2 runs random frames. In each case the exact run must visit the next ≥ 3 macro frames in order. - Per family, by earlier stages: notes.md, val_corner*/val_hubsweep/val_events2 and others, 1,500+ instances in total.

Rules marked (k) apply k-fold. "unruled" means that no rule applies. The invariant must exclude every such frame (§5, §8).

4.1 Edge mode F_E(Y, d, Z)

4.2 P-mode F_P(X, P, [1, b1, M, ak], d, Z)

EatToEdge. Write n = ⌊(P−2)/4⌋. First eat n whole units from the front of the chunk. A unit is one six-block or two pairs, and each unit gives P − 4 and b1 + 2, plus ak + 1 for a six-block. This leaves P0 = P − 4n ∈ {2, 3, 4, 5}. Then one more unit:

Every six-block unit adds 1 to ak. If the last unit finishes the chunk, d = c + 1 ("Exact"). If it does not, the rest of the chunk stays in Z with d = 0.

4.3 Virtual frames, walls (p, q) nearest last

V1 (P = 1 next to the wall (p, q)):

V0 (P = 0 next to the wall): Absorb0, a carry chain. Number the walls nearest first, (p_1, q_1), (p_2, q_2), .... Set r_1 = 0 (r_1 = 2 for the old AbsorbChain, which is BounceP 2→0 + Absorb0). Then

e_j = floor((q_j + r_j) / 2),   r_{j+1} = (q_j + r_j) mod 2

• It stops at the first J with r_{J+1} = 0. Then X loses its J nearest walls, P = p_J and Y = [1, e_J, p_{J-1}, e_{J-1}, ..., p_1, b1 + e_1, M, ak] If p_J ∈ {0, 1}, resolve the virtual frame again.
• If it never stops, the result is edge mode with a0 = p_m + 3, with the same Y body.
• Domain: interior walls have p ≥ 1. The wall p = −1 occurs only as the leftmost wall, and the chain does not stop there. Outside this domain the rule is unruled (§4.5, rows U15-U16).

4.4 Right ends: the staircase restart

Let R = (mode, X, P, Y) with Y = [a0, b1, ..., bk, ak] and k ≥ 1. Its wall list is

E hub (X empty):          V = (a0 − 1, 2 b1), (a1, 2 b2), ..., (a_{k−1}, 2 bk)
P-mode, X empty:          V = (P − 2, 2 b1 + 1), (a1, 2 b2), ...
P-mode with walls X:      V = normX( X, (P − 2, 2 b1 + 1), (a1, 2 b2), ... ),   needs P ≥ 2

The P-mode first wall is the "collapse wall". The third line is the rule PModeW* of macro_sim3 (right_end with OPTS['pmode_walls']): the old walls X simply stay in front of the new ones. It was validated by exact simulation with random X in a third of the instances (val_hubsweep seed 94, 30/30 clean + 30/30 top), and it is exercised in check E1 (PModeWClean 2,338, PModeWLevel 3,357, PModeWTop 10,524 frames). Then normX. Let S = Sof(ak).

• If the start has P0 ∈ {0, 1}, it is a virtual frame, handled by §4.3.
• Long starts (P0 ≥ d0 + 4) just bounce on to the next P-mode right end (RightPhaseLong). That is BounceP followed by RightEndP; no new rule is needed.

Window right ends (skeptic round 2). The derivation of Clean never uses ak < 2S − 1. It needs only: - the right sweep and the regrouping; - P(S) on the last S pairs of the (01)^ak run; - Start, which needs m = ak − S ≥ 2 pairs left over.

So the Clean start frame also holds in the window. Check L1 confirms it by exact simulation: 60 window right ends at S ≤ 83, E hubs and P-mode right ends, with 1 or 2 segments and every δ. In the window, P0 − d0 = δ, where δ ∈ {0, 1, 2} for S even and δ ∈ {0, 1} for S odd.

The bounce then ends as follows (scripts/round2.py):

• Check L2 runs every ruled window hub of a random box (S ≤ 83) exactly for 3 events: 0 misses. It also counts the unruled ones (L2b): all with δ ∈ {1, 2}, and 1 of 60 with δ = 0.
• On the skeptic's δ = 0 examples the orbit is back in H*c4 one or two right ends later. For example, [2995,29,677] goes by Absorb to P = 2994, [1,199,338], which is a member. [1485,15,335] goes by V1RightEnd to P = 1453, [1,16,30,84,167], which fails H2t', and then to P = 992, [1,230,353], a member.
• The δ ∈ {1, 2} rows are not ruled.
• Exact simulation shows what happens there. The restart of a V1 right end with walls writes the left word (10)^p (101)^q 1 (101)^r: a wall glued to a lone 1 cell.
• Such a word contains 111, which never occurs in a wall stack (10)^p (101)^q. So this is a tape form outside the grammar of §2 (check L3, window hub [21,3,38], at step 3,010).

• The glued wall looks transient. In the exact run from [21,3,38] it appears at step 3,010 ((10)^19 (101)^6 1 (101)^20 (10)^18 <A ...). By step 4,685 the orbit is back in the grammar at the edge-side P-mode frame F_P(−, 17, [1, 4, 0], 39):

  • d = 39 = (2b1 + 1) + ak, with b1 = 10 and ak = 18 at the V1 right end;
  • the wall (20, 6) has been absorbed: b1' = 1 + 6/2 and P = 20 − 3.

  The next 6e7 steps never show the glued word again. So a composite rule for the V1 right end with walls probably exists: here ak + 1 = 19 is a level, so it is a Top-like restart whose last wall is the glued one. But it is not written, it is not validated beyond this one run, and the Clean/Level/window cases of the same corner are not explored. - Free runs of 4e9 steps from the δ ∈ {1, 2} hubs [21,3,38], [25,3,17], [3003,29,678], [6101,15,1360] and [6109,15,1361] do not halt (skeptic: 4e9 steps from the δ = 0 hub of the S = 168 family). This round has no rule for these cases.

4.5 Every unruled branch, and what excludes it

macro_sim3 raises Unruled exactly in the branches below (this list is the complete set of raise Unruled sites in scripts/macro_sim3.py). "Excluded by" names the clause of H*c4 (§5) or the argument that keeps the orbit out of the branch, and how well that is established: - local: the clause excludes it at the right end itself, by the definition; - box: no member of the exhaustive closure boxes (§5.5) reaches it within one traversal, but there is no symbolic proof; - refuted by box: members of H*c4 reach it, within one or a few traversals, in the wider boxes of skeptic round 2 (§5.5). The clause named does not exclude it; - argued: an argument is written below, but it is not a full induction.

So no unruled branch is excluded by a proof. Each is excluded locally by a clause of H*c4 (and then the question is whether the clause is preserved), or by an argument, or only by the closure boxes. Three rows (U4, U13, U24) and the successor part of U17 are reached by members. The 'box' rows are tested only on the boxes of §5.5, and their counts depend on how those boxes are cut.

5. Invariant

5.1 Hub coordinates

Every right end R without walls (except a segment-less hub) gets a flat sequence z = (z_1, ..., z_2m) and a scale τ.

1. Take the walls V of §4.4 in order.
2. Add one virtual last pair, the start frame's fresh bouncer: - Clean: (ak − S + 1, S − 1), with τ = S − 1; - Level: (1, ak − 1), with τ = ak − 1; - Top: replace the last pair (p, q) by (p, q + ak), with τ = ak.
3. Define the tail sums

B(k) = Σ_{l ≥ k} (−1)^l z_l

so z_2m is counted with sign +.

"Short" means m ≤ 2, that is, at most one real wall. "Long" means m ≥ 3.

Lemma T (traversal as a stack process). Status: fitted, not derived.

Hypotheses (all needed; the skeptic's counterexamples break each one that is dropped): - R is an E hub or a P-mode right end, with no walls; - R is Clean or Top. A Level right end with ≥ 2 real walls is excluded: [35,13,30,14,18,2,40] has B(3), B(5), B(7) ≥ 0 and still ends its traversal in a P-mode right end with a wall; - every restart at a wall has P odd, so the bouncer pushes or merges and never absorbs. This holds when every real wall is even/even, which is H1 (a0 odd, inner a even); a P-mode right end's collapse wall is odd/odd and gives a P-even restart, which absorbs. So in P-mode the statement covers the walls after the first one only.

Statement. Write Δ = d − P. During the left traversal of the walls: - at a wall with Δ ≥ 1, Push stores a chunk with Δ − 1 triples and restarts with δ_i = q_i − p_i + 1; - with Δ ≤ 0, BounceP runs d down and the top chunk is merged or eaten.

The running sum is T_i = 1 + B(2i − 1). Hence: - B(odd k ≥ 3) ≥ 0 means the traversal does not end while walls remain; - B(1) < 0 means the traversal ends in a P-mode right end (a collapse).

What is derived. The push step is derived from the rules: at P = 3 BounceP31 leaves d − 2 at V1, and Push1 stores d − 4 = Δ − 1 triples (§4.3). The restart value δ = q − (p − 1) is read off Push1. The merge step is a tape identity. What is not derived is the accounting through eats (EatChunkP changes P by 4B + 2A, which must cancel against the chunk's contribution to the B sums), and the identity T_i = 1 + B(2i − 1) as a whole. That is gap G2.

5.2 H*c4 (scripts/inv4.py Hc4)

H*c4 is H*c3 (stage seed_clause) with three repairs, one new clause and a total implementation. H*c3's own clauses are listed first.

H*c2 (scripts/hubinv_Hc3.py Hc):

Added in H*c3 (scripts/seed_clause.py):

Changed or added in H*c4 (skeptic round 1):

What the CP sketch shows, and what it does not. CP is fitted. The sketch below does not derive it: it shows only that, given Lemma T, CP is equivalent to H1 (P odd) at the successor. That is not enough, because H1 at the successor is part of what closure has to prove.

A long P-mode right end is the image of a long E hub R0 under a collapse; on orbits every one of them has an E-hub predecessor (2,051/2,051). Three facts enter: 1. The traversal of R0 ends at its first wall (a0 − 1, 2b1), which restarts with P = a0 − 2. If Lemma T holds there (T_1 = 1 + B0(1) < 0), BounceP and a final RightEndP consume all the remaining triples, so P' = −B0(1) − 1 − r with r = (final d) mod 2. 2. The other walls move one position right and are reflected, as in a growth step: B'(3) = 2τ − B0(2). 3. HR at k = 1 for R0 gives B0(1) = 2B0(2) − 2τ − 4 − e0, with e0 = B0(2) mod 2 = B'(3) mod 2.

Substituting gives

P' = 2B'(3) − 2τ + 3 + e0 − r

• If r = e0, this is CP, and P' is odd.
• If r ≠ e0, the same algebra gives an even P', which breaks H1.

So, given Lemma T, CP ⟺ (r = e0) ⟺ H1 at the successor. An earlier version picked r = e0 because P' is odd, which is circular (skeptic round 2).

What a derivation needs: - r, the parity of the final d, computed from the traversal itself (the BounceP / RightEndP count at the first wall); - Lemma T at the first wall (step 1), which is itself fitted (§5.1).

Neither is done. As a fitted fact, CP holds on 2,051/2,051 long P-mode right ends on orbits (blank + 400 rnd_R orbits; check J3 re-checks 1,599/1,599 on another seed).

5.3 What is proved about closure

1. Zipper swap (proved; check H1, exact identity). Suppose B'(k) = 2τ − B(k−1) on a range. Then the even-k zipper relation for B' at k is equivalent to the odd-k relation for B at k − 1, and vice versa. The parities agree because B'(k+1) ≡ B(k) (mod 2). For example,

B'(k) = 2B'(k+1) + 4 + e ⟺ 2τ − B(k−1) = 4τ − 2B(k) + 4 + e ⟺ B(k−1) = 2B(k) − 2τ − 4 − e

So a growth step G preserves HR on the shifted range. This algebra is the easy part. The hard part is that the growth step has this form at all, which is item 3. 2. Band under G (proved, given item 3). If 0 ≤ B ≤ 2τ, then 0 ≤ 2τ − B ≤ 2τ. A unit defect −1 ↔ 2τ + 1 is carried one position deeper, which is clause H3d. 3. Growth step G (fitted, not derived). z' = [h] + z, with the tail re-paired, B'(k) = 2τ − B(k−1) for 2 ≤ k ≤ 2m − 1, and new head h = 5 + B(1) − e with e ∈ {0, 1}. Needs B(1) ≥ 0. 352/352 growth transitions in check H2; 1,329/1,329 from blank (hubinv_bsums.py). Derivation needs Lemma T. 4. Collapse C (fitted). B(1) < 0: the head entry is replaced by the odd collapse wall (P − 2, 2b1 + 1). CW is the closed form of its B(2): 47,668/47,668 in the seed_clause stage. CP (§5.2) pins P. 5. Short transitions S (fitted). Closed forms: - First collapse of a short E hub: B'(1) = B(1) + 2τ + 6 + 2r. - A short P-odd end goes to the E hub [a0', (P−1)/2, B(2) + z_3/2] (2,521/2,521). - Second collapse: v1 = b1, which forces b1 odd (3,538/3,538). - These are fits on the macro map. They are not derived, and they do not yet add up to an inductive clause (§8 G1).

5.4 V1 parity invariant (excludes "V1 with d = 1 and Z nonempty"). Status: induction over the §4 rules, conditional on H1 at every right end.

Claim. At every P-mode frame with walls (X nonempty, including V1/V0): - (a) every chunk in Z has an even triple count c, except possibly the deepest one; - (b) if Z is nonempty, d + P is odd; - (c) if P is even, Z is empty.

Wall parities (the hypothesis). Every wall of X is a wall of some earlier right end's list V (§4.4), possibly glued by normX. Under H1 at that right end: - an E hub gives the walls (a0 − 1, 2b1) and (a_{i−1}, 2b_i), all even/even (a0 odd, inner a even); - a P-mode right end gives its collapse wall (P − 2, 2b1 + 1) first. That wall is odd/odd for P odd but even/odd for P even. The rest are even/even; - normX glues a p = 0 wall onto its left neighbour and adds an even q = 2b_i, so it keeps both parities.

By H0 the right end has no walls in front, so the collapse wall is always the leftmost wall. Hence every wall that is not leftmost is even/even. (Round 1 claimed p ≡ q for every wall; that is false for the even/odd collapse wall, as the skeptic noted. The claim is used below only for walls that are not leftmost.)

Induction over the rules that act on a P-mode frame with walls.

Hence, at V1 with Z nonempty, d + 1 is odd, so d is even and d ≠ 1, and U11 never fires.

Status. This is now an induction over the rules. It still rests on H1 at every right end, which is exactly the closure that is open (G1, G2). The rows were also checked on frames: 127,020 frames with walls and Z nonempty (v1d1_parity.py).

"ak even at Push1" (§6). This is a different statement, and it is not derived. EatChunkP adds B (the number of six-blocks in the eaten chunk) to ak, and nothing above makes B even. It stays a census fact: parity census, 0 exceptions to 1e12 steps (G5).

5.5 Closure evidence: exhaustive back-solved boxes (scripts/inv4.py, scripts/round2.py; checks K1-K6, L4-L7)

The round-0 closure tests drew their right ends from random generators (rnd_R, rnd_short). rnd_R makes only clean/top E hubs at levels ≥ 19, with clean top tails, so it never produced the counterexamples above. The boxes below are exhaustive within their bounds instead.

How a long box is built: - Take every tail of z at the given levels: for Clean and Level the last four entries, for Top the last three, with all even values up to 2τ + 4. - Extend the tail towards the head by the zipper relations (HR), one entry at a time, to every even length up to 2 · MMAX + 2 (MMAX = the pair bound below). - Read the right end off z. For P-mode, z_2 comes from CW and P from CP. - Keep the members of H*c4, run one traversal on macro_sim3, and test H*c4 at the next right end.

Short boxes are plain grids, with the bounds given in the table. Every row is a one-step test. Leak counts are lower bounds: a box with other bounds can only find more. Round 1 reported a short E box with a0 ≤ 80, b1 ≤ 40, ak ≤ 170 (232,794 members, 3 leaks) and a short P box with P ≤ 80 (36,043, 0 leaks). Neither had a saved log or a check, so both rows are withdrawn and replaced by K4 and L6.

What the rows show: - The long E boxes give 0 one-step leaks up to S = 168. The skeptic also ran members for many traversals: 22,877 E and 15,707 P at S ≤ 40 for 40 traversals. - The long P boxes leak, and the leaks grow with the level (1, 60, ≥ 96). That is the window family of §8 G2. - The short boxes leak as soon as a0 and P are no longer cut at 80, and the Pt1 kind, absent in round 1, leaks the most (§8 G1).

6. Progress and halting

Progress. Every rule of §3-§4 is a run of ≥ 1 step: BounceE ≥ 10 steps per trip, BounceP ≥ 22, every event gadget ≥ 1.

A traversal from one right end to the next is a finite chain of rules: - every P-mode rule strictly decreases the left material L = P + Σ (p_i + q_i) (BounceP, Eat*P: P drops; Push1/Push1End/Absorb: walls are removed and P becomes p − 1 or p_J), or ends the traversal; - every edge-mode rule strictly decreases the right material d + Σ chunk sizes (merging is a tape identity), or ends at a right end; - edge mode never returns to P-mode before the next right end.

So (mode, L, right material) decreases lexicographically, and P-mode comes first.

Halting needs B> 0 0 1 (check A3). D is entered only by C0 and F0. - F is entered only by C1, which writes the 0 that F0 then sends D onto. - C0 returns D onto the 0 that A1 just wrote. - The only other entry to C is B0.

So every halt is B0, C0, D1: B reads 0, C reads the next 0, and D reads the following 1.

Every rule of §3-§4 is an exact run, so a rule never reads B> 001. In the grammar the pattern comes up only when the right sweep enters a chunk on the odd alignment, that is, when it eats an odd (10)-run that is not at the tape end (I1: 30/30 such frames halt). H1 (inner a even) and §5.4 keep every chunk's (10)-runs even: - Push1 builds them from inner a's and ak + 2. That these runs are even needs "ak is even whenever Push1 fires at a wall". This is a census fact (parity census, 0 exceptions to 1e12 steps), not derived, and not a local parity fact: eats with an odd six-block count flip ak (75 of 163 eats from blank). It is part of G5. - EatLast handles the one odd last run that sits at the tape end.

So "no halt" reduces to: the orbit stays inside the ruled domain (every step is a rule of §4) — which is exactly the closure of the invariant. Without the closure (G1, G2), the halting argument is incomplete. The window family (§4.4) already leaves the ruled domain, so the rule set itself has to grow before an invariant can close.

7. Initial segment

0^inf A> 0^inf  ->(46,734)  K0 = 0^inf <A (10)^85 (011010)^7 (10)^46 0^inf

This is a direct computation: check F1 finds K0 as a left-turn frame at exactly step 46,734.

From K0, macro_sim3 and exact simulation agree: - F2: the first 104 macro frames in order, to 6e7 steps; - earlier stages: 278/278 frames to 1.02e12 (macro_vs_census.py), and 383 right ends on short-seed orbits (seed_e2e.py).

K0 satisfies H*c4, and so do the first 4,001 right ends of its orbit (scripts/inv4_blank_4000.txt; check G1 re-checks 2,001; runs up to about 10^4000 cells). In the skeptic's census these 4,001 right ends contain 0 Level right ends and 0 P-mode right ends with walls.

8. Gaps (why this is not a proof)

After skeptic round 2 the gaps are of two kinds: - two fatal gaps, where the invariant is not inductive and no candidate repair is known (G1, G2); - major gaps: unruled branches that members reach (G3), and derivations that are still fits or arguments (G5).

All leak counts below are lower bounds. They depend on how the boxes were cut (§5.5 states every bound).

Confidence. The mechanism is understood. The macro rules are sound where they apply: independently re-checked on 422,018 right-end transitions (2.6e10 steps), plus 400 transitions of the new kinds (1.0e8 steps), all matched by exact simulation. Every free run from a leak point (window hubs, the U24 chain, the [79,12,32] chain) runs on without halting, so non-halting is very likely.

As a proof, though, this is stuck. The invariant has now failed two independent reviews. Each repair moved the leaks to larger boxes; it did not remove them: - round 1: four fatal gaps; - round 2: the window family grows with the level, and the short regime leaks once its boxes are cut from the band.

What is missing is not a calculation. It is an inductive invariant in a vocabulary that includes the window frames and the short regime. No pseudo-random arithmetic has appeared, so this is not a cryptid.

9. Evidence: check_proof.py

check_proof.py prints PASS / FAIL for claims and OPEN for measured gaps; SUMMARY counts only PASS/FAIL and lists the OPEN lines. Log: check_proof_full.txt (sections A-L in one run: 36 checks, 0 fail, 11 OPEN; section M, added during that run, run on its own: 2 checks, 0 fail, 1 OPEN).

10. Lemma plan (Rocq)

Machine part. Copy FractalType4.v TM5: - rename the states, set tm to this string; - S1, Inc1, Incs1, P, P_S and P_S' carry over verbatim; P0/P3 by es. - Add P_level : forall j, P (S j) by induction on j, with the case split S_j even (P_S') or odd (P_S).

Bouncer part (FractalType7v4 style): - Definition F_P X P Y d Z / F_E Y d Z as tape builders. Y and Z are lists of exponents. Use <* for X and *> for Y and Z, as in FractalType7v4's C x d r / E t. - Trip lemmas by es on the generic block lists: an Inc-style lemma per trip, then Incs by ind. - Each §4 event is a lemma: es plus follow of the trip lemmas. The P-mode/V1/V0 events take the walls as a list argument. Absorb0 is a Fixpoint over walls with a carry, proved by induction on the wall list. - The right-end lemmas use P_level + Start + the right sweep.

Abstract part. A record R for right ends with a next : R -> R function, the composite of the §4 rules (macro_sim3's step iterated to the next right end). Then: - Lemma next_spec : Inv R -> conf R -->+ conf (next R); - Lemma Inv_next : Inv R -> Inv (next R), which needs G1 and G2 first (no inductive Inv exists yet, and next is not total on H*c4: the window family reaches unruled frames); - nonhalt via progress_nonhalt_cond with Inv, plus an esx init of 46,734 steps to K0 (about 0.6 of kill #3's 78,710-step init).

Following rocq-notes, any parameter search (polyhedra for the short-regime clauses) stays native; Rocq checks only the final case list. Formalization should not start before G1 and G2 are closed: the look-ahead Hs_K cannot be the Inv of progress_nonhalt_cond, and the window family needs rules for frames outside the grammar of §2 before any Inv can be stated.

Nearest templates: - TM5 (FractalType4.v) for the staircase; - TM20 (FractalType7v4.v) for the Good/Inv architecture, about 7 of 11 transitions apart. Its rules do not transfer.

Review log

• 2026-10-12 (stage informal_proof, first version):
• Wrote this file from the stages deepen … seed_clause (notes.md).
• New in this stage:
  • the explicit shift rules and the TM5 identification (TM5 is this table started in B; P(a) holds exactly on the levels);
  • the local halting pattern B> 0 0 1;
  • the soundness check of the whole macro rule set on an exhaustive small box (E1);
  • the algebraic zipper swap.
• Self-review findings:
  • (1) The first draft of check C3 used the wrong renamed state in S1 (<C for TM5's <{{A}}); fixed to <B, and it passes.
  • (2) H2's head formula had a sign error in the check script, not in the claim; fixed.
  • (3) The right-end lemma's derivation (right sweep + regrouping + P(S) + Start) was confirmed on one hub by hand: (10)^3 (011010) (10)^10 gives (10)^3 11011 (01)^11 B> 0^inf before P(8).
• Open items are §8 G1-G5. No skeptic review yet.
• 2026-10-12 (skeptic round 1, applied in the same stage):
• Skeptic verdict: not sound. Four fatal gaps, three major, two minor. Confirmed sound by the skeptic: the TM5 renaming, the halting pattern, R1-R6/T1 and BounceE/BounceP with exact step counts, the initial segment (K0 at step 46,734), the progress argument, and 422,018 right-end transitions of macro_sim3 against exact simulation. So the defect is the invariant and its closure, not the rules.
• Fatal 1, H2t false ([9,20,24,2,24,20,39] in H*c3, next right end a window): fixed by H2t' (top tail clean at level ak + 1). Re-checked: J1; long E boxes K1/K3 0 leaks.
• Fatal 2, long Level hubs leak and break Lemma T ([35,13,30,14,18,2,40], [79,2,40,1,40]): fixed by HL (no Level right end with ≥ 2 real walls). Lemma T restated with its real hypotheses (clean/top, P-odd restarts) in §5.1; its derivation is still open (G2). §2 no longer claims that right ends never have walls.
• Fatal 3, long P-mode right ends untested and leaking (118,034 of 726,432): fixed on the S ≤ 40 box by the new clause CP, P = 2B(3) − 2τ + 3 (found on orbits, 2,051/2,051; sketched from Lemma T in §5.2). Long P box: 15,707/15,707 at S ≤ 40. At S = 83, 1 of 128,043 still leaks into a window hub (G2, open). The skeptic's V1 d = 1 (P = 1, [1,41,40,1,41]) and EatLast (P = 23, [1,9,8,1,9]) members fail CP.
• Fatal 4, the look-ahead clauses EB/Hs_K are not inductive ([79,12,32] chain of ≥ 7 short right ends, a P-mode right end with walls at depth 8): not fixed. Measured: runs of short right ends reach 44 (blank) and 46 (rnd_R) in a row, so no fixed look-ahead depth can work. Open as G1, with first data for explicit clauses.
• Major 1, closure evidence from narrow generators: fixed. check_proof.py has exhaustive back-solved boxes (K1-K6); the "0 leaks / high" claim is withdrawn (§8 Confidence).
• Major 2, §4.4 silent on P-mode right ends with walls and incomplete on unruled branches: fixed. §4.4 states the PModeW rule and its validation. New §4.5 lists every raise Unruled of macro_sim3 (U1-U25), each with the clause that excludes it and its status (local / argued / box / proved).
• Major 3, Lemma T, G/C/S closed forms, V1 parity, "ak even at walls" fitted, not derived: not fixed. Each item is now labelled with its status (§5.1, §5.3, §5.4, §6), and G2/G5 name the derivations still owed.
• Minor, Hc3 not total ([12,2,2]): fixed in Hc4 (J2: 0 exceptions on 8,448 short right ends, where Hc3 raised on 12).
• Minor, §4.3 unruled rows incomplete (V1 d = 1, Z empty, p ≤ 0): fixed (§4.3, §4.5 U12).
• New script scripts/inv4.py (H*c4, boxes, CP test); scripts/inv4_blank_4000.txt. check_proof.py: sections G (H*c4), J, K; OPEN lines for measured gaps.
• Result: two fatal-class items remain open (G1 fully, G2 partly: one box leak plus all derivations). Status OPEN.
• 2026-10-12 (skeptic round 2, applied in the same stage):
• Skeptic verdict: not sound. Two fatal gaps, three major, one minor.
• Confirmed by the skeptic:
  • H2t', HL and CP repair round-1 fatal gaps 1-3 where tested, except for the window family;
  • rows U1-U25 match every raise Unruled of macro_sim3;
  • the initial segment;
  • 400 transitions of new kinds against exact simulation (1.0e8 steps);
  • the progress argument and the halting pattern.
• Fatal 1, window family (long right ends reach window hubs, 1 / 60 / ≥ 96 members at S = 83 / 168 / 339): not fixed; analysed.
  • The window start is derived: it is the Clean formula with P0 = d0 + δ (§4.4). Check L1: exact on 60 window right ends.
  • With it, δ = 0 is ruled by the existing rules (one exception with two walls).
  • δ ∈ {1, 2} reaches RightEndP with P ≤ 3 at a wall or a V1 right end with walls (U4, U13). Its restart writes (10)^p (101)^q 1 (101)^r, outside the grammar (L3). So the rule set itself must grow before an invariant can close.
  • The S = 168 long boxes are in check_proof (L4: 60 window leaks; L5: 0 one-step leaks among 1,516,903 E members; L5b: a two-step example). The S = 339 box was re-run with the skeptic's script (§5.5).
  • One corner is now ruled: RightEndP2W (P = 2 at a wall = RightEndP to P = 0 + Absorb0; exact on 251 ruled random frames of 300, negative control, checks M1-M2). With it only the V1 right end with walls stays unruled in the window family (M3). In one followed run ([21,3,38]) the glued word is transient: the orbit is back in the grammar at step 4,685, 1,675 steps after the glued word appears.
  • U4, U13, U17 (successor part) relabelled "refuted by box".
• Fatal 2, short regime (Hs_4 not inductive; box cut at a0 ≤ 80; Pt1 missing): not fixed.
  • The wider boxes are now in check_proof (L6): E1w 110, P1w 12, Pt1 450 leaks; Et1 and Eseg 0.
  • §8 G1 states the bounds and treats the counts as lower bounds.
  • No explicit clause set is known.
• Major, Reflect into a top (U24): not fixed; relabelled "refuted by box". Check L7 runs the chain from [255,35,3]. A rule for Reflect with n a top, a level or a window is missing.
• Major, derivations: partly addressed.
  • The CP sketch is restated as what it is: given Lemma T, CP ⟺ H1 at the successor. Round 1's choice of r was circular.
  • §5.4 is rewritten as an induction over the §4 rules, conditional on H1. It now uses p ≡ q only for walls that are not leftmost; the even/odd collapse wall of a P-even right end is always leftmost.
  • "ak even at Push1" is shown not to be a local parity fact (75 of 163 eats from blank have an odd six-block count) and stays a census fact (G5).
  • Lemma T, G, C and CP are still fitted.
• Major, headline numbers and box bounds: fixed.
  • §5.5 states every box's bounds and reports leaks as lower bounds.
  • The round-1 rows without a saved log (232,794 short E, 36,043 short P) are withdrawn.
  • The §1 status bullets no longer say "one leak".
• Minor, Hc4 not total on degenerate tuples: fixed (inv4.degenerate; J2b: 0 exceptions on 60,000 fuzzed tuples).
• New: scripts/round2.py (window and corner rule patches, chains, wider short boxes); scripts/round2_box339_rerun.txt; check_proof.py sections L, M and J2b.
• Validations re-run: check_proof.py A-L, SUMMARY PASS (36 checks, 0 fail, 11 OPEN, 1,239 s), plus M (2 checks, 0 fail, 1 OPEN). Every leak count the skeptic reported was reproduced exactly: S = 168 P 60/1,079,332, E 0/1,516,903; S = 339 96/4,649,851; E1w 110/445,843, P1w 12/108,831, Pt1 450/1,202,119, Et1 0/143,766, Eseg 0/2,937.
• Result: STUCK. Two fatal gaps remain, each needing new rules or a new invariant vocabulary, not a calculation (§8).