1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE (W4-6)

Status: STUCK (stage chain_law done 2026-10-12, confidence low; chain-length law found, but the steady state ends at k = 650,686: D/F meet double walls and walls merge, so (ii)/(iii) are false; see the last section) Class guess (agent / Dennis): Skelet-like nested bouncer: movable walls between (01) runs, left buffer, multi-level counter / — Spreadsheet notes / Discord thread: Results row "Unknown", no status, no notes, no "Done By". No match in data/discord/*.txt. Unclaimed. Viewer: https://bbchallenge.org/1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE

Checks

• Byte-exact on data/holdouts/BB6_holdouts_740.txt line 99 (778 list line 106).
• Same table up to renaming and mirroring (canon over all 6 starts, 740 and 778 lists): only 740 line 612 1RB0RA_1LC0RA_0LF0LD_1LE---_0LC0LB_1LA0RE (778 line 648) = this table started in state E. That is the only sibling.
• Upstream: vendor/busycoq/verify/Eqv_v3.v (same at BB6 HEAD 9cf9e88) TM1 proves halts 1RB---_0RC0RF_0RD0RA_1RE0RD_1LF0LE_1RC0LE <-> halts this (D1 = 0LB replaced by 0RD). TM4 does the same for line 612, and TM24/TM74 do it for the D- and F-starts of the table. These are equivalences only, with no nonhalt proof. The simplified machine is not on either list, and its tapes at every E left record equal ours (diffed to k = 300). A proof for the simplified machine plus Eqv_v3 TM1 would work only if check_kill accepts the BBinf/TMinf framing. Not checked.

Observation

• sim: no halt to 1e10 (span 140,891). C tracker scripts/avec.c ran to 1e11 (223,095 cycles), no halt, no exception.
• Family. Every E left record (the head is on a fresh cell in E: one record per cycle, followed by an F record one step later) is K(n; a) = 0^inf <E (01)^n 0 (01)^a1 0 (01)^a2 ... 0 (01)^aL 0^inf, with n = k−1 at cycle k. A "wall" is a single extra 0 between runs of 01. It held at all 223,095 records to 1e11 steps (data/avec_1e11.txt.gz). compress's skeleton (10)^a (01)^b 0^2 ... is the same tape, cut at other places.
• Cycle-level facts (data/avec_1e11*.txt):
• a1 is in {7, 8} (4 only at k = 1). a_j is exactly periodic in k with period 2^(j+1) for j = 1..8 on k = 1e5..2.2e5.
• At k = 2^m the first 14 entries are 7 13 25 9 3 10 9 6 34 1 12 15 1 3 for every m >= 13.
• The tail fills with 3s (… 3 3 3 2 4).
• The region right of the buffer grows only when the head reaches the right end, at k = 16, 32, 48, 64, 160, 192, 448, 1472, 1984, 2496, 3008, 3520, then at 3520 + 8192(2^m − 1) = 11712, 28096, 60864, 126400 (+14 cells each, 483 cells at 1e11).
• a_j = 0 (double wall) occurs only for j >= 5.
• Pass mechanics (scripts/check_rules.py, 6,000/6,000 random-context checks):
• Leftward is complete: E reads 1 → L2 (1 <E -> <E 0: an open wall closes); E reads 0, F reads 1 → L1 (10 <E -> <E 01); E reads 0, F reads 0 → L3 (0 0 <E -> 1 0 A>: bounce at a closed wall; on the blank this is the edge step).
• Rightward phases: A/F alternate per pair (R1/R2); C/D is the zigzag pair (R3/R4).
• At a wall: A shifts it one pair right (R5); F opens it (R6: Z becomes an extra 1); C opens it one pair further left (R7) or, behind a mark 11, turns back (R8); D turns back (R9).
• Double walls: R10 (D), R11 (C turns back).
• Coverage on the blank run (scripts/coverage.py, data/coverage_2e7.out): 9,292,537 rule applications. 10,122 steps fall outside the matcher, as follows:
• the edge step (L3 on the blank; the matcher needs written cells): 3 × 2,826;
• "C at a double wall" before R11 was added: 1,191;
• ~600 steps of the right-end routine, ~99 visits;
• a handful of start-up steps. The right-end routine (A/F/C/D> 0^inf) reads a long left context (scripts probe: outputs vary with random contexts). It is not a fixed local rule.
• Halting: the only halt cell is A1, so A must read 1 (B> 0 1 1, B> 1 0 1 1, F> 0 1 1). Leftward bounces are always safe.
• 300 random K(n; a), a_i <= 12, 2e6 steps: 5 halts, all with a1 = 0 and n odd.
• 400 random K(n; a) with a1 >= 1, a_i <= 14, 2e7 steps: 0 halts.
• Sibling 612 (scripts/avec_c TM 3e8 1 E → data/avec_startE_3e8.txt): same family. a1 is in {3, 4}, and the a-vector from entry 2 on equals this orbit's at the same depth by 3e8 steps (e.g. 13 24-26 10-11 1 10 9 5 34 …).
• qsim (block 4, prover on): 200,000 loops, 0 rules, 0 Collatz rules (data/qsim.jsonl). compress track: 38 skeletons, all re-cuts of K(n; a).
• CTL (extracted busycoq CTL62, scripts/ctl/): 25 parameter sets → 20 false, 4 hit the 6 GB cap (NG k=6/9/12 with 48, RWL_mod 4 … 12), 1 timeout (CPS_LRU 12/3200). No certificate.

Candidate rules

See observe.json rules: the sweeps plus R1–R11 and L1–L3 (L4 = L1+L2), all validated 300/300 with random binary contexts and exact step counts. Not yet ruled: - the cycle map K(n; a) → K(n+1; a'); - the right-end routine; - double-wall cases other than R10/R11 (none seen on the orbit besides these to 2e7).

Template check

Nearest proved neighbour per the pick: kill #3 (1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, its .v and proof.md read).

3 is a down-counter on pairs [p,q,d] = (10)^p (01)^q s(d) with digit blocks s(1) = 0001, s(0) = 0010. One cycle is one decrement (three short bounces and one sweep), with macro rules Dec_k, DecMerge, End, Ov, X1 and X2, and the invariant J.

This machine has no digit blocks and no 11 on the stable tape. Its walls are single extra 0s, and one cycle is a nested bounce (the head turns at walls several times per cycle). - What transfers: the proof plumbing. That is #3's sweep lemmas folded over a block list (RP/LP, PassesR/PassesL), K as a list-indexed configuration, and progress_nonhalt_cond with a per-cycle invariant. - What does not transfer: the rule table. Applies: partly.

Cryptid check (ground rule 6)

No sign of pseudo-random arithmetic: - a_j is exactly 2^(j+1)-periodic; - the first 14 entries are frozen at k = 2^m; - right-end reaches come at doubling intervals (8192·2^m); - qsim reports 0 Collatz rules.

So this is not a cryptid candidate on current evidence. The risk is the opposite one: a clean but deep hierarchy (8+ levels) with irregular settled values and no closed form yet.

Checkpoint A (Dennis)

(open; see card.html and decision.json)

Informal proof

Not started (waits on decision.json).

Formalization log

—

Outcome

—

Decision (2026-10-11)

Question: W4-6 and its E-start twin (740 line 612) are a nested wall-bouncer with a clean 2^(j+1)-periodic hierarchy: fund a ~2 h wall-model stage, run only a bigger CTL search in the background, or park both? Answer: wall_model (Fund one ~2 h wall-model stage for both lines). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, wall_model)

Scope (decision.json, answered 2026-10-11): build an abstract simulator on K(n; a) from the local rules plus a ruled right-end routine, check it against the TM to 1e11 for both starts, derive the cycle map, look for the carry invariant, and give a go/no-go on proof.md.

Done 1. Rule set completed (scripts/wallmodel.py RULES, validator scripts/check_rules2.py, data/check_rules2.out). - Validated rules: 22 fixed rules plus 6 sweep forms. Each was run 300 times in random binary contexts, with exact tape, state, head and step count. Result: 8,400/8,400 passed with seed 20261011 and 8,400/8,400 with seed 7. - New rules: - R12 F> 0001 -> <E 0100 (7 steps): F at a double wall. - R13 A> 0001 -> 1000 D> (6 steps): A at a double wall. - F1 F> 1 -> <E 0 and C1 C> 1 -> 0 A>: never used. - The zero-run rules ZA A> 00000 -> 100 <E 01 (6), ZF F> 0000 -> 10 <E 01 (5), ZC C> 000 -> 0 <E 01 (4) and ZD 00 D> 00 -> 00 <E 01 (3). - The right-end routine is local after all. The observe probe ran it until the head came back. Cut at the first leftward E move instead, it is these four zero-run rules, and the ordinary L/R rules do the rest. - R9 and R10 also split into atomic rules: R9 = ZD + L3 + R1 + F1 + L1 + L1 (13 steps); R10 = ZD + L3 + R1 + R2. 2. Rule-only model = TM to 1e11, both starts (scripts/validate_model.sh → data/model_validate_1e11.out). - The model applies only these rules and stops with UNRULED if no rule matches. A halt would show up that way. - Compared at every E left record (k, TM step count, n and the whole wall vector): - start A (line 99): 223,095/223,095 records identical; - start E (line 612): 223,102/223,102 records identical, against a new C-tracker run (data/avec_startE_1e11.txt.gz, no halt). - No UNRULED configuration. Every step from blank to 1e11 is a rule application. - Rules used on the run: L1–L3, R1–R7, R9–R13, ZA/ZF/ZC/ZD plus the 3 sweeps. R8, F1 and C1 are never used. 3. Cycle map (scripts/cyclemap.py, data/cyclemap_check_1e11.out, data/cyclemap_freerun_1e11.out). - One cycle is a sequence of rightward passes and leftward sweeps over the walls. With g = the gap after the wall, the phase on reaching a wall acts as follows:

 | Phase | Rule | Effect on the wall | Next phase |
 |---|---|---|---|
 | A | R5 | shifts right one pair (a pending bounce) | A if g odd, else F |
 | F | R6 | opens in place | D if g odd, else C |
 | C | R7 | opens one pair further left | C if g odd, else D |
 | D | R9 | shifts right one pair, then the head turns | — |

• g = 0 with C is R11. R11 is exactly the generic even-gap move: wall j moves one pair left, wall j+1 one pair right, then the head turns.
• The sweep closes open walls in place. It bounces (L3) at the first shifted wall, which returns to its old place and acts as "A at that wall". A sweep that finds no shifted wall ends the cycle at the edge.
• Phase at wall 1: A iff n is even.
• One-cycle check from every TM record against the next:
  • start A: 223,065 match, 0 mismatch;
  • start E: 223,073 match, 0 mismatch.
• Not covered: 30 and 29 cycles. These are the right-end reaches and the start-up double walls (R10 ×5, R12 ×2).
• Free run from blank (cycle map, with the rule model for the uncovered cycles) reproduces all 223,095 and 223,102 records. 4. Steady state (k > 3,520), to 1e11:
• The only rules used are L1–L3, R1–R7, R9, R11, ZC and ZF.
• Zero gaps are met only in phase C: 85,695 times (R11). A, F and D meet a zero gap only in start-up (D 5×, F 2×, all at k ≤ 3,519).
• The right end is reached only in phase C: k = 11711, 28095, 60863 (one reach each: ZC×2 + ZF×2, appends walls with gaps 2, 4 = 14 cells) and 126399 (two reaches, appends 2 3 3 4). 5. Parity-determined.
• Inflating every gap by 100 (same parities, far from 0) gives identical wall moves and pass counts for 96,000 cycles (k = 126,400..222,400).
• Gap values matter only through their parity and the zero test. The irregular settled values (7 13 25 9 3 10 9 6 34 …) are frozen offsets the dynamics never reads.
• All base gaps are odd. 6. Uniform hierarchy (counts per 65,536 cycles from k = 131,072):
• Wall 2m moves (2^m − 1)·2^(17−2m) times and wall 2m+1 half as often. This holds for walls 2..21 within ±1, through both the irregular prefix and the 3-3-3 tail. Walls come in pairs per level.
• a_j is exactly 2^(j+1)-periodic for j = 1..15 (k ≥ 60,000; observe had j ≤ 8).
• Wall windows (k = 126,400..223,095):
  • walls 4..17: 4 positions each;
  • walls 2, 3: 2 positions;
  • walls 18..35: 2 positions so far (their period exceeds the window).
  • So a gap is base ± 3. A zero gap needs base 3 with both neighbours at the extremes. 7. Long free run of the abstract simulator (scripts/longrun.py A 2^20 → data/longrun_A.out, progress line per power of 2; ~5.5e11 TM steps' worth at k = 2^19):
• to k = 2^19 (524,288 cycles, L = 41) there is no unruled cycle;
• the right end is reached only in phase C, now also at k = 388,543 (126,400 + 2^18, again a double reach);
• zero gaps are met only in phase C (290,365 times);
• the min gap never drops below 0.

Go/no-go on proof.md: no-go for now. - The model is exact and the cycle map is short and parity-only. Both lines (99 and 612) are covered by the same map; they differ only in n's parity offset and a1. - What is missing is the non-halting invariant, which must give all three of: - (i) gaps never go negative; - (ii) a zero gap is only ever reached in phase C (A/F/D at a double wall gives R13/R12/R10, which break the wall structure); - (iii) the right end is only reached in phase C. - These are facts about the counter's reachable parity words. They need the level recursion, i.e. the carry rule behind the (2^m − 1)/2^(2m−1) move rates, which is not derived yet. - Confidence med: the mechanism is now exact, but there is no invariant yet.

Still open - The level recursion: what one visit to level m (walls 2m, 2m+1) does, as a function of the parity word. From it, the 4-position windows and (i)–(iii). - The right-end reach at wall level (empirical only: appends gaps 2, 4 in phase C). - Whether a wall-level closed language (alphabet: gap parity, zero flag, wall status) closes. That would be an alternative to the recursion, but no search was run.

Decision (2026-10-12)

Question: W4-6 and its twin (line 612) now have an exact parity-only cycle map: fund one ~2 h carry stage to derive the level recursion and the invariant, try a wall-level closed-language search instead, or park? Answer: carry_stage (Fund one ~2 h carry stage). Dennis: apply recommendations (2026-10-12).

Funded stage (2026-10-10, carry_stage)

Scope (decision.json, answered 2026-10-12): derive what one visit to a level does to the parity word, from it the move rates, the wall windows and the invariant (gaps >= 0; zero gaps and the right end met only in phase C), test on random words, give a go/no-go on proof.md. Run on 2026-10-12.

Done 1. Recursive form of the cycle map (scripts/carry.py). Walls 1-based, g_w = gap after wall w, g_0 = buffer n; a one-pair move of wall w changes g_{w-1} and g_w by -+1. - cycle(n, a) = Run(1, A if n even else F), then n + 1. - Run(w, A) = Run(w+1, A if g_w odd else F), then Run(w+1, A if g_w odd else F) again (g_w read again; wall w is shifted during the first call and back for the second: net move 0). - Run(w, F) = Leaf_w = Chain(w+1, D if g_w odd else C) (wall w opens in place: net move 0). - Chain(v, C): wall v one pair left, then Chain(v+1, C if g_v (before the move) odd else D). Chain(v, D): wall v one pair right, stop. - So a chain moves walls v..r-1 left through a run of odd gaps and wall r right; all net wall motion happens in chains. - Check: = scripts/cyclemap.py on every record (start A: 223,066 agree, 0 disagree, 29 both unsupported = right end / start-up; start E: 223,074 / 0 / 28; data/carry_check_A.out, data/carry_check_E.out) and on 20,000 random words (13,526 agree, 6,474 both unsupported, 0 disagree; data/carry_random.out). 2. The A-tree is complete. Run(w+1, .) never moves wall w or anything left of it, so g_1..g_w are constant inside Run(w, .). Hence with p = the first wall whose gap is even, an n-even cycle is A at walls 1..p and 2^p F-leaves at wall p+1: Leaf_{p+1}^(2^p). Seen on the orbit (traces 0A 1A 2A 3F 3F ... at k = 2^m - 1). 3. Squaring lemma Leaf_w^2 = Leaf_{w+1} if g_w is odd, and S^-1 Leaf_{w+1} S if g_w is even (S = wall w+1 one pair left, undone after); g_w is the same after Leaf_w^2. - Random words (gaps >= 2): 26,256/26,256 (seed 20261012) and 26,328/26,328 (seed 7), exact positions (scripts/onechain.py random). 4. Every cycle is one chain (scripts/onechain.py cycle1). Applying the lemma p times: an n-even cycle at depth p is Leaf_{2p+1} conjugated by temporary shifts of walls p+2..2p+1 (each where the gap before it is even, read in order); an n-odd cycle is Leaf_1. This is level p = 0, 1, 2, ...: the chain starts at wall 2p+2, which is why each level owns two walls. - Check: cycle1 = carry.cycle on all records (223,066 A, 223,074 E, 0 disagree) and on random words (20,305 and 20,206 agree, 0 differ; 9,695 / 9,794 skipped because the original raises Unsupported). 5. Level law (exact). The level of cycle k is p = t1(k xor c), t1 = number of trailing 1 bits, with c = 4672 = 2^6 + 2^9 + 2^12 for start A and c = 4673 for start E (scripts/levels.py, data/levels_1e11.out). - The mask bits are forced by the data with 0 conflicts (bits 0..16), and the law holds on all 219,492 (A) and 219,499 (E) cycle-map cycles with k >= 3,600: 0 mismatches. - So the time structure is a binary counter whose digits 6, 9, 12 run with the opposite orientation (frozen at start-up). Level p takes exactly a fraction 2^-(p+1) of the cycles, which gives the halving rates and the 2^(j+1) periods. 6. Chain lengths (scripts/chainlen.py, data/chainlen_A.out, data/chainlen_E.out). Every level-q cycle starts its chain at wall 2q+2 (no exception on either line). The number l of C walls is geometric at every level (l with frequency ~2^-(l+1)). - Level 0 (all n-odd cycles): l = t1((k xor c) >> 1 xor m_0) exactly, m_0 = 2^16 (A) or 2^16 + 1 (E): 109,748 and 109,751 cycles, 0 mismatches. Level 0 is a second ruler counter running along walls 2, 3, 4, ... - Levels >= 1: no such law. A ruler of the level-q cycle index with a fixed mask fails on almost every cycle, and l is not a function of the index mod 2^b for b <= 11. The chains of lower levels move the same walls, so the per-level length depends on their history.

Go/no-go on proof.md: no-go. Confidence stays med. - What is now exact and proof-shaped: the recursion (1), the complete-tree fact (2) and the squaring lemma (3), each a short induction from the cycle map. They reduce a cycle to one chain at a known level (4, 5). - Still missing for (i)-(iii): what fixes the chain length at levels >= 1, and so the wall windows. Only a chain changes positions; a chain is safe when its D wall has a nonzero gap after it, the wall before its first C wall has a nonzero gap, and the run of odd gaps ends before the right end except in phase C. The conjugating shifts and the real A-shifts are temporary moves that also need nonzero gaps. - Also open: the right-end reach at wall level (empirical, phase C, appends 2 4 or 2 3 3 4) and the start-up (k < 3,600) handled by the rule model. - The move rates (2^m - 1)/2^(2m-1) are not derived yet: they need the chain-length law.

Still open - Chain-length law for levels >= 1 (the "carry inside a level"). With it come the 4-position windows and (i)-(iii). - A wall-level right-end rule. - The alternative: a closed-language search on the pass/sweep machine at wall level. Fact (2) makes the S/O status pattern a plain binary counter, which helps.

Decision (2026-10-12)

Question: W4-6 and its twin (line 612) now reduce to one chain per cycle at a known level: fund one more ~2 h stage for the chain-length law above level 0, try a wall-level closed-language search instead, or park? Answer: chain_law (Fund one ~2 h chain-length stage). Dennis: b (fund all five), 2026-10-12.

Funded stage (2026-10-10, chain_law)

Scope (decision.json, answered 2026-10-12): find what fixes the number of C walls in a level-q chain for q >= 1, as a function of the lower levels' state; from it the wall windows and the invariant (i) gaps >= 0, (ii) zero gaps met only in phase C, (iii) right end reached only in phase C. Stop rule: if no law fits all cycles to 1e11 in 2 h, both lines go to STUCK. Run on 2026-10-12.

Done 1. Chain-length law found (scripts/chainlaw.py, scripts/chainfit.py). - The law is a selector-masked ruler. Take a level-q cycle k, q = t1(k xor c), and let s = bits q+1..2q of (k xor c) (the lower levels' state, q bits). Then l = t1(((k xor c) >> (2q+1)) xor m_q[s]), with one fixed mask m_q[s] per level and selector value, forced by the data as in levels.py. - Equivalently, [l >= L] at level q is a function of k mod 2^(2q+L+1), and exactly 2^q of the 2^(q+L) level-q residues are positive (checked for levels 0..7 and L = 1..6 where the window allows; data/chainlaw_period_far_A.out). - Fits: - 1e11 window, k >= 3,600: start A 219,492 cycles and start E 219,499 cycles in 935 (level, selector) groups each, 0 forcing conflicts, 0 cycles off the law (data/chainlaw_fit_A.out, data/chainlaw_fit_E.out). - Far window k = 2^24 .. 2^24 + 2^20 (records from the new simulator below): 1,048,576 cycles in 2,047 groups, 0 conflicts, 0 off the law (data/chainlaw_fit_far_A.out). There the level law needs more mask bits: c = 1,184,320 = 2^6+2^9+2^12+2^17+2^20, forced on bits 0..21 with 0 conflicts. The 1e11 window only forced bits 0..16. - How strong the test is: groups at levels 0..5 hold hundreds to tens of thousands of cycles each, so the fit is a real test there. At level 8 there are about 1.7 cycles per group. Groups with a single cycle (levels >= 9 in the 1e11 window, >= 10 in the far window) fit trivially. - The masks are irregular constants: 2^q per level, with no formula in s. They are the frozen gap offsets read through parity. - The masks are not time-invariant. A joint fit of the two windows has 0 conflicts at levels 0..4, but 1,067 conflicts at levels 5..9 (854 cycles off the law; data/chainlaw_fit_joint_A.out). Long chains at those levels read walls that changed between the windows (item 3). 2. Faithful fast simulator (scripts/hyb.c, scripts/hyb2.c). - The cycle map runs in C. Every cycle the map does not cover (a zero gap met in phase A/F/D, the right end, a sweep meeting an untouched wall) is run by the TM itself, cell by cell, from K(n; a) to the next E left record, and parsed back. The run stops on a halt or on a non-K tape (TAIL). - Every ~4e6 cycles one ordinary cycle is also run by the TM and compared. - Checks: it reproduces the 1e11 record k = 223,095 of line 99 exactly (cross-checks 223/223 at every 997th cycle), and the E-start run gives the same event list shifted by one cycle (data/hyb_E_2e25.out, data/hyb_E_2e26.out). 3. The target invariant is false beyond 1e11. - Long run from blank, start A (data/hyb_A_2e28.out; finished, see item 6): - At k = 650,686 (about 8.5e11 steps) D meets a zero gap (R10, a double wall near wall 19). The walls merge (L 41 -> 39), and at k = 650,687 the right end is reached in phase D. The earlier data/longrun_A.out already had this event in its k = 2^20 line, but the wall_model notes stopped at 2^19. - After start-up (k > 3,600) there are 7 zero-gap events in non-C phases by k = 2^26: - D (R10) at k = 650,686, 1,437,118, 1,699,262, 7,204,286, 15,592,894 and 61,730,238. Each merges walls: L -2, -2, -2, -4, -2, -2. - F at a double wall (R12) at k = 44,953,023, a level-26 cycle: the record has g_1..g_25 odd, g_26 = 8 and g_27 = 0, so F at wall 27 reads a zero gap (item 5). That one cycle takes 5.4e10 TM steps. It rewrites everything right of wall 26 and reaches the right end (L 50 -> 59). - The right end is reached in phase D 5 times (each right after a D merge). - Zero gaps met in phase A: 0 to 2^26 (about 9e15 steps). In phase C: 51.9 M. - Every record is still K(n; a): no TAIL, no halt. - Timing. Every right-end reach after k = 126,399 falls on a cycle with t1(k xor c) >= 17, and every D merge on the level-0 cycle just before such a cycle. Only c's bits 0..16 are certain; higher bits can still change (e.g. k = 28,175,807 has level 24 by its record). - Where the merges happen (scripts/hyb2.c prints the record before and after every uncovered cycle; data/hyb2_A_events_4.5e7.out): - The first three merges sit right after wall 18. At k = 650,686 the gaps g_17..g_21 go 5 4 0 7 2 -> 5 13 2 3 4: the double wall and one more wall vanish. - g_18 then grows at each merge (13, 21, 26) and settles in 24..28. Walls 18..22 now take 4 positions each, like the core. - The next merges sit further right (k = 7,204,286: g_21..g_25 = 4 0 7 2 0 -> 13 8 2, four walls gone). - So the frontier settles in steps, and each step passes through a transient with merges. - The high region is irregular. Beyond wall ~17, merges and right-end reaches write gaps such as 24, 16, 15, 13, and double walls persist in the records. Min gap = 0 holds in 54.4 M of the 67.1 M records to 2^26. The low walls look undisturbed: at k = 2^m the first 15 gaps are 7 13 25 9 3 10 9 6 34 1 12 15 1 3 5 for every m = 16..25 (the 16th is 3 for m = 17..25), and the chain-law masks of levels 0..4 are the same in both windows. - New figure img/farmap_2e25.png: one row per 32,768 cycles to 2^25. The left part is fixed; the jumps in the right part are the merge events. - Both lines have identical event lists to 2^26, including the R12 at k = 44,953,022 for start E (E = A shifted by one cycle; data/hyb_E_2e26.out). 4. What the non-C zero-gap events do in general (random K(n; a), a1 >= 1, gaps 0..5; scripts/eventclass.py → data/eventclass_random.out; the cycle is run by the rule model):

• One TM cycle from 1,000,000 random K(n; a) with a1 >= 1 (scripts/closure.c → data/closure_random.out): 0 halts. But 72–700 words per batch (0.02–0.35 %) leave the K family (e.g. a misaligned (10) run after an R13), so K(n; a) alone is not a closed language.
• So the orbit's safety rests on A and F (almost) never meeting a double wall, in a high region whose layout changes at every merge.

5. Where A and F can meet a zero gap (a record-level condition, from the recursion of carry.py). - A meets a zero gap exactly when n is even and the first even gap g_p (counting from wall 1) is 0. That is the end of the A-tree; the other A-reads are odd gaps. - F meets a zero gap exactly when n is odd and g_1 = 0, or n is even and g_{p+1} = 0. The reason: the 2^p leaves at wall p+1 move wall p+2 once each, alternately right and left, so g_{p+1} only alternates between two adjacent values. - Checked on 200,000 random words against the cycle map (data/afcheck_random.out): 47,465 predicted A cases, all observed; 40,949 predicted F cases, all observed; no case observed without the prediction. - On the orbit (data/firsteven_A.out) the first even gap at an n-even record is always >= 4, taking the values 4, 6 and >= 8: on all 109,748 records k = 3,600..1e11 and on 524,288 far-window records. That is why A never meets a zero gap. - g_{p+1} takes the values 1, 3, 4, 6, 7 and >= 9 there, so F is safe in those windows. It is 0 once later, at k = 44,953,023. - Safety from R13/R12 therefore reduces to two record conditions on the first even gap and the gap after it. The D merges (R10) are the part that has no record-level form yet.
6. Long run finished: k = 2^28 = 268,435,456 cycles from blank, start A (about 1.4e17 TM steps; data/hyb_A_2e28.out). - No halt, and every record is of the form K(n; a). All 67 TM cross-checks agree. - No new non-C zero-gap event after k = 61,730,238. Totals including start-up: A 0, F 3, D 11, C 184.8 M. - One more right-end reach, at k = 212,725,183 (phase C, L 57 -> 59; that one cycle takes 5.6e10 TM steps). L = 59 at 2^28. - Start E to 2^26: the same events, one cycle earlier.

Go/no-go on proof.md: no-go. Confidence drops to low. - The chain law is exact, but it is a periodicity law with 2^q irregular masks per level, and the masks of levels >= 5 change when walls merge. It describes the counter between merges. It cannot give an invariant valid for all time. - Invariants (ii) and (iii) are false on the orbit (R10 x6, R12 x1, right end in phase D x5 by k = 2^26). - A proof needs an invariant that allows merges, right-end reaches in any phase, and an irregular high region, and that still keeps A and F away from double walls (F already failed once, at k = 44,953,023). No such invariant is in sight. - Per the decision this would be the stop case. The literal trigger (no law to 1e11) did not happen, but the law it was meant to unlock does not lead to (i)–(iii). Both lines go to STUCK.

Still open - A merge-tolerant invariant. The likely shape is a wall-level closed language over (gap value capped at ~4, wall status, phase) that includes R10/R12 and the right-end routines and excludes R13 and misalignment. It would be searched natively and is untried. The irregular high region makes success unlikely within one stage. - Whether A ever meets a double wall (R13 can misalign the tape), and if so what follows. To 2^28 (about 1.4e17 steps) it has not happened. Going further needs a leaner TM fallback: the cell array of scripts/hyb.c reaches the 6 GB cap near 2^30. - Bug note: scripts/longrun.py drops the rule model's TAIL in fallback cycles. No TAIL ever occurred, so its numbers stand. scripts/event.py and scripts/hyb.c stop on a TAIL instead.