1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---

Status: CHECKPOINT_A Class guess (agent / Dennis): two coupled binary counters, a drifting-defect digit counter on the right and a bit counter at the left edge (sheet: Structural counter + counter) / pending Spreadsheet notes / Discord thread: Results tab has no status, notes or sources. It is struck in Direct Simulation col D, so it was simulated to 1e15. It is in neither data/discord list and no thread is linked. Trio twins: #21 1RB0LC_1LA0RE_0RD0LA_1RE1RA_0LD1RF_0RB--- and #22 1RB1RC_0LA1RF_1RD0LE_1LC0RB_0RA0LC_0RD---. Viewer: https://bbchallenge.org/1RB0LC_1LA0RE_0RD1LF_1LC1LB_0LD0RB_0LA---

Observation

• 1e9 steps (C core): no halt; 2,457 cells, 1,464 nonzeros, lo -1964, hi 492; width ~t^0.33.
• The tape is the period-5 pattern 10110. The head sweeps from the left counter to the first 0-digit, then back.
• Hub (E starts a right sweep): 0^inf 10 W σ E> 110 (10110)^g D_1 (10110)^G_1 … D_k (10110)^G_k 11 0^inf
• W: big-endian bits, 10=1 and 00=0.
• σ: 101010 in phase X, 100010 in phase Y.
• D: little-endian digits, 110=1 and 100=0. G_i is the gap after D_i, in blocks.
• About 40% of hubs are in a separator regime, with left part 10 W1 s W2 σ and s ∈ {0, 110}. It is entered after a phase-Y absorption.
• Diagrams in img/:
• hubmap.png: one row per right sweep (hub), steps 7,400,830–8,747,651 (1,056 rows, unevenly spaced), cells −412..105 at 2 px per cell. Custom colours (legend in observe.json). Digits drift left and are absorbed, and new ones appear at the right end.
• hubs_raw.png: the same rows and window in plain bbchallenge colours, to check the hub map against the real tape.
• default_site_1e4.png, blaze_1e8.png, records_1e8.png, and viewer.html with all bbchallenge views.
• sweeps_from_hub.png (rows every 16 steps from the hub at step 8,307,182) is no longer on the card: at that sampling the sweeps read as gray stripes.
• Every card diagram's start, rows, window, legend and style are in observe.json → diagrams.
• History: observe.json → history (31 hub snapshots; 5 consecutive macro steps at 8.307e6; an absorption at 8.43e6).
• Tools: Quick_Sim finds 0 prover rules (block 5, chain moves only). rulefit covers 3% (2 rules at the record hub), so it does not fit this machine. compress gives direct-local.

Candidate rules

Abbreviations: B = 10110, C = 11010, inc = R3/R4/R5 applied to the right part.

• How they were tested:
• R1–R5: an independent window simulator checks exact steps and that the head never leaves the window. That proves the rule holds in any context.
• R6–R8: concrete hubs with random parameters, in three size bands: small, medium (to 40) and large (100–400). Every residue and edge case is covered: all-ones W, all-zero W, and right overflow.
• 20 instances (R4, R6) were re-checked with tools/sim.py and matched.
• Total: 696/696.
• Open:
• Absorption in phase Y. Its first hubs land in the separator regime, for example 10 W 0 W2 101010.
• R8 when W2 is empty or all ones, i.e. how the separator is created and dissolved.
• Danger spot: F1 is the only halt. F must never read 1 on its way left. The local rules guarantee this inside the right part; it still has to be shown for the left part in every regime.
• Not a cryptid: all branching is on low bits of counters that step by +1. There is no multiplicative growth with parity tests.
• Template check: the CounterCmp_v1 TM1 shape does not carry over (0/5; 3 of the 5 halt). Only the BECv7 layout is reusable: digit lists as Inductive RD with bin_inc.
• Scripts: scripts/ (model2.py is the hub model; validate.py and validate2.py contain the rule tests).
• The hub-map data is regenerated with python3 scripts/macro.py 4e7 hubs_4e7.json, run inside scripts/.
• Hub map: python3 -B hubmap.py 7.4e6 8.75e6 ../img/hubmap.png 2; raw companion: python3 -B hubraw.py 7.4e6 8.75e6 ../img/hubs_raw.png 2 (both inside scripts/; hubraw.py needs no data file).

Checkpoint A (Dennis)

• Q1: does the hub map read as one binary counter whose digits drift left and are absorbed by the left counter?
• Q2: should I derive the separator-regime rules before proof.md?
• Q3: should #21 and #22 be proved by re-targeting this rule table?
• If Discord check A/F is wanted, the ready message is observe.json → discord_check.

Informal proof

(not started; waits for Checkpoint A)

Formalization log

(not started)

Outcome

Card data pass (2026-10-10)

• Figures on the card: Fig 1 = img/hubmap.png, Fig 2 = img/hubs_raw.png, Fig 3 = img/records_1e8.png, Fig 4 = img/blaze_1e8.png, Fig 5 = img/default_site_1e4.png. Figs 1-2 are the primary figures, shown beside the checkpoint.
• The card's mechanism is cut to 3 bullets. The full list before the cut:
• Tape is the period-5 pattern 10110; the head sweeps from the left counter to the first 0-digit and back.
• Right counter: little-endian digits 110=1 / 100=0 between background blocks; each sweep adds 1 with carry.
• A carried digit moves 5 cells left, so digit k drifts 1 block per 2^k sweeps; overflow spawns two 0-digits at the right end.
• Left counter: big-endian bits 10=1 / 00=0, +1 every 2 sweeps; on overflow it gains a bit (left edge moves 2 cells).
• When the lowest digit reaches the left counter it is absorbed (left counter halves); phase X/Y and a separator regime follow.
• Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
• "Hub map, left band: derive the separator-regime rules (extra marks inside the left counter) before writing proof.md?"
• "After this lead, prove #21 and #22 by re-targeting the same rule table instead of separately?"

Deepen pass (overnight 2026-10-10)

Confidence: med, up from med with open regimes. Every regime up to 1e10 is now covered by one exact rule table. What is still missing is an inductive invariant, which is a proof obligation. Recommendation: proof (the invariant is the main lemma), after Dennis looks.

New view: tokens. The tape is a word over four tokens: 0=00, 1=10, O=100, I=110. The parse is unique. - The background block is 10110 = 1I. A digit 110 / 100 is I / O. - The left counter is a token word w: - old phase X/Y = the last token of w (1/0); - old separator s = an O/I token inside w.

Configuration ("departure"). E has just entered the first background block after w: 0^inf w E> (10110)^g d_1 (10110)^G_1 ... d_k (10110)^G_k 11 0^inf. One sweep takes one departure to the next.

Rules. Formulas are in deepen.json → model; code is in scripts/deepen/model3.py and linc.py. - strip: while w ends in I1, drop it and add 1 to g. That I1 is the C block 11010, which the returning F (R2) turns into 10110. This is how a separator leaves w. - GEN (g ≥ 2 or d_1 = 0): w → inc_L(w) and (g,D,G) → inc(g,D,G), where inc is the old R3/R4/R5. - inc_L is "+2": skip the last token, then carry right to left. - A carry turns 1 into 0. It stops at the first 0 (which becomes 1) or O (which becomes I). - A carry that reaches an I gives x I 1^k t → inc_L(x) O 0^(k-1) t 1. - Off the left edge, the left end grows by one token. - ABS1 (g = 1, d_1 = 1, w ends in 1): w → drop_last(inc_L(inc_L(w))), right part → inc(G_1+2, D[2..], G[2..]). - ABS0 (g = 1, d_1 = 1, w = u0): - v0 0 1^k 0 (k ≥ 1) → v0 1 0^(k-1) O 1 1; - v0 0 1^k 0 0 → v0 O 0^(k+1) 1 1; - if no 0 sits left of the 1-run, a leading 1 or O replaces v0 0; - right part → inc(G_1+1, D[2..], G[2..]). - ABSO1 (g = 1, d_1 = 1, w = xO1): w → inc_L(x), and the right part becomes (1, [1]+D'[2..], G'), where (0,D',G') = inc(1,D,G). This rule only appears in random tests.

Open items from the observe pass, now closed: - Phase-Y absorption is just ABS0 or ABS1 chosen by the last token. - A separator is created by ABS0 (it appends O11) or by a carry crossing the left edge (a leading O/I). - A separator moves only as a carry rewrites it: O→I, or an I-crossing. - A separator dissolves through the I1 strip. - Configurations with two O/I tokens or a leading O/I, such as 100 10 10 10 100 … at step 86,806, were unparsed in the old hub picture. The token model covers them.

Evidence: - Lockstep check of the C departure dump against the model, from step 2,000 to 1e10: 1,096,578 sweeps with 0 mismatches (GEN 1,094,493 / ABS1 1,561 / ABS0 524). - Random instances simulated directly to the next departure: 8,540/8,540 pass (GEN 5,487 / ABS1 1,647 / ABS0 1,311 / ABSO1 95). - Sizes: words of 4–40 tokens, 2–16 digits, g up to 300, gaps up to about 600. - Results are in scripts/deepen/valreal_21..23.json. - Invariant probes on the 1e10 data: - G is non-increasing at every departure. - G_1 ≥ 1 everywhere except once, at step 2,343 (initial segment). - min g = 1. - At most 2 O/I tokens; words have at most 14 tokens. - At absorptions, ABS0 always sees an all-0/1 tail.

Still open (main lemmas for proof.md): 1. Word-shape invariant: - O/I tokens are at least 4 apart; - the last token is 0 or 1; - at an ABS0 step, no O/I sits right before the trailing 1-run. Random words outside this set break the rules, so it is essential. 2. Spacing invariant: G is non-increasing and G_1 ≥ 1 at every absorption, which keeps g ≥ 1. 3. Parity coupling: the transient tails xI0, xO1 and xI1 never meet an absorption. The informal argument is that g ≥ 2 after ABS1 and that d_1 alternates. 4. Initial segment: simulate directly from the blank tape to the first configuration in the invariant. 5. A per-rule step count, and a proof that F never reads 1.

Not a cryptid: every rule is a counter increment or a fixed rewrite.

Scripts (scripts/deepen/, run with python3 -B): - gcc -O2 -o dep dep.c && ./dep 1e10 > dep.txt dumps every departure (about 40 s, 106 MB). - lockstream.py dep.txt runs the lockstep check. - valreal.py 3000 SEED runs the random validation. - nextdep.py is the direct simulator to the next departure. - rinv.py and parity.py are the invariant probes.

Informal proof pass (overnight 2026-10-10)

Outcome: proof.md written, status.json = informal_proof / OPEN. check_proof.py SUMMARY PASS 25/25 (full mode, about 3 min).

What's new: - Unified token view. The whole tape is one token word over 0=00, 1=10, O=100, I=110: B = 1 I, C = I 1, digit 1 = I, digit 0 = O, and the right end is T = 11 0^inf. The right sweep is six token window lemmas, W1–W6: - W1 E> 1 → 1 E> (4 steps); W2 1 E> I → I 1 E> (13); - W3 E> O → <F I (7); W4 1 E> T → <F O T (19); - W5 I 1 <F → <F 1 I (9); W6 I <F → <F O (3). The E pass rotates the token segment by one, and the F return re-pairs it. R1–R5 follow from W1–W6, with the step formulas checked. - Left turnaround L = inc_L. It is exact on all 13,183 domain words of length ≤ 9 (domain: first token not 0, last token 0/1, markers ≥ 3 apart). - Marker-free words take 8k+13 steps, with k the number of trailing 1s of u. - The I-crossing re-launches F (C1) on the prefix. - L reads into the right part only on an I-crossing with t = 0, and then only its first token 1. - Right-part invariant, proved. With H_i = G_i − d_(i+1): - inc never lowers H_i (H_i counts clears of digit i+1), and never lowers H_i − H_(i+1); - G_k = 0, g ≥ 1, and H_i ≥ 1 for i ≤ k−3 all hold; - the absorption interval is Δ = 2(h_1+c) − 1 + d_2; - the two sweeps after an ABS1 are GEN, which settles the old "parity coupling" item for the transient tails xI0 / xO1 / xI1. - Word shape INV-W (first token not 0, last token 0/1, markers ≥ 4 apart) is kept by GEN, ABS1, ABSO1 and strip, because inc_L never moves a marker. - Initial segment: c0 -->(2,033) Dep(10O011; 2; 11; 1,0), checked cell by cell.

Still open: - O1: h_1 ≥ 1 at every absorption. This gives k ≥ 2; ABS0 with D=[1], G=[0] leaves the model. - Proved: h_1 ≥ 2 implies next h_1 ≥ 1, using next h_1 = h_2 + ⌊(h_1+c−1+d_2+d_3)/2⌋. - Missing: an inductive lower bound. Every chain h_i ≥ a_i tried loses 1 at the top level. - O2: ABS0 must meet a clean tail: abs0 defined, and the new marker ≥ 4 from older markers. - Proved for case-(i) markers, and whenever the marker's crossing period 2^(p−1) is shorter than the time left to the absorption. - Open for far case-(ii) markers and leading markers. - Rocq decomposition owed for L (start/carry/stop/return/crossing window lemmas) and for the ABS tails, which are only checked by simulation so far.

Evidence for O1/O2 (scripts/proof/probe1e10.py on the 1e10 dump): O1 holds at 2,085/2,085 absorptions and O2 at 524/524 ABS0. INV-R, H5 and INV-W hold at all 1,096,579 departures.

Not a cryptid: the open lemmas are timing coincidences between two counters that both step once per sweep.

Scripts: scripts/proof/tmsim.py, turn.py (turnaround exploration), probe1e10.py.

Review pass (2026-10-10, skeptic gaps -> proof.md revision)

Outcome: STUCK, cryptid flag raised. proof.md revised for all 10 skeptic gaps, with a review log in §9. check_proof.py full mode reports SUMMARY PASS 36/36, up from 25/25 (11 checks added). status.json is STUCK with cryptid_flag: true.

Closed this pass: - O1 replaced by P_k: k >= 2, or (k = 1, D = [1], and (g >= 2 or last token 1)). Proved by case analysis. The exhaustive one-step check has 0 failures: 2,358,665 transitions at spacing 4 and 3,047,785 at spacing 3. - L's precondition: any right context whose first two cells are 1,0. - Checked with three contexts and the empty word. - Sharp: with I to the right, 1,735 of 1,735 t=0 I-crossing words go wrong. - Edge cases added: ABS1 on w = 1 gives 10; GEN on '' gives 10. - The ABS0 left-edge cases are now written out. - Spacing lowered to >= 3. All rules are exact at spacing 3. - H4 needs +2s for strips: Delta = 2(h_1+c) - 1 + d_2 + 2s, matching all 438 trajectory intervals. - The false claim "next h_1" was removed. - Corrected trajectory number: h_1 = 161 at step 300,628,504.

Still open: - Fatal: Safe (old O2) is now a decidable predicate on one configuration, but it is not inductive. - A leading O is born when ABS0 meets u = 2^m - 2. - The next t=0 absorption sees a segment of about 1.5Delta against a maximum of 2^m - 1. - The unsafe segment values are near the maximum (abs0 undefined) and at the 1/4, 1/2 and 3/4 points (spacing). - u/Delta at ABS0 fills the band [1.6066, 2.0006]. - At step 86,265 the trajectory came within 2 sweeps of a configuration that halts. Dep(O111100; 1; 111100; 9,4,2,0,0,0) halts 18,861 steps later. - Abstract model to 1e10 sweeps (199,990 absorptions): 8 leading-O births and 5 ABS0 events with a marker. Margins: 2 sweeps, then 7-13% of Delta. - Major:* L and the ABS rules are still only checked. The window-lemma chains are not written.

Cryptid assessment: the halting question is a coincidence-avoidance question about a coupled counter system, with no structural margin known. Heuristically it is probviously non-halting: about one birth per doubling of Delta, each with hit probability O(1/Delta). Needs Dennis: stop or continue.

Scripts: scripts/review/ - absmodel.c: C abstract model plus margin probe. - pk_check.py. - unsafe_probe.c: runs the TM from a departure. - *.before_review.*: pre-review copies of the edited files.

Decision (2026-10-10)

Question: Stop proof work on #1 and file it as a cryptid candidate (rules written out, Rocq rule reduction later), or spend another stage searching for the missing invariant clause X? Answer: stop (Stop: mark CRYPTID_CANDIDATE; Rocq rule reduction later, low priority). Dennis: go with all recommendations (2026-10-10). Stopped by Dennis 2026-10-10: cryptid candidate; Rocq rule reduction later, low priority.