Decision queue

This is the case the cryptid protocol covers: formalize the rules, flag, and stop. Non-halting comes down to whether a coupled counter system avoids a sparse target set. The left counter u must miss O(1)-wide unsafe values at about one leading-O birth per doubling of Delta. The trajectory came within 2 sweeps of a configuration that is verified to halt (step 86,265). Later margins are only 7-13% of Delta, and the band edge sits on an unsafe point, so the obvious margin route is already closed. Heuristically the machine never halts, but no structural reason is known. Another search stage has poor odds, and stopping frees the budget for machines with validated mechanisms. The rule table itself is clean (1,096,578 sweeps exact to 1e10), so it is worth keeping as the write-up.

• proof proof.md 3.3-3.4: Safe(w, 2g-1-d_1) can be decided on any single configuration, but it is not inductive. Configurations satisfying every proved clause still halt, e.g. Dep(1O100; 1; 11; 2,0) at step 940, and 85 of 323 random starts failing only this clause halted within 2e6 steps. proof.md
• near-halt Step 86,265: Dep(O111000; 1; 111100; 9,4,2,0,0,0). The same configuration two sweeps later (word O111100) halts 18,861 steps on (unsafe_probe.c). unsafe_probe.c
• data At marker-free ABS0 events, u/Delta fills [1.6066, 2.0006], and the 3/4 unsafe point is at 2.0. Margins at the five ABS0 events with a marker (to 1e10 sweeps): 2 sweeps, then 7-13% of Delta. proof.md
• Fig 1 · Hub map: one row per right sweep
  Card Fig 1: the hub map, one row per right sweep, showing both counters.
  customStart mid-run: step 7,400,830Rows one row per hub = start of each right sweepWindow cells -412..105, 1 px = 0.5 cellsColors 1 0 head (E) 1s between the head and the first two 10110 blocks one 10110 background block digit 110 (=1) digit 100 (=0) 1s of the right-end tail 11 blank

  Rows: (state E, taken 6 cells after the head turns right): 1,056 rows, steps 7,400,830 to 8,747,651, unevenly spaced (22 to 2,614 steps apart, median 1,272) · Window: each cell 2 px wide; each row 1 px tall · Colors: each row recoloured from its parsed hub: left of the head (10 W σ); lavender: normally the 110 right after the head; gray: 5 cells drawn flat

Round 2 made the halting condition exact. The machine halts only when the cluster 11.01.00 meets arrivals in the phases x,E,x,x,E. That sequence halts in 60 of 60 instances, and every other phase prefix dissolves the cluster harmlessly. Seeds of this chain keep forming: 11 by 2.45e10 steps, about 0.7 per doubling. Stages 2-5 read only the left context, and their phases match the generic rates seen anywhere on the tape (about 50%, 35%, 13% and 50%). Two candidate invariants were ruled out (a global phase gauge and gap mod 4), and the 70 cells left of each seed differ in every seed. A non-halting proof would need hidden structure that the data do not show. Under the coin model the machine halts only around 2^100 steps or later, so neither a proof nor a halting search is in reach. This is the obstacle the cryptid protocol is for. Another stage would gain little: 11 seeds are too few to test events that happen 1% of the time.

• validation The halting chain on cluster 11.01.00: x,E,x,x,E halts 60/60, and x,E,x,x,x ends in a safe 1^5 60/60. All 30 phase prefixes of length 1-4 give a single outcome each (40 instances each). deepen2_chainval.py
• sim Direct simulation to about 4e10 steps found 11 seeds (steps 1.93e6 to 2.45e10). Stage 2 was E in 4 of 10. Seed #3 is the near miss at step 12,975,111, which got through x,E,x. deepen2_chain_seeds_4e10.txt
• analysis Generic next-arrival rates (3e8 and 1e9 runs) are 49.7%, 34.7% and 12.7%, which match the seeds; nothing forces them. The coin model gives about a 1% halt chance per seed. deepen.json
• Fig 2 · Right edge pinned, defects only
  Fig 2: the dense band at the right edge that emits defects.
  customStart blankRows the start, then one per new rightmost cellWindow cells -1,599..0, 1 px = 2 cellsColors at least one defect (00 or 11) among the pixel's 2 cells clean 0101... run not yet visited

  Rows: (2,819 rows, steps 0..969,848,428; no new right cell from then to 1e9); not evenly spaced in time · Window: counted from the right edge (each row's rightmost visited cell is 0, pinned to the last column; it is absolute cell 2,818 in the last row) · Colors: head not drawn; Each slanted line = a defect drifting left, away from the edge; the dense band at the right = the chaotic edge zone

Stop rule hit: left-zone size went 50, 168, 96, 128, 212 cells over gens 2-6. Every zone tested is safe (0/80 nested); gens g and g-2 agree on 53, 91, 99 cells. A 2-cycle is plausible but unshown; other machines are closer to a kill.

• Window map from the real gen-1 window reproduces all 12 real gen-2 left-zone events (6/6 runs, 11-12 blocks). val12seq.json
• Predicted left zones, gens 3-6: raw prefix 168, 96, 128, 212 cells; gens g and g-2 agree on 53, 91, 99 cells. iter2_8_10_g7.json
• Capacity: gen-3 zone 0/80 and gen-4 zone 0/80 nested events (real gen-2 zone: 22/200 nested DA). tcap_g3_R2.json
• Fig 3 · After the reset: left quarter to 1e9
  Fig 3: digit lines cross the reset walls without bending.
  customStart blankRows one row per 6th sweep endWindow cells -40..13,559, 1 px = 8 cellsColors shift 0..7 block that is not a copy of P not visited yet

  Rows: (head at the right edge in state D): 2,177 rows, steps 527..999,316,836. Not equal time: rows ~1,000 steps apart at the top, ~950,000 at the bottom, and between rows 363 and 364 (from the top) 8.1M steps are skipped (29,646,275 -> 37,788,160: the reset) · Window: the left quarter of the tape, an exact crop of img/phase_1e9.png; all 7 walls left by the reset (cells ~190..8,750) are in it, and cells 13,560..52,247 (not shown) hold only the newest digit runs · Colors: away from digits the tape repeats the 8-cell word P = 11111010, and colour = how P is shifted in that 8-cell block (red, orange, yellow, green, cyan, blue, purple, magenta = shift 0..7); colour edge = a digit block (6 cells: colour steps back 2, e.g. green -> orange) or a wall X = 11 (2 cells: colour steps forward 2)

The tail D is chaotic. It does not repeat in 5.5e6 cycles, its k-factor counts grow about 1.6^k without saturating, and 120 cycles show 3,786 distinct per-cell crossing sequences. Every regular candidate tried so far has failed: SFT_k invariants are refuted with verified chains for every k <= 36, plain n-gram CPS does not close (whole machine n <= 26, edge system n <= 24), and CTL62 searches ran out of memory with no verdict. Nobody knows whether any regular invariant exists, and the cheapest remaining route costs days with unknown odds. The obstacle is not arithmetic, but for proof purposes it behaves like a cryptid: no structure has been found to build an invariant on. The budget does more on machines with validated mechanisms, and the conditional reduction keeps this work reusable.

• proof proof.md 6.4: SFT_k refuted for k <= 22 by sampling and for k = 24-36 by verified chains. Plain CPS does not close. Two CTL62 Nsolve_cert runs reached about 10 GB within 5 min and were killed with no verdict. proof.md
• refutation Refutation chains for k = 24, 26, 28, 30, 32, 36, each re-checked in pure Python by scripts/edge_sft/verify_refutations.py. refute_k36.txt
• data Orbit to 5.5e6 cycles: no break, no halt, no repeated D, |D| in [144, 564] with no drift, deeper cells chaotic (proof.md 6.3). proof.md
• Fig 1 · One row per bounce, from a built tape
  Card Fig 1: one row per bounce. Regular bulk and junction, all the disorder in the tail.
  bbchallenge-defaultStart constructed: 0^∞ <A (1101101101)²⁰ X0 D0 0^∞Rows left recordsWindow cells -320..725, 1 px = 0.5 cellsColors 1 0 or never visited head just moved right/left

  Start: X0 = the fixed 54-cell junction; D0 = the real 261-cell tail at step 784,041, where the real bulk is a = 59, not 20 · Rows: the start, then one row per new leftmost cell = one row per bounce (321 rows, steps 0..1,200,000; 7 rows = one probe cycle) · Window: each cell is 2x2 px; cell 0 = the cell the head reads at the start

The micro rules and the left recursion are exact: a_n = 171*3^n - 3 predicted epoch 5 before it was simulated. Halting reduces to one local pattern, and the machine has come near it only at the right edge (6 D1 events, all in E0 and E3, all reading 1). But the tail is a fossil-processing particle system whose catalogue keeps growing (363 types, with new ones in E7 and E8), and E8 rebuilt the right end without its 1^k run. Both cheap routes failed: plain CPS up to n = 20 and parity CPS up to n = 14 both give abstract HALT, and bulk saturation fails after E4. What remains is open-ended (several days) with no template, while four machines in this queue each need one well-defined lemma. Parking loses nothing, since the evidence is written up. With no halt to 4.31e13 and no near-halt ever seen in the bulk, it is not a promising halting candidate either.

• rules Epoch map P(a,c,T) -> P(3a+6, 3a+c+2, T') 34/34, including 4 swapped-in tails; burst cycle 420/420; slow-phase cycle 86/86. The closed form a_n = 171*3^n - 3 predicted epoch 5 before it was simulated. notes.md
• rules Crossing lemma checked on all 931,918 sweeps to 3.54e10. Halting lemma (the machine halts iff 1 0 0 <F 0 0 (0 0 | 1 0 0) occurs) matched 7,886/7,888 random halts after step 40; the 2 misses come from the random start. deepen.json
• data No halt to 3.3e11 by direct simulation (exactly 6 D1 near-halts, none after step 2.497e9), and none to 4.31e13 by Quick_Sim, cross-checked cell for cell. The E8 right-end rebuild was re-run at cell level with 0 D1. longrun_3.3e11.txt
• Tail particles at each epoch start, placed by distance from the right end: grey = fossil suffix unchanged since the previous start, blue = rewritten.

Within an epoch, #19 is solved in practice. One uniform digit rule explains 119,956 of 120,091 trips to 1e11 steps, the closed-form fast-forward reproduces the real run, and all 72 top events to trip 13.5e6 behave. But round 2 found where the epoch ends, at about 1.27e15 steps. There, a recoding pass rewrites the whole tape. Its time is quadratic in zone size (about 1e16 steps at the real sizes). It splits zones into pieces whose sizes and number depend on the parity of m (S = 200, 202, 204 give a different structure from 201 and 203). A new counter then grows on top of the recoded tape. A proof would need three things: a rule for how every zone is recoded, an epoch-to-epoch recursion, and an invariant that survives parity-dependent recodings of zones millions of blocks long. That is new work several stages deep, and parity splits on such large numbers are the warning sign the cryptid protocol names. No cheap compute settles it, because the next epoch lies far beyond 1e16 steps. Parking keeps the budget for machines with validated mechanisms. Revisit if R5's overflow run, or another shift-overflow machine, yields a reusable epoch-recursion argument.

• validation Uniform digit rule (types A/B, 4 states each): 119,956 of 120,091 trip transitions to 1e11 steps match token by token. The other 135 are identified start-up, left-end and top-region events. counter_trace_1e11.json
• sim The topsim closed-form fast-forward reproduces all 16 round-1 events and 3 full-size K=9 events. It finds 72 top events up to trip 13,539,937, and none halts. topsim_events_to_13539937.log
• analysis Epoch overflow at trip 13,539,937 (about 1.27e15 steps): the carry crosses the top region, the sweep makes the first left record since 1.8e8, and the return pass recodes the whole tape. pre_overflow_13539937.json
• Fig 2 · One row per round trip, 452 trips
  Fig 2: the base-4 turn-back pattern, one row per round trip.
  customStart blankRows one per round trip of the headWindow cells -68..900, 1 px = 1 cellColors 1/0 on cells this trip reached 1/0 on cells it did not reach the turn-back cell not yet visited

  Rows: (it leaves the right end, turns back, returns to within 120 cells of the right end), drawn at the return: 452 trips, steps 24,389..1,994,475 (1 row = 4 px tall); not evenly spaced in time · Window: the right part of the tape, up to cell 2,185 at the end, is cut off: every trip reaches it · Colors: red: deepest point; The red diagonal is S0 (3 trips in 4 turn there); every 4th trip goes on to S1, every 16th to S2, every 64th deeper still

The architecture is TM20's call stack, but the hand closure is spreading rather than converging. Round 2 added 10 rules (731/731 instances pass) and still found 2 parsed and 7 transit classes that first appear in epoch 7. It also found a root that drifts right, which TM20's fixed-root invariant does not cover. The blocker is not the rule list. It is an invariant grammar that keeps every call away from the halting shapes, and there is no candidate for it. Small configurations next to reachable ones often halt (640 of 1,584); medium ones never do (0 of 144). The real run makes a room-2 call in epoch 7, so a proof must show that small blocks arise only at low recursion levels and in fixed shapes. The observer warns this turns cryptid-like if that fails. mxdys's FractalType7 LLM batch did not solve this machine either. Parking costs nothing and frees budget for machines with validated mechanisms. Revisit if an abstract run-length simulator gets built for another fractal (for example, if #16's accelerated simulator generalises), or if the family sweep finds a solved FractalType7 sibling whose grammar covers transit callees.

• validation Deepen round 2: 10 new rules (Call4, Call2 odd/even, ResumeTY and 3 halting patterns), 731/731 random-context instances. Round-1 rules unchanged. deepen2_validate.txt
• analysis Census to 1e9: of 46,375 E:R moments, 45,716 parse as standard frames (40 classes) and 659 are transit forms (86 shapes). 2 parsed and 7 transit classes first appear in epoch 7 (step >= 4.58e8). deepen2_census_1e9.txt
• risk Danger scan with caller X/Y(20,16,5) and 'E> 0^2 1^n 0^2 1^m 0^g 1100 1^5': for small n, m, g, 640 of 1,584 halt, in every residue class. For medium sizes, 0 of 144 halt within 2e7 steps. deepen2_danger_small.txt
• Fig 1 · State-E entries, to 3 million steps
  Fig 1, state-E entries to 3e6 steps: the replay staircases to the left of each wide white band.
  bbchallenge-defaultStart blankRows every entry into state E moving rightWindow cells -16..4214, 1 px = 1 cellColors 1 0 or unvisited head (last move right/left)

  Rows: 1,937 rows to step 3,000,000 (1,402 at the right edge = right turnarounds, 535 inside the tape), 9 to 5,473 steps apart · Colors: (10)^b blocks are 1-px stripes that look gray when shrunk, 1^a blocks are solid white

Rules, sweep and start compile; the domain is one inequality, and V* makes the sweep affine. Missing: a proof of Lemma T and a condition K on L positions. Both are new math, and so is the Rocq port. Park unless the queue runs dry: one kill for several stages of new work.

• J4 := ends with 1 and V* <= 2N+1 fails at (257, 10000000L1): V*(x') = 642 > 519, yet theta(x') = 94 <= N' (check 9i). proof.md
• 400 random J4 starts x 25 sweeps: theta <= N at every step; V*/N falls below about 1.45 after two sweeps (check 9j). check_proof.py
• Without the new RIncs_eq, 75 of 15,593 G words have no derivation. With it all do, and Example sweep_LS01 compiles (5/5 closed). TwinSpec.v
• proof.md section 3.3.5: the open problem stated precisely

Tables identical under mirror + renaming; edges agree at all 102,240 bounces to 1e10. So #5's 2026-10-10 cryptid call applies unchanged: no known erosion bound. The owed rule reduction is best done once, in one file for both twins.

• Fig 2 · #26 beside its twin #5, mirrored
  Fig 2: #26 beside #5 mirrored, one row per bounce; red marks the only differing cell (the wall).
  customStart blankRows one row per bounceWindow cells -201..192, 1 px = 1 cellColors 1 0 cell where the two tapes differ gap between the panels

  Rows: bounces 1..200: left panel = each new left record of #26, right panel = each new right record of #5 · Window: #26 cells; right panel: #5 cell x drawn at column -x-1, i.e. mirrored and shifted 1 cell · Colors: no head drawn
• Twin map: #26 at 0^inf <E 1^n w 0^inf (step t) <-> #5 at 0^inf rev(w) 1^(n+1) B> 0^inf (step t+2k), k = 2..102,241, 102,240/102,240. lockstep_1e10.txt
• Rules: walks, bounce, T/Ca/Fo/E1/E2/P1/P2 and the halting door, 60/60 each; no-00 invariant 0 violations to 1e9. validate_rules.json
• #5 erosion research: why no deterministic bound was found

Same table under mirror + renaming; the orbits coincide from our epoch 350,328. #10's counter-family satisfies #28's full invariant, then reaches an unsafe eat. L9 is proved except one exact-carry case: #10's open Lemma X, so its call applies.

• Conjugacy: A..F -> E,A,B,F,C,D mirrored, 12/12 entries, 3,000,000 steps lock-step; merge: our epoch 350,328 = #10's cascade state at t = 350,272 conj10.json
• #10's family sigma0(B) in #28's rules: invariant holds, L9 then fails twice, and the third flush is late (an eat sees an s block), for every B = 8..18 family10.json
• Real machine at B = 8: 779/779 round starts match, the unsafe eat comes at N = 194, then the machine recovers (no halt in 2.8e6 steps) tm_family_B8.json
• Debris lemmas W1-W5 (L9 everywhere but case H): 100,000 random states, 0 violations; in case H, 1,836 of 34,699 successors exceed s = 1 l9_reduce.json

The only open part is the edge map; #13's tail = fixed 58-cell word + our Z at 1,952/1,952 visits. #13 was parked on exactly this edge, and 5e6 more visits here show nothing new (no repeat, no halt). Everything else is exact: wall, sweeps, junction bounces 360/360, edge visit n-free 2,077/2,077.

• Fig 3 · Bulk, junction and edge, every 28 bounces
  Fig 3: bulk and junction columns stay fixed; all disorder is in the edge band
  customStart blankRows every 28 bouncesWindow cells -60..539, 1 px = 1 cellColors 1 0 right of the visited span

  Rows: (every 4th edge visit), bounces 315..14,819 of the 1e9-step run, 519 rows, each taken at a left record · Window: cells counted from the junction frame, which moves 12 cells right per row (3 per edge visit)
• #13's tail at bounce c-6 = fixed 58-cell word + #35's Z at bounce c, 1,952/1,952 edge visits notes.md
• Edge map iterated 5e6 visits (~5e15 machine steps): |Z| 143-563, no exact repeat, no halt phi2_5e6.txt
• #13 card (parked, same edge)

Not easier than #13: same junction, same tail cycle for cycle, same probe map on every tested input. You parked #13 on this lemma; this machine gives no new idea for (E'). New value: any future (E') proof now pays 4 kills (noted here and in STATUS.md).

• Fig 2 · Our tail vs #13's tail, per cycle
  Fig 2: our tail D_n | #13's tail | XOR, one row per cycle (XOR all black)
  customStart mid-run: step 679,041Rows one row per 7-bounce cycle n = 0..399Window cells 0..423, 1 px = 1 cellColors 1 0 past the end of D same cell cells differ

  Start: row 0 = cycle start C_0(58, D_0) of the run from blank; #13's row 0 is its C_0(59, D_0) at step 784,041 · Rows: taken at each cycle start (this machine: steps 679,041..47,105,452) · Window: of D in each of 3 panels (cell 0 = first cell right of the 54-cell junction X0); panels: this machine | #13 | XOR · Colors: blue-grey bar = panel separator; XOR panel
• Probe map equal to #13's: 120/120 orbit D; 200 random D give 97 the same and 103 break in both; 0 disagree validate.json
• #35 is this table renamed (A..F -> D,C,E,A,F,B) and follows the same D_n; #34 follows the mirror of D_n notes.md
• Edge map clean to 1.5e7 cycles (about 4.9e16 real steps); its first 5.5e6 cycles match #13's log line for line edgemap_5.5e6_to_1.5e7.txt

No halt to phase 1,857; 4/4 excursions benign; the 3-run in question was absorbed by a merge. Fast-forward is exact on the past excursion and predicts the next 3 excursions benign. A proof needs a wave grammar on unbounded run words; no busycoq template is near.

• Real orbit followed to phase 1,857 (n ~ 2^1860) with the C port: excursions at phases 91, 119, 215 and 487, all benign, with 14, 77, 93 and 700 cells in the run that became the bottom. real2.log
• C port checks: 160/160 phases equal to Python; random instances 90/90 vs Python and 90/90 vs exact fastphase; fast-path rules 3,000/3,000 each. cmp_c_vs_py_160.log
• Fast-forward from phases 311 and 411 reproduces the real excursion at phase 487 and its cascade (45/45 phases). From phases 811, 1,011 and 1,207 it predicts phase 3,321 as benign, with a1 = 555. next_d1196_r4.txt
• Fig 5: frozen runs are vertical stripes, merge waves are diagonal bands, and short runs (orange) are absorbed by the next wave. follow_lowruns_real.png

One inequality is open: R1 holds at all 808,539 epochs to N = 1e7 (T/I <= 0.13 for N >= 2^14). Size-only invariants are not inductive, so a crossing argument is needed. #29 and R3 face the same lemma now; waiting costs nothing.

• Gaps never grow (20.6M ball-eats to N = 1e7, 743k random); births outside one special case satisfy 2^h1 <= V*/2; R1 holds at every epoch firstt_1e7.txt
• R1 margin per octave of N to 1e7: T/I <= 0.28 (2^13 octave), <= 0.13 for N >= 2^14 binned_1e7.txt
• Near-power-of-two random states break the size-only candidates Ja/Jb/Jc (44/601/668 of 2000 within 3 epochs) randinv2_2.txt
• Fig 2 · Rounds aligned at the bell boundary
  Fig 2: rounds aligned at the bell boundary; each triangle is an epoch
  customStart blankRows one row per clean round startWindow cells -80..-1, 1 px = 0.33 cellsColors 1 0 (left word L) never visited boundary cell b (a 1) one 110 block one 010 block beyond the tape

  Rows: (E0 -> A turn landing on the boundary cell b of 1 (110)^e (010)^f 1), i.e. every second round of an epoch: 198 rows, steps 250,017..469,936 · Window: (3x scale), counted from the boundary cell b; then b (red); then 112 columns in block units (1 column = one 3-cell block) · Colors: black right of

Stop rule fired: no inductive form for C or C0; C0 breaks on random near-crossing states. Narrower gap than L*: Lemma S covers every epoch with Y < 2^(m+1); the rest occurs 3 times in 1e7. Big-Y has a concrete target, but it is the same crossing arithmetic that stalled R2.

• Fig 2 · Hub rows: gap and counter, four epochs
  Hub rows: gap and counter over four epochs
  customStart mid-run: step 2,850,432Rows one row per K hubWindow cells 1..90, 1 px = 0.33 cellsColors digit 1 (010) digit 0 (000) J block (100) x/z/w block (001/011/101) past the end of G 101 blocks the 00 gap

  Rows: (one bounce), 943 hubs from step 2,850,432 to 3,848,095 · Window: (counted right of the head, 9 px per 3-cell group); left 120 px = gap position a/(a+b) · Colors: left panel; cyan bar between panels = a b=0 hub
• Integer model to 1e7 epochs (N = 1.44e8): all safe, but the minimum margin is 1.000 bit (epoch 350,274, N = 2^22 - 4,693), not 2.3. longrun_1e7.txt
• Lemma S (C(e) => next epoch safe): 100,000/100,000 trajectory epochs and 59,887/59,887 random states. lemma_s_checks.txt
• Big-Y epochs (Y >= 2^(m+1)) to 1e7: only 9, 16 and 350,275, each right after a Y = 2^m pair; C-margins 3, 3, 15. crossing_stats_1e7.txt

BR is an exact M-type word; its gliders build K = 3 levels without end (33/33). Zone T halts on B^1 or B^3 bursts with short gaps, and deeper levels can get B^3. Excluding that needs control of pseudo-random burst timing (about 2^-m per epoch).

• Fig 3 · The m=14 overflow: creep across the middle
  Fig 3: the m = 14 creep. The glider leaves the middle as five B visits; a BR glider does the same at the far end and builds a new level.
  bbchallenge-defaultStart mid-run: step 148,740,000Rows every 250 stepsWindow cells -100..699, 1 px = 1 cellColors 1 0 or unvisited head moving R/L

  Rows: steps 148,740,000..148,890,000 (601 rows) · Window: absolute positions
• B^j A^n with j up to 991,164: 0 halts in 300 runs; 48 runs built a second level with K = 3. bigburst_small_e_seed11.jsonl
• Zone T halts: T(RP; 34) on B3 A4 B3 B3 A6 B3 A4 B3 (2/200 for B^3, 15/200 for B^1). multiburst_bs.txt
• notes.md, section 'Funded stage (2026-10-10, f3_first)'

Only the bottom level is understood. The sea sweeps, the wall toggles and both inner counter laws are exact (33,140/33,140 and 5,545/5,545 turns on the orbit). Above that level there are several unknowns: a second engine/counter pair, edge structures, engine-dissolving epochs (43 between 1e9 and 2.73e9, then none in the inner region), and a regime change at about 2.7e9 that 1e10 steps may not fully show. The defect algebra has real halting routes (B> 1^n 0 1 0, or a D sweep meeting 110), so non-halting needs a global invariant on defect shapes. qsim does not accelerate it and no template applies. Edge visits keep slowing (near 8e9 the left edge is visited about once per 1.5e9 steps), so each new regime costs more simulation. One stage is unlikely to make this machine proof-ready, while other machines are one stage away from proof work. The 1e12 run costs almost nothing and is the one cheap way to learn something new.

• rules 7 exact local rules at 200/200 each (S_R, S_L, RB0, RB1, RB1r, LB0, D_R) and the halt pattern H at 400/400. The inner counter laws hold on the orbit: 33,140/33,140 (right) and 5,545/5,545 (left). notes.md
• open Not understood: the right-end engine/counter pair, the edge structures, and the engine-dissolving epochs (EP has no exact rule). The regime changed at about 2.73e9. observe.json
• Fig 3 · Where the head turns, log time to 1e9
  Card Fig 3: where the head turns, log time to 1e9 (several separate wall systems).
  customStart blankRows 800 log-spaced time bins from step 1e3Window cells -549..988, 1 px = 1 cellColors no turn right turning point (R -> L) left turning point (L -> R)

  Rows: (top) to 1e9 (bottom); a turning point is a sweep's extreme cell before the head moves 8+ cells back · Colors: dark = both; darker = more turns in the bin (log scale)
• Fig 1 · Edge records to 10 billion steps
  Card Fig 1: edge records to 10 billion steps.
  bbchallenge-defaultStart blankRows the start, then one per new leftmost or rightmost cellWindow cells -729..1291, 1 px = 1 cellColors 1 0 or never visited head at a new right/left edge

  Rows: (2,021 rows, steps 0..9,957,807,009); not evenly spaced in time

Counting is exact and safe; halts need an exact value/gap coincidence at overflow/collision events. The orbit survived every event to 2.1e7; the next event is ~4.6e15 steps out and hinges on irregular digits. Even a halt there needs a W5-5-style formal increment lemma and runner: kill odds about 0.05.

• Fig 1 · Phases to 2.2e7: count, erase, rebuild
  Phases to 2.2e7: count, erase, rebuild
  bbchallenge-defaultStart blankRows every 20,000 steps (1101 rows, to step 2.2e7)Window cells -81..89,280, 1 px = 128 cellsColors 1 0

  Colors: black: each pixel samples one of 128 cells
• Fig 3 · A collision that halts
  A synthetic collision that halts
  bbchallenge-defaultStart constructed tape (below)Rows every 8 steps; last row = halt at step 6290Window cells -90..47, 1 px = 1 cellColors 1 0

  Start: 0^∞ 1³ 0 1² 0 1⁵ 0 1³⁰ 0² 1³ 0 1² 0 1² 0 1³ 0 1² 0 1² 0 1 C> 0²⁸ 1 0^∞ · Colors: coloured pixel = head (bbchallenge colours)
• R1: each C right record = +1 on the base-4 pair counter, 10,416/10,416 random transitions. validate_increment.py
• Current counter: 23 pairs, V = 61,170,343,443,693 at step 100,000,903; ~9.2e12 increments (~4.6e15 steps) to overflow. notes.md

Seam words keep growing at every abstraction (1,028 verbatim, 270 pieces at 1e10); no template is near. Yet re-drawn run lengths never halt (0/1,200): one local invariant (no 00 <B inside) would suffice. Standard CTL/NG deciders already missed this holdout, so a 2 h search has only a fair chance.

• Segment map to 1e10, right part: grey deposits turn into dark fossil u-runs (card Fig 5)
• Distinct seam words 513 / 783 / 1,028 and elementary pieces 182 / 226 / 270 at 1e8 / 1e9 / 1e10. seams_growth.txt
• Run-length fuzz from real cycle starts: 0/1,200 halts within 5e7 steps (residues kept, free, phases free). fuzz_lengths.out
• C reads 0 33,051 times to 1e10, always at the blank left edge, never inside the tape. census_1e10.txt

No outside case to 1e100 on the four starts, but perturbed copies fail at the far end (~0.2 % per episode). Some failures halt (+ 0 +); the exact fast map reaches 1e100 in ~2 s, so a halting search is cheap.

• proof.md revision 2, section 6.4: far-end race; 24/300 perturbations of line 75 at 1e13 leave the rule set (22 at the far end, 3 at the halting + 0 +), between 1e14 and 1e85 steps. proof.md
• check_proof.py PASS (A-I): 15 rules, climb automaton, both C6 branches; fast map = plain map to 1e11; no outside case to 1e100 on all four starts. check_proof.out
• The race (check_proof.py section C): 1 + 0 | 0 | 23 | 86 | 300 | L stays inside the rules for L = 1201 but meets (o4) for L = 1200; the far region's direction decides. check_proof.out

One general return is derived, but the other two remain candidates and the edge-word family is not closed. Line 593 has a more sharply isolated safety condition.

• R1 has an informal universal derivation; exact models match 264 full configurations across both starts. study.md
• Completed studies and comparison

Two exact return families are derived, but short-factor and modulo-six endpoint languages fail closure. A new nonlocal grammar is needed before formalization.

• The complete word model matches 1,283 records; proposed endpoint languages have verified 20- and 22-cell counterexamples. study.md
• Completed studies and comparison

The 21-step local extension is known, but the enabling returns remain irregular and sampled factor diversity grows. Line 282 offers a clearer initial lead.

• One billion direct steps without halt; sampled length-12 factor count grows from 523 to 1,146. notes.md
• Six-candidate comparison and proposed scope

The irregular region grows while the compressor needs 104, 267 and 866 tokens at the sampled horizons. Line 593 gives a more compact starting point.

• No halt through 100 million direct steps; a periodic bulk alone leaves the irregular-region safety obligation open. notes.md
• Six-candidate comparison and proposed scope