1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD

Status: CHECKPOINT_A (observe done; confidence low, so proof work waits for Dennis) Class guess (agent / Dennis): Sync bouncer counter, an SBCv8 TM31 cousin (binary counter left, ternary throttle right, nested overflow pause) / — Spreadsheet notes / Discord thread: sheet results row 106 = Unknown, no status/notes/links/strikethrough; classifications col AK (Unknown). Not in dyuan's Oct 1 list of 24 or mxdys's Aug 24 UBRRBA list of 86 (data/discord/). Present in all 26 holdout snapshots, including the newest (2026-10-07_778). Not claimed, so not skipped. Viewer: https://bbchallenge.org/1RB0RA_1RC1RF_1LD0LC_1RA1LE_1RA0LC_---0RD Pool: reserve R8 (reports/targeting.md §4.4): 1 transition from SBCv8.v TM31 (F1 0RD vs 0RE), "odd growth (t^0.85)", risk Medium.

Observation

Simulations (all from blank): - tools/sim.py to 1e9 (span -92..53186, 32,920 nonzeros) and 1e10 (span -99..191426, 126,623 nonzeros, 191,526 cells; records_1e10.jsonl); no halt. - Own C trackers (scripts/sweeps.c, scripts/ovf.c; they match sim.py and the Python tracker exactly to 3e8) to 2e11: no halt, right edge 886,362 (sweeps_1e10.txt, sweeps_2e11.txt, ovf_1e10.txt, ovf_2e11.txt). - tools/compress.py track to 1e9: compress_track_1e9.txt. qsim/rulefit not used: the structure was decoded directly (rulefit's sweep row in reports/rulefit-sweep.tsv is "partial").

Layout at the canonical point (the head steps from cell 300 to 301, moving right; positions absolute, after step ~3e8):

cell  -87      -86 .. 3             4..15          16..21   22..300 | 301..618          619..622  623+4j   marker  (0011)^e .. right end
      1(wall)  D_15 .. D_1 (6 each) 110111 011101  D_0      (1110)^70 D> (0011)^79 ...  s3        t_j      1011    big region

• Left counter: binary, MSB on the left; digit 0 = 001101, 1 = 101101 (in -130 alignment these read 010011/011011; 011011 is TM31's d). The LSB sits at 16..21 behind a fixed 110111 011101. The wall is a 3-state top digit, so the capacity is 3·2^m trips (measured between overflows: 3062, 6133, 12272, 24563, 49129, 98230, 196597 = 3·2^10..3·2^16 minus the previous residual).
• Middle: 150 four-cell blocks, transparent. A rightward pass turns 0011 into 1110 (aligned at cell ≡ 1 mod 4) and the leftward pass turns them back. The head zigzags inside each block, as in TM31's segRLs passes.
• Right throttle: with P=1001, Q=1011, R=1000 (cells read one cell later than the 4-cell groups 1100/1101/0100/0101):
• s3 cycles P→Q (bounce), Q→R (carry), R→P (carry), so it forwards 2 of every 3 trips.
• The K ternary digits use P=0, R=1, Q=2: 0 and 1 absorb a trip, 2 carries.
• The carry-out of the top digit runs the head to the right end, which appends one block (right edge +4).
• Penetration fractions measured to 3e8 are exactly 1, 2/3, 2/9, 2/27, 2/81. Round trips per record alternate 40/41 (K=3, 81/2) until step 1.474e8, then 13/14 (K=2, 27/2) for all 216,000 records up to 2e11.
• Growth: right edge ~t^0.70 over 1.3e8..1e10 and tending to t^0.5, because every record trip also sweeps the whole right region. The left edge grows like log t.

Overflow events (the left counter is full):

• The pause (each overflow): the head stays left of about cell 50 for about 80·2^m steps. The left turnaround depths run through a ruler sequence (-17, -23, -29, …, a recount of the 6-cell digits). The right turnarounds (13, 23, 27, 31, …) build an inner counter of 4-cell digits at the start of the middle. Its digits use the same P/Q/R alphabet as the throttle (data/left_records_1.5e8.txt).
• Ordinary ending: the pause ends with a new left record, a few repair trips (turnarounds at 39, 51, 48, 48, 52, 52), and then normal trips through the middle. The residual counter value is 10..23.
• m = 14 ending (the only one in m = 9..18): the right turnaround restarts at cell 28 and creeps right 4 cells per round trip (47, 55, 59, …, 299, 303, …, 622). This rebuilds all 150 middle blocks, about 150 trips (Fig: img/creep_special_1.487e8.png). Afterwards the throttle's top digit is gone: the marker moves from cell 635 to 631 and the big region starts 4 cells earlier, so K goes from 3 to 2. That period's record gaps were 121 (= 80 creep trips past cell 300 + 41) and then 28. The left residual was 77.
• Robustness (scripts/kdrop.py, kdrop_m1.py): from the real configuration at 3e8, removing digits by hand still runs the same regime. K=1 gives gaps 4/5 and K=0 gives 1/2 (2e8 steps each); K=-1 (s3 removed too) gives a record every trip (1e8 steps). No halts.
• Halting: halting needs A to read 0 1 0 (A0=1RB, B1=1RF, F0=---). Every validated rule avoids this. Any halt would have to come from the unruled pause or creep.

Diagrams (img/, all tools/diagram.py, Default colours; mid-run starts use data/cfg_<step>.txt): default_site_1e4.png (site view), records_1e8.png (records to 2.28e7), overflow_ordinary_3.6e6.png (every 50 steps, cells -80..119), creep_special_1.487e8.png (every 250 steps, cells -100..699), right_counter_3e8.png (every 10 steps, cells 590..669), plus viewer.html (all site views).

Candidate rules

Canonical point C = the head steps from cell 300 to 301 (state D). One rule application = one round trip, from C to the next C.

Validation (scripts/validate_rules.py): the real configuration at the first canonical point after 3e8 was edited with random V < 2^16 − 1, random s3, random K ∈ 0..5 (the marker and big region shifted) and random digits (a quarter of the instances all-2, to force carry-outs). One round trip was then simulated. - Seed 1: RL/RS/RT/record 300/300 (validation.json). - Seed 2: the same four rules plus RM (middle unchanged) (validation_seed2.json). - OV holds as stated for 9 of the 10 real events.

Template check (SBCv8.v TM31, line 9675; diff F1 0RD vs 0RE). TM31 has the same vocabulary: the 10 wall, d=011011, w=0011/0110, and a (1110)^e right region. Simulated, its tape at right records reads 0^inf 10 … (1011)^30 0 (1101)^451 … (1110)^4416. But its right edge grows in bursts (no right record from 4.65e8 to 1e9), and its proof's invariant (P ls i c, BigStep312) does not match our steady ternary throttle or our overflow pauses. What is reusable is the Longitudinal machinery: segRLs_addmul_v2 transfer lemmas, Incs_d/Incs_w style, and DivModCases for the mod-3 digits.

Cryptid check (ground rule 6). No pseudo-random arithmetic in the normal regime: the counters and the throttle are exact. Open point: the creep trigger. Only m = 14 of m = 9..18 crept. If the trigger depends on, say, the base-3 digits of ~2^m (the pause feeds about 2^m trips into a ternary inner counter), then when K drops is pseudo-random. The robustness tests suggest the drops are harmless down to K = −1. The behaviour of a creep with no digits left is untested. Verdict: not a cryptid candidate yet; flagged as a risk.

Checkpoint A (Dennis)

Questions are on the card: (1) the creep picture, (2) the ordinary pause picture, (3) a priority call: decode the pause/creep in a deepen stage, or park. Confidence is low, so no proof work starts before his answer.

Informal proof

Not started (blocked on Checkpoint A, low confidence).

Formalization log

—

Outcome

Open. Observe stage done 2026-10-10 (about 2 h). Next, if Dennis says go: rules for the pause (the inner P/Q/R counter fed by the left recount), its exit condition (creep or not), and a creep at K ≤ 0.

Decision (2026-10-10)

Question: Spend one deepen stage, with a stop rule, decoding the overflow pause and the creep, or park R8? Answer: deepen (One deepen stage (2 h): the pause's inner counter, both endings, and creeps at K <= 0). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, deepen)

Scope (decision deepen): rules for the overflow pause and both of its endings, and creeps at K <= 0; stop with CRYPTID_CANDIDATE if a branch that matters for halting depends on the trigger arithmetic. New scripts are in scripts/funded/ (C runner runcfg.c and dumper cfgdump.c; Python test drivers), and new data in data/funded/.

What the pause is. - Universal start. At every overflow the left counter is all ones and the inner zone is fixed. At the 8 real pause starts m = 9..16, cells -10..90 at the canonical point are identical, and the left zone is (011011)^(m-2). So the pause and its ending depend on m alone. A pause start built for any m from the m = 10 right part (cfg.set_left) reproduces the real endings: for m = 9..18 only m = 14 creeps, as in the 2e11 run. - Inner throttle. The inner zone at cells 2..17 is a second throttle in the same P/Q/R alphabet: s3' (2..5), digits t0 t1 (6..13), marker Q (14..17). Normal trips pass it unchanged. In the pause, a pause-mode binary counter (digits 011010/011011 in -130 alignment, wall 000001) sends every trip into it. - PJ. s3' works as a rotor together with the junction cells -10..1. (J, s3') -> (J', s3', passes?) is a deterministic table with 20 entries. - PI. A trip that passes s3' adds 1 to the ternary pair t0 t1 (P=0, R=1, Q=2). The trip carries out iff both digits are Q. - Middle-start counter MS. Inner carry-outs feed a third counter that grows into the middle from cell 22 (4-cell blocks .=0110, 1=1110, 2=0010 in 2-mod-4 alignment). - PM. d1 is an s3-type rotor: .->1 stops, 1->2 carries, 2->. carries. The digits d2.. are ternary (.=0, 2=1, 1=2, LSB first). A carry past the last digit appends one. - PI and PM: 23,495/23,495 trips on 16 random-start pauses (m = 9..11, random t0 t1 and MS word; pausetrips.py M SEED + checkpause.py), plus 3,810/3,810 on the real m = 10, 11 pauses. The only mismatches are trips after the final left record, which belong to the ending. - Phases and length. The pause has three left records: the start pair, one in the middle, and the end pair. m = 10: trips 1, 508 and 1524 of 1531; m = 14: trips 1, 8128 and 24382 of 24412. The inner state at the pause end has period 6 in m (t0 t1 = QQ, RQ, QR, RP, QP, RR for m = 9..14, then repeating to m = 20). The MS word does not repeat: m = 10 2.211, m = 14 22111122, m = 20 .1.1122211.2. It grows about 0.63 digits per m. - Scan. Constructed pauses m = 3..27 never halt. Creeps happen at m = 5, 14 and 22; m = 5 lies in the start-up range, where the creep overlapped a wall step. All other m end ordinarily.

The endings. - The sweep (CL). After the final overflow left record, normal-mode trips clean the inner digits (R -> P stops a trip, Q -> P lets it pass). They then sweep the MS word back to . from the left, one segment per trip. - Ordinary ending. The sweep dissolves; any remnant (?2) is gone after one more trip. - Creep. The sweep leaves exactly one glider 12 (1110 0010). Each later trip bounces off the glider and pushes it 4 blocks right, so crossing the 150-block middle takes 31..37 trips. This is the creep of the observe stage. - Validation. 1,700 random MS words (cleantest.py): 600 of length <= 14 with the real throttle, 600 with random throttles K = -1..5, and 500 of length <= 60. Results: 0 halts, 1,700/1,700 with the middle clean afterwards (cells 22..618 equal a normal canonical point). Every creep was a single glider; no instance had two. Mid-pause closure (pausetest.py): 550 instances (random m = 8..16, random point in the pause, random t0 t1 and MS word; 150 also with random throttles) gave 0 halts, 550/550 clean, 48 creeps. - Absorption (AB). The glider merges into the right throttle and the run returns to the normal regime with K' = K or K' = K - 1. - Exhaustive over every throttle state with K = 0..4 (absorbgrid.py, 363 states): 0 halts, 363/363 clean. K stays in 307 states and drops by one in 56; it never drops for K <= 1. - Across all tests with random throttles, K never rose and never fell by more than one. - Forced repeated creeps (creepiter.py): 3 -> 2 -> 2 -> 2 -> 2 -> 2. K = -1, 0, 1, 2 and 5 stay unchanged over 4 creeps each. - In the real run the throttle at arrival is Q RQQ, which loses a digit. That is why m = 14 took K from 3 to 2. - K = -1 (no s3, marker at 619). Normal trips there: RL, RM and the marker hold, and every round trip is a record with right edge +8: 300/300 (validate_km1.py). This is a fixed point of every ending and of MO (below). - Wall step RW. In normal mode, wall 001011 -> 010011 and all-ones digits -> zeros; RS, RT and the record rule are unchanged. 400/400 over two seeds, with 3..20 digits and random throttles (validate_wall.py). This was the one normal-regime event that had no validated rule.

A new far-future regime (MO). MS grows about 0.63 digits per m, so near m ~ 236 (~10^72 steps) it fills the 149 middle blocks and carries into the right throttle. After that it does so many times per pause. Constructed tests (MS = d1 + 148 maximal digits): - 120 single overflows with random throttles: 0 halts, 120/120 clean. K stays or drops by one: K = 0 -> -1 in 6/16, K = 1 -> 0 in 11/27, and K = -1 stays in 22/22. - 60 pauses with 5 forced overflows each: 0 halts, 60/60 clean. K stays in 58 and drops by one in 2. - An overflow can leave a transient 0000 digit in the throttle; the next trips clear it. - K = -1 with overflows: 70 more runs (30 pauses with 5 overflows, 40 single overflows) all end with the marker Q at 619 and the big region right after it (msrepeat_km1_seed2.jsonl, pausetest_fullms_km1_seed5.jsonl).

Verdict on the stop rule. Which m creep (14 and 22 in 9..27) depends on the MS word at the pause end, which is pseudo-random in m. But no tested branch that matters for halting depends on it: ordinary ending, creep, absorption and MS overflow all return to the normal regime with K' in {K, K-1}, and K = -1 is a fixed point. Not a cryptid candidate. In all 2,863 logged constructed runs of this stage (data/funded/*.jsonl) there was no halt, and every run ended with a clean middle.

Still open (why confidence is med, not high). - CL, AB and MO are validated only as set-valued macro rules (ordinary or one glider; K' in {K, K-1}), not as exact block rules. Which words leave a glider, and which throttle states lose a digit, is not decoded. - A per-block transducer for the sweep, using the entry state of each block as the signal (transducer.py), is not a function: the leftward pass and the zigzags carry extra context. - The digit loss does not follow from the number of trips left before the next record (absorbgrid data). - The pause-mode left counter, with its wall 000001 and three left records, is validated only end-to-end. - MO is covered only by constructed probes. - The proof needs exact rules for these three events, or a closed regular-language invariant over the decoded block grammar that is checked natively.

Next. One stage to turn CL, AB and MO into exact block rules (enumerate short words with two-sided context), then proof.md. A new decision.json asks Dennis to choose between that, proof.md now, and parking.

Decision (2026-10-10, auto-applied)

Question: Spend one more stage deriving exact block rules for the sweep, the glider absorption and the MS overflow before proof.md, start proof.md now, or park? Answer: exact_rules (One stage (2 h): exact rules for the sweep, the absorption and the overflow). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.

Funded stage (2026-10-10, exact_rules)

Scope (decision exact_rules): exact rules for the ending sweep (CL), the glider absorption (AB) and the MS overflow (MO), plus the pause-mode counter as a per-trip rule. Stop rule: if an event still has no exact rule after 2 h, proof.md takes it as a validated lemma and flags the gap. New scripts are in scripts/exact/ and new data in data/exact/.

The key change of view: visits, not trips. Count visits at a fixed block boundary, as busycoq's Longitudinal segRLs does (TM31 in SBCv8.v uses the same machinery). A visit is the head crossing the boundary rightward and coming back. Blocks are 4 cells in 2-mod-4 alignment (block k = cells 2+4k..5+4k). The boundary at cell 18 sits between the inner zone and the MS word. After a pause ends, the visits there are exactly DC^a AC AC AC ... (D or A in, C out). Every rule below is per visit.

Inner zone (exact, finite table). At the pause end the inner zone (s3', t0, t1) emits a DC visits at cell 18, then only AC visits. a is a fixed 27-entry table (scripts/exact/validate_cl_tab.py; for example PRQ -> 4, PQR -> 5, PRR -> 0). It does not depend on the MS word: 27/27 states, 8 random words each (data/exact/innertable.txt).

CL, the sweep (exact). Read the word from cell 18 as ternary digits, LSB first, with .=0, 2=1, 1=2. 0 = 0000 is a transient junk block. The frontier is the first non-. block. - A DC visit adds 2 to the word, with the LSB at cell 22 (d1). - An AC visit acts on the frontier: - frontier 0 -> . - frontier 2 -> 0 - frontier 1 -> ., and the rest of the word gets +4. Inside the visit the 1 block cycles x -> v -> P -> d -> ., sending four B signals right, and a B signal is a ternary increment (.->2 stop, 2->1 stop, 1->pass). - an all-. word passes the visit on into the middle. - Glider = 12, the only fixed point: 12 -> .12 (1 + 4 = 5 = 12). It moves one block per AC visit. - Closed-form outcome. Let v = value(MS word) + 2a. Iterate g: strip factors of 3 (free); v ≡ 1 (mod 3) -> (v-1)/3 (2 visits); v ≡ 2 -> (v+10)/3 (1 visit). Since g decreases for v > 5, it always ends at 0 (ordinary) or at 5 (glider). Of v < 3^10, exactly 3^8 give a glider. - Validation (validate_cl.py): 800/800 random pause ends. 500 had words of length <= 14 (seed 2); 300 had length <= 60 with random right throttles K = -1..5 (seed 3), plus random s3' and t0 t1. - 19,732/19,732 visits matched the predicted block word (blocks 4..150) exactly. - The predicted outcome matched in 800/800 (92 gliders, 708 ordinary), and the DC count matched the table in 800/800. - There were 0 halts, and no visit other than DC/AC appeared. - The glider runs check the one-block-per-visit move across about 140 blocks.

The creep trigger is now an exact formula. trigger.py runs pauses to their final left record and applies the formula: - m = 9..16: the 8 real pauses. m = 17..26: constructed from the m = 10 start (m = 27 was still running at write-up and appends to the same file). - The prediction matched the actual ending at 18/18 pause ends: gliders at m = 14 and m = 22, ordinary otherwise (data/exact/trigger_m9-27.jsonl). - The MS value at the pause end follows v_m = 2·v_{m-1} + 2ε_m, where ε_m has period 6 (+2, +2, +2, 0, 0, 0), like the inner state (112, 226, 454, 910, 1820, 3640, …, 14,913,080 at m = 26). - So the trigger is "the ternary map g applied to about c·2^m". This is pseudo-random in m, but both outcomes are safe, so it is still not a cryptid.

Glider transport (exact, Longitudinal form). In the visit list at each middle boundary, the glider is the prefix G = [BC, BE, BC, BC, BE]. A . block maps G ++ AC^(n+1) to G ++ AC^n: each . absorbs exactly one AC visit (scripts/exact/visits.py 22111122 PP 2e5 4 30, blocks 13..30; macro.py is the 4-cell block macro table, pervisit.py/rules.py the per-visit rewrite search). This is a TM31-style segRLs lemma (segRLs_addmul_v2 shape).

AB, absorption: the B phase is exact. The glider reaches the throttle as exactly five visits (B in, E out) at cell 618, followed by the normal (A in, E out) visits. Each B visit acts on the throttle word s3 d0 .. d_{K-1} (P=0, R=1, Q=2; the marker Q ends it) with the same frontier rule as CL: - frontier Q -> P, and the later digits get +4 (carry out of the top digit dropped); - frontier R -> P over two visits, with the next block turned to junk in between (P -> 0001, R -> 0000, Q -> 0011); - all P: the visit passes the marker into the big region, leaving junk there that a later carry-out run sweeps away.

Checked exhaustively for K = 0..4 (bvisit.py + check_bvisit.py, data/exact/bvisit_K*.jsonl): - all 363 throttle states: 363/363 visit lists, and 1,815/1,815 B visits exact; - K-drop predicate: K' = K-1 exactly when an R step is still half done after the fifth B visit. It matches the observed K after in 363/363 states (56 drops, 307 stays; data/funded/absorbgrid_*.jsonl). This is why K never falls by two.

Still open (why confidence stays med). - AB tail. How the first normal AE visits finish a half-done R step, and remove the marker, is not written as a rule. The K outcome is exact; the resulting digits are validated only for K <= 4 (exhaustive) and on random throttles. - MO. Not decoded in this stage. The expected form is that an MS overflow carry reaches cell 618 as B visits and follows the same B-visit throttle rule. That is untested; MO stays a validated set-valued lemma (190 constructed probes, funded deepen stage). - Pause-mode counter. Still validated end-to-end only (no per-trip rule written). - Stop-rule outcome: proof.md comes next, with the AB tail, MO and the pause counter as validated lemmas, flagged.

Next. proof.md (informal, TM31-style visit counts) using: RL/RS/RT/RM/RW; PI/PM; the inner table; CL with g; the glider segRLs rule; the AB B phase and K-drop predicate; flagged lemmas for the AB tail, MO and the pause counter.

Decision (2026-10-10, auto-applied, round 3)

Question: Write proof.md now with the absorption tail, the MS overflow and the pause counter as flagged lemmas, spend one more stage making them exact, or park? Answer: proof_now (Write proof.md now (the stop rule)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, proof_now)

Scope (decision proof_now): write proof.md with the absorption tail, the MS overflow and the pause counter as explicitly flagged lemmas, validated in check_proof.py. New: proof.md, check_proof.py, scripts/proof/ (zones.py zone drivers; C trackers rle2.c, vis.c), data/proof/ (visit runs to 1.3e10, check logs).

New structure: three zones that only talk through fixed answers. Split the tape at cells 18 and 618 (busycoq Longitudinal style). - In the run from blank to 1.3e10, b18 sees only AC/DC visits (833,504) and b618 only AE/BE (803,803). - So zone L (cells <= 17) is autonomous: its visit word at b18 is fixed, A^N D^c A^N D^c ..., with one D-run per counter overflow. - Zone M (18..617) and zone T (>= 618) only consume visit words.

This turns the old trip rules into per-visit rules: - M is an exact ternary word (blocks 4..153, .=0 2=1 1=2, junk 0): - D: +2 at block 5; - A: the CL frontier rule, or a pass to T as an A when blank; - a carry of c out of block 153: c B visits at b618. This covers the glider exit (1 + 4 = 5 B) and the MS overflow MO (1 B per overflow carry). - Check ZM: 160 random instances, 14,428/14,428 visits exact. The ending takes at most 300 A visits, so T gets one B-burst per epoch, followed by at least 2,700 A's. - T: TA (A visit = s3 rotor + ternary increment, carry-out e+1; K = -1: e+2) 4,800/4,800. TB (B frontier rule on the throttle) 1,200/1,200. - Epoch table from the full run (m = 9..17): c_m = 58, 117, 232, 455, 911, 1820, 3642, 7285, 14568. N_m = 3·2^m - δ (δ in {2,4,6,8}). B-bursts of exactly 5 only at m = 5 and m = 14. - check_proof.py --long (seed 1, data/proof/check_proof_long_seed1.txt) reruns the C trackers from blank and the cfgdump to 3e8, and compares them with the stored files.

Flagged lemmas (proof.md §8): - F1, zone L per epoch (the pause counter): D^{c_m} A^{N_m}, N_m >= 3000, pause m -> pause m+1. Validated only. - F2, the absorption tail: B^5 A^2600 -> canonical T with K' in {K, K-1}. - 40/40 throttles with K <= 2. This is the whole reachable range: K = 2 at S0, and no rule raises K. - New negative finding: for K = 3, 3 of 81 throttles (RRRP/RRRQ/RRRR) end in a non-canonical "dead slot" form. A 0011/0000 block sits between the digits and the marker, and the marker does not move. The earlier full-machine grid did not check the throttle's form. Not reachable from S0, but the old claim "K' in {K, K-1} always" was too strong. - F3, MO: B^j A^2600 for all j. 40/40 random tests (K <= 2, j <= ~2,700) never halt and answer E, but only 34/40 end canonical. The rest end with a dead slot (e.g. T(RRQ), j = 3) or leftover big-region blocks. So F3 is false in its canonical form and needs a wider closed family (data/proof/check_proof_long_seed1_before_F3_restatement.txt has the original failing statement). - New: in the MO regime (m >~ 236), j_m roughly doubles each epoch, so it is unbounded. - For j beyond the throttle value, B visits pass into the big region and build a third counter there (digits 0011/0111/0001), which the throttle's carry-outs then dismantle. This is the weakest point. - TNEG: T is not safe for arbitrary visit words. T(RR) on B A^7 B A^8 B answers C, which breaks the decomposition. The proof therefore depends on the burst shape (one burst per epoch, then >= 2,700 A's), which M guarantees.

Outcome. proof.md is a conditional proof: section 6 (Inv(m) -> Inv(m+1) for m >= 15, start at S0 = step 300,032,133) is complete given F1-F3. Confidence stays med: F1 and F2 are labour, but F3 is a genuine third nesting level with no rule and is unbounded in j. Next: a decision (F3 first, F1/F2 first, or park).

Decision (2026-10-11)

Question: Spend the next stage on F3 (the unbounded overflow bursts into the throttle), on F1 and F2 (the pause counter and the absorption tail), or park? Answer: f3_first (One stage (2 h) on F3, the riskiest lemma). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, f3_first)

Scope (decision f3_first): find a closed invariant family for zone T under the MO bursts B^j A^n, decode the big-region counter (0011/0111/0001), and test j up to 1e6 natively. Stop rule: if no closed family emerges, the far-future regime (m ~ 236 on) is open, so park or make a priority call. New scripts are in scripts/f3/. tzone.c is a C zone-T driver with a per-visit step cap (TZCAP); tz.py wraps it and has the tower parser. New data is in data/f3/.

Result: no closed family. The big region is a fourth zone with the same shape as M. Its gliders build new throttle levels at the right end, so the far future is an unbounded tower of levels. A T level is safe for the burst shapes tested so far, but not for every shape the deeper levels can receive. The stop rule applies.

1. The big region BR is an M-type ternary word (exact). Read the region after the marker as 4-cell blocks (3-mod-4 alignment, LSB next to the marker): s = 0011 (0), y = 0001 (1), x = 0111 (2), _ = 0000 (junk). Its left boundary sees only AC and DC, the same alphabet as b18. - BA: an A visit adds 1 at block 0. - BD: a D visit follows the frontier rule: _ -> s, y -> _, x -> s with +4 at the next block. If the word is all s, the visit runs to the end and appends one s (a record).

This is M with the roles relabelled: BR's A is half of M's D, and BR's D is M's A. So CL's map g, the glider xy (value 5) and the length bound all carry over. Validation (validate_br.py, 2 seeds × 300 random words, --nojunk): 40,766/40,766 visits exact, every answer C (data/f3/validate_br.txt).

2. Interface T -> BR (exact). - IA: an A visit sends D^c to BR, where c is the carry out of the throttle. At K = -1 it sends D D (that is the e+2). - IB: a B visit on an all-P throttle passes as A A (+2). The throttle is unchanged.

Validation (validate_iface.py, 2 seeds × 400 random throttles K = -1..4 with random BR words): IA 16,971/16,971, IB 2,637/2,637, with answers E at 618 and C at the BR boundary (data/f3/validate_iface.txt). So an MO burst B^j becomes +2j' on BR, where j' is j minus the B's the throttle frontier absorbs. The A-run then sweeps it with g, using one D per throttle carry-out.

3. New levels (exact in tests). - GX: a BR glider leaves the end of BR as exactly five B visits (BE^5). Later passes through a clean BR arrive there as A visits (AE). - NB: five B's on blank tape build a new throttle level 1 θ2 Q (0011)^e2 with K2 = 3. In general, B^j on blank tape builds K = j-2 (checked for j = 1..10). From then on BR1 stops growing. Each level hands the next one the same {A, B} -> E interface that M hands T.

validate_gx.py seed 2 (300 random bursts with small e): 33 runs built a second level, GX 33/33 and NB 33/33 (K2 = 3 in all 33). 256 runs kept one level and 11 ended in a dead slot (data/f3/validate_gx_seed2.txt). So the closed family has to be a tower [θ1 | BR1] [θ2 | BR2] ... (tz.parse_levels). A new level is added each time the last BR emits a glider, so the tower is unbounded.

4. B^j A^n with j up to 1e6 (bigburst.py, C). - Small e: 300 runs, K = -1..2, e = 30..60, j up to 991,164, A^2600 (data/f3/bigburst_small_e_seed11.jsonl). Results: 0 halts, every answer E. 250 runs end with one canonical level, 48 with a two-level tower (K2 = 3), and 2 with a dead slot. Both dead slots came from j = 1. - Large e: 85 runs (stopped at the time limit), e = 2000..4000, A^20000, j up to 864,393 (data/f3/bigburst_large_e_seed12.jsonl): 0 halts, all E, every run in the tower family. 76 runs keep one level, sometimes with a glider still in flight in BR1, and 9 have a second level.

5. What a level is safe against (multiburst.py, twoburst.py; data/f3/multiburst*.txt, twoburst.txt). - Safe for glider bursts: - B^5 A^n B^5 A^2600 on every canonical throttle with K <= 3, n = 0..30: 3,751/3,751 safe. - 4 bursts of B^5 with random gaps 0..8 or 0..40: 400/400 safe. - 5 bursts of B^4 with gaps 0..6: 200/200 safe. - Not safe for small bursts with short gaps: - B^1 (6 bursts, gaps 0..3): 15/200 halt, and 28 more answer C or D. - B^2 (5 bursts, gaps 0..6): 1/200 halts. - B^3 (5 bursts, gaps 0..6): 2/200 halt. One example is T(RP; 34) on B3 A4 B3 B3 A6 B3 A4 B3, which halts in the 5th burst. - An interleaved word with junk on BR (A on junk, item 6) also halts (data/f3/halt_interleaved_example.txt).

These are real halts of zone T on constructed input words. They are not halts of the machine.

6. Further non-canonical modes. - JA (A on junk): an A visit that meets a junk frontier turns it into a permanent 0110 block. After that, BR only counts up (A +1, D +6) and never sweeps again. - Dead slots: a single B (j = 1) on some throttles leaves a dead slot, as in F2 at K = 3, and it can persist. Dead slots were reached in 2/300 runs with j up to 1e6 and 11/300 with j up to 1e4. - Dead slot plus short A-runs: epochs.py runs repeated level-1 epochs B^j A^2600, with up to 8 rounds and j up to 3,000 (data/f3/epochs_seed31.jsonl). Of 60 runs, 0 halted, but 11 answered C or D on a later burst. Every failure came after a j = 1 round: 11 of the 34 runs that had a j = 1 round failed, and none of the others did. Two of them were replayed: RQP e=40 with j = 169, 5, 1, 14, 14, and QPP e=33 with j = 20, 9, 4, 1, 2, 1019. Before the failing burst both are in a dead-slot variant Q [1101] P Q with an unswept BR word. With A^100000 per round, the same j sequences stay canonical and safe (11/11 rounds). So level 1 also needs a quantitative "the A-run is long enough" lemma, plus a rule for what a single-B epoch does. j_m = 1 epochs can occur when MO starts.

7. Burst sizes the deeper levels can receive (BR arithmetic, exitsizes.py). - A glider exit is 1 + 4 units, contiguous because BR is not clean in between. - If new units reach BR while the glider is between its two carries, the rest of the exit is 4 units (2,637/3,000 cases) or 1 + 1 (363/3,000), so the next level gets B^5 or B^3. - Gaps between bursts at level k+1 are the clean passes of BR_k, and they can be anything from 0 up.

At level 1, M guarantees one burst per epoch followed by >= 2,700 A's. Below level 1 nothing guarantees a shape: B^3 bursts and short gaps each need a level-1 burst to land within a few D visits of a BR1 event. In the MO regime that is heuristically a chance of about 2^-m per epoch, from m ~ 236 on. The machine almost surely never meets the unsafe patterns, but a proof has to exclude them. That needs control of pseudo-random timing (burst times against glider exits), which is cryptid-like for a formal proof.

Verdict. F3 has no closed family; the stop rule applies. - The near-term argument (m < ~236, proof.md section 6 given F1 and F2) is unchanged. - From m ~ 236 on, the regime opens an unbounded tower of levels with K = 3 births, dead slots, JA and short-gap bursts. The zone tests show that T levels are not robust to all of these. - 0 halts of the full machine in any test. The zone T halts above come from constructed input words that the level-1 burst shape excludes and that the deeper levels could only receive through timing coincidences.

Confidence in non-halting stays med, on heuristic grounds. Confidence in a proof along this route is low.

Still open. - A tower invariant that includes dead slots, JA, K = 3 births and the input languages between levels. - A timing lemma: bursts never land in a sweep or exit window. It may be unprovable without number theory. - The safe input language of a T level. It is finite-state in the throttle head and could be computed, but that is a research stage. - Recommendation: park R8. A new decision.json asks for that priority call.

Decision (2026-10-12)

Question: Park R8, spend one research stage on the tower (the safe input language of a level plus a burst-timing lemma), or flag it as a cryptid candidate? Answer: park (Park). Dennis: apply recommendations (2026-10-12).