1RB1RF_1RC---_1RD0RD_1LE1RC_1RA1LE_1RE0LF

Status: CHECKPOINT_A Class guess (agent / Dennis): base-4 bouncer counter, sheet "Shift-overflow structural counter" / pending Spreadsheet notes / Discord thread: Results row 620: class only, no status, notes, links or cell comments. The only Discord appearance is mxdys's UBRRBA_TODO list (2026-08-24), which Dennis ruled fair game on 2026-10-10. Not on Level 1, Category 1 or dyuan01's list. Trajectory twin: 1RB1LF_1LC1RB_1LE1LD_1LB0RD_1LF---_1LA0LA (Level 0 tab, Eqv mention). Viewer: https://bbchallenge.org/1RB1RF_1RC---_1RD0RD_1LE1RC_1RA1LE_1RE0LF

Observation

• Simulated to 2·10^10 steps (scratch C tracker, observe_scripts/cyc.c) with no halt. Right edge at 214,890; step ≈ 0.432·hi². The left edge has been at −78 since step 1.8·10^8 (left records only at 1.45e6 and 1.8e8).
• Tape: 0^inf [left end] … Z2 S1 Z1 S0 Z0 W 0^inf.
• Each zone Z_k is a single 6-cell block repeated (a rotation of 110101).
• Each separator S_k is a small debris word.
• W is a fixed 99-cell wall that just translates right.
• Head motion:
• Right pass in C/D, 1 cell/step.
• Left pass: F carries a 0^6 packet at 0.3 cells/step.
• Turn-back depth over cycles follows the base-4 ruler (cyc.c output, file not kept; to 2e6 steps it is visible in img/sweeps_turnback_2e6.png, one row per round trip, red = turn-back, made by python3 -B observe_scripts/sweepview.py img/sweeps_turnback_2e6.png 2e6 4 -68 900):
• S0 bounces 3 times, at positions x−10, x+2 and x; the 4th sweep passes to S1.
• S1 has the same pattern (offset −12 instead of −10), and so does S2.
• This was seen to at least 9 levels by 2e9.
• Zone sizes at 1.45e9: Z0 7205, Z1 1790, Z2 440, Z3 70, Z4 17 blocks, so ×~4 per level (history rows in observe.json).
• Left end: at the 1.8e8 left record the deep zones were rebuilt (Z3 went from 32 to new pieces of 6 and 13). After 2.28e8, no sweep reached below cell 104 up to 2e10.
• qsim: block size 2, 200k loops, 0 rules (no acceleration). rulefit: no validated rules (26 fitted, all killed). The tools can't see a counter whose digits are separators.

Definitions used below: - W = 0^3 1^11 0^7 (111110)^2 1^13 0 1^5 0^7 1^5 0 1^11 0^7 1^7 0^inf - P0 = 1^7 0 1^9 (01111111)^2 (110101)^3 (01)^2 1^8 0 1^7 0 1^9 0 1^7 0 (1^8 (10)^4)^2 (inert part of S0) - S0 at its turn-back (F reading the last 0): - a(n) = X 1^9 010 <F 0^4 1^13 (011111)^n 1^8 W - b(n) = X 1^9 0 1^7 (01)^3 0 <F 0^4 (111110)^n 1^13 W - c(n) = X 1^9 (01)^6 0 <F 0^4 (111110)^n 1^13 W - S1 stored forms (followed by P0): - H(m) = 1^8 (10111111)^2 (10)^6 (101110)^m - P(m) = 1^8 (10111111)^2 (10)^4 1^7 0 (101110)^m - M(m) = 1^9 0 1^7 (01)^3 1 (10)^5 (101110)^m - L(m) = 1^9 0 1^4 (11101010)^2 1^7 0 (101110)^m

Candidate rules

All are exact configuration transitions, checked by observe_scripts/harness.py: Python engine, head-relative trimmed-tape equality, first hit, with the step count fitted and then re-checked.

Total: 134/134 instances, with random n and m (small values 1–5 and large ones up to about 2770; both parities).

How the rules fit together: - Digit 0 cycles a → b → (S0 open) → c → a, with Z0 += 2 per 4 sweeps. - Digit 1 cycles H → P (open) → M → L → H, with Z1 += 2 per 4 visits. - So this is a base-4 counter whose digits sit at the left edges of the growing zones. - No parity-of-big-number branching anywhere, so this is not a cryptid.

Template check: - Named templates: SBCv6a TM1 (9 transitions away), SBCv10 TM4 (8), SOBLv2 TM3 (8; that one is a HALT proof). - Their tapes collapse to (10)^k or halt at step 1 under this machine, so their rules don't carry over. The architecture does: SBCv6a's RIncs digit list and SBCv10's signal net.

Checkpoint A (Dennis)

• Q1: In sweeps_turnback_2e6 (diagram 1), are there 3 turn-backs at S0, then 1 deeper, with every 4th deeper one going deeper still? Call it a base-4 counter?
• Q2: In blaze_1e9, are the inner curves (about 1/4 and 1/16 of the edge) the digit borders?
• Q3: Pin down the left end (new-digit creation, the 1.8e8 rebuild) before proof.md?

Informal proof

Not started (waiting for Checkpoint A).

Formalization log

Not started.

Outcome

Open.

Card data pass (2026-10-10)

The card now shows at most 3 short mechanism bullets and yes/no questions that point at figures by number (primary figures first). The text they replaced is kept here. - Figure order on the card: Fig 1 = img/counter_every50.png, Fig 2 = img/sweeps_turnback_2e6.png, Fig 3 = img/records_R_right.png, Fig 4 = img/blaze_1e9.png, Fig 5 = img/default_site.png (Figs 1-3 primary). - Mechanism, full observer version: - Tape = left end … Z2 S1 Z1 S0 Z0 W: each zone Z is one 6-cell block (110101, some rotation) repeated; W = fixed 99-cell right wall. - Right pass: C> (011111)^n -> (110101)^n C> (1 cell/step). Left pass: F carries a 0^6 packet: (111010)^n <F 0^6 (111110)^n (20 steps/block). - A left sweep stops at the first separator that is closed. Each separator has 4 states: 3 bounce the head back, the 4th lets it through to the next one. - So bounce depth follows the base-4 ruler (0,0,0,1, 0,0,0,1, 0,0,0,1, 0,0,0,2 …). Z0 gains 1 block per 2 sweeps, Z_k ≈ Z_(k-1)/4, edge ≈ sqrt(t/0.432). - Left end: new digits appear rarely. The left end reorganised at the left records (1.45e6, 1.8e8) and is NOT characterised yet. - Checkpoint questions before the rewrite (some were decisions, not questions about a figure): - Diagram 1 (one row per round trip): do the red turn-backs read as 3 at the S0 diagonal, then 1 deeper, with every 4th deeper one going deeper still? OK to call it a base-4 counter? - blaze_1e9: are the inner curves (about 1/4 and 1/16 of the edge) the digit borders, all made of the same 6-cell block? - records_R_right: the far-left lines barely change (new digits are rare). Should the next stage pin down the left end before writing proof.md?

Deepen pass (overnight 2026-10-10)

Result: the digit layer is now one rule for every level, checked on every trip of the real run. The open gap is narrower and now has a location: the top region (left end + an "embryo" word that absorbs the top carries and eats the topmost zone). Confidence stays med. Not a cryptid: there is no parity or big-number branching anywhere. The top region is reached once every 4^7 trips up to 1e11, and once every 4^8 trips after trip 236129, the fast-forward result in §3.

Scripts (all new, in scripts/; C tools are built with gcc -O2 -o X X.c): - toktrack.c: blank-start tracker that prints the rest tape as tokens at every trip (format below). - counter_trace.py: replays the digit rule trip by trip on that output and lists every trip it does not explain. - top_events.py: shows the top region before and after each unexplained trip. - digit_cycle.py, counter_check.py, runcfg.c: synthetic tests (real S0 + Z0 + wall, with a synthetic digit or digit stack and left context above it). - trips.c, tripsr.c, levels.c: turn-back trackers. tok.py, tokmark.py, zones.py, load.py, snap.py: viewers and helpers. - Results: scripts/data/*.json.

1. Rest-tape alphabet

• A rest tape is the tape when the head makes a new right record, at the end of a full right pass.
• It reads 0^inf 1^t1 0 1^t2 0 ... W, and every token t_i is odd. The only exception is the leftmost token (10 now).
• Reason: the C/D right pass flips the C-cells and needs every D-cell to be 1, so 0s sit only on C-cells.
• Below, a token sequence like 7 1 1 7 means 1^7 0 1 0 1 0 1^7 0.
• A zone block is the pair 1 3, which is 101110. Zk means (1 3)^k.

2. Digit rule, the same at every level (closes "missing phase rules", "separators differ", "carry at S2+")

The rest tape is:

LE' D_top Z_top E { debris_k X_k (1 3)^m_k } (k = K..0) W

Each digit word X_k is one of two types, A or B, and each type has 4 states:

Every trip adds 1 at X_0, the S0 digit, as follows: - State s < 3: the digit moves to s+1 and the sweep turns back inside this digit. The zone m_k gains 1 block when the digit leaves s=1, and stays the same when it leaves s=0 or s=2. - State s = 3: the digit goes to s=0 and m_k gains 1. The sweep then runs on through debris_k, which is left unchanged, and into zone k+1 and digit X_(k+1). This is the carry.

What stays fixed: - The debris words never change, and neither does the wall W. - S0 is type A. Its debris is 7 9 7 9 1 3 1 3 1 1 1 9 7 9 7 9 1 1 1 9 1 1 1 9. - S1 is type B. Its debris is 1 1 1 9 7 1 1 3 1 1 3 9 1 3 1 1 1 7 1 9 7 7 1 1 1 3 9 1 3 1 1 1 9. - Deeper digits are type A or B. Some have their own debris and some are bare: S3 at 9825, for example, is just (10)^7. - The bounce offsets −10 and −12 from the observe pass are the two types, A and B. - Earlier rules: the observe-pass rules Ra/Rc/Rb* (turn-back configurations) are this rule for S0 (type A) and S1 (type B), seen at turn-back time instead of at rest.

Time law: - The turn-back level of trip t is 1 + (number of trailing digits in state 3). This is a base-4 ruler. - Between trips 2000 and 5088 the level is exactly 1 + v4(t+31), capped at 4. - The 1.8e8 rebuild changed the phase of the levels ≥ 4.

Validation: - Real run, trip by trip (toktrack 2e10 → counter_trace.py). The prediction is compared on the whole token string, including all debris and the wall. - 53572 of 53703 trip-to-trip transitions are exactly the predicted counter step, at turn-back levels 1..7: {1: 40254, 2: 10030, 3: 2495, 4: 611, 5: 147, 6: 28, 7: 7}. - The 131 others: - the start-up phase up to about trip 480, where zones are too small for the parser; - young-digit and top-region events at trips 481..5729; - 12 top-region events after trip 5729: 6753, 7777, 8801, 9825, 10849, 11873, 12897, 13921, 14945, 23137, 39521, and 5729 itself. - To 1e11 (toktrack 1e11, 120,092 trips, no halt): 119,956 of 120,091 transitions are counter steps: {1: 90045, 2: 22478, 3: 5607, 4: 1389, 5: 341, 6: 77, 7: 19}. - The 135 others are the same start-up and top events as above, plus the top events at 55905, 72289, 88673 and 105057. - Since trip 14945 the only trips the rule does not explain are the six carries into the top region, at 23137 + k·16384 (k = 0..5). - Synthetic, single digit (digit_cycle.py, 40 runs): - Set-up: type A and type B, all 4 start states, zone 0..274, random left context ending in a 9, real S0 + Z0 + wall below. - All 87 non-carry visits matched the prediction. - Carry visits: 27 runs end OK. - The other 13 carries go into the artificial top context. There the left end starts a long excursion (up to about 9e7 steps), and the check cannot follow it: 11 runs end with S0 outside the printed window, and 2 report MISMATCH from a window that no longer contains the digit. - So these 13 runs are untested, not failures of the digit itself. A carry into a realistic debris ending (9 1 3 1 1 1 9) is OK. - Synthetic stacks (counter_check.py, 24 runs, 2–4 random digits, zones 0–12): - 14 runs are fully OK, up to and including the carry out of the stack. - 9 runs end with S0 outside the window after the stack carries into the artificial top. - 1 run HALTs, after 57 correct counter steps, when the carry left the stack into the artificial left context 9 1 1 9. So non-halting depends on what the top region looks like. - With B defined without its leading 7, a bare B digit right after a zone breaks at once: it borrows a 7 from the digit above. That is why the B words include the 7. In the real tape every B digit has ...9 debris in front of it.

3. What is still open: the top region

• No left record after 1.8e8: the left edge is −78 from trip 5089 up to 1e11 (levels 1e11, 120,092 trips, no halt).
• Since trip 9825 the left part reads:
• LE' = 10 1 1 3 1 1 1 7 1 1 3 15 1 1 1 1 1 7 7 1 1 3 1 7 9 9 7 9 1 3 1 3 1 1 1 1 1 3 9 1 3. It was unchanged from trip 5729 until trip 236129.
• D_top is a type-A digit at the end of LE'. Its history: a1 (5729), then a2 (9825), then a3 (72289).
• Z_top is D_top's zone, but it shrinks: 12 (5729), 10 (9825), 9 (39521), 7 (72289).
• E is an "embryo" word, followed by young digits whose zones are 0–5.
• E takes the carry out of the highest normal digit. That happens once every 4^7 = 16384 trips: 23137, 39521, 55905, 72289, 88673, 105057.
• In the one full cycle seen (23137..72289), E absorbed 3 carries and passed the 4th, like a 4-state digit. That pass, at 72289, moved D_top from a2 to a3 and cost Z_top 2 blocks.
• E's words over time:
• after 23137: 1 9 1 1 13
• after 39521: 1 9 1 1 1 1 1 7 9 (Z_top −1)
• after 55905: 1 9 1 1 1 7 7 9
• after 72289: 1 9 1 9 1 1 1 1 1 3 7 9 (Z_top −2)
• after 88673: 1 9 1 9 1 1 7 1 3 7 9
• after 105057: 1 15 1 1 1 1 1 1 1 1 1 3 1 3 7 9
• D_top + Z_top + E together grow by exactly 4 cells per event. This is the same +4 per visit that every separator shows.
• New digits are born inside or next to E with zones of 0–1. Examples:
• The proto-word 1 1 3 1 1 3 1 → 1 1 3 1 1 9 → 7 1 1 1 1 9 → 13 1 1 1 9 (trips 6753, 7777, 8801, 9825).
• At 23137 two young A digits, with zones 1 and 5, both carry and E's 7 1 becomes 13.
• The earlier left-end history looks similar, at smaller sizes: the left records at 1.45e6 and 1.8e8, and the LE rewrites at trips 993, 1249, 1505, 1761, 2017, 2273, 2529, 2785, 3041, 4065.
• Past 1e11, with a fast-forward (fastforward.py):
• How it works. The digit rule above is applied trip by trip in compact form. Only the trips it cannot cover (carry out of the topmost parsed digit) are run exactly in C (runcfg), from the rendered rest tape.
• Spot checks. Some ordinary trips are also run exactly and compared with the rule's prediction: deep carries and every 997th trip in the first run, every 4999th trip in the second.
• Check against real data. Started at trip 88673, it matched every real line to 105057 exactly: 16,384/16,384 trips, including the simulated top event at 105057, plus 80 spot checks. Output: scripts/data/fastforward_check_88673.json.
• From trip 120092 (1e11) on (scripts/data/fastforward_120092.json):
  • 164 spot checks agree with the rule. The one failure, at trip 789842, is the tool limit: the tape no longer fits runcfg's 4M-cell buffer.
  • No halt, and no left record.
  • Step counts below are ≈ 6.93·trip², extrapolated from the real run.
• Trips 121441, 137825, 154209: E has matured into an ordinary type-A digit. Read as debris 1 15 1 + a0 + Z2, it counts a0→a1→a2→a3 with zone 2→3 like any digit. Its old debris 1 15 1 is the new embryo.
• Trip 170593 (≈2.0e11 steps): the carry out of that digit is absorbed by the embryo, 1 15 1 → 1 21.
• Trip 236129 (≈3.9e11): the embryo passes the carry on. D_top (a3) carries into LE'. LE' is rewritten from its 8th token on (10 1 1 3 1 1 1 7 1 1 3 15 ... → 10 1 1 3 1 1 1 13 1 3 ...), and Z_top is used up completely. The deepest turn-back is cell 32 of the tape, so there is no left record, unlike 1.45e6 and 1.8e8. One trip, 4.1M steps.
• Trips 301665, 367201, ..., 760417 (≈4.0e12): every 65536 = 4^8 trips the carry out of the 8th digit enters the new top region and is absorbed there. Turn-backs are at cells 210–260, the top words change, and young digits form inside them (e.g. tokens 15, 19, 7 9 Z2 ...).
• What a proof still needs:
• (a) a closed description of the top region. That means the embryo word family; how an embryo matures into a type-A/B digit and leaves a new embryo behind; and the rewrite of LE' when D_top carries (seen at 449, 5089 and 236129, each time different).
• (b) an invariant on the debris words that rules out the halting pattern (F reads 0 with 0 0 1 to its right). A synthetic top context does halt (§2), so this has to come from the real words.
• (c) head-level lemmas for passage through debris and for type-A/B bounces. So far the rule is checked at rest-tape level, plus the observe-pass head-level rules for S0/S1.

4. Verdict for this pass

• Confidence: med, unchanged.
• Covered: the counter layer is covered, at every level, on every trip seen so far.
• Not covered: the top region, which is where new digits are created and where the halting risk sits (shown by a synthetic halt), has no rule yet.
• Recommendation: more observation, aimed only at the top region.
• No new long runs are needed: fastforward.py reaches about 4e12 equivalent steps in about 1 minute.
• Next step: dump the full top-region word after every top event, at 1.45e6, 1.8e8, 1.0e11 … 4e12, and fit the embryo life cycle. That is: embryo → absorbs carries → matures into a digit → leaves a new embryo, and LE' is rewritten when D_top carries.
• To go past trip ~790k, raise runcfg's buffer (SZ). This costs about 2 bytes per tape cell (tape plus input buffer), so 8 MB now.

Deepen pass 2

Result: the counter is not the whole story. A closed-form fast-forward reaches trip 13.5e6, about 1.27e15 steps. There the counter overflows: the carry crosses the whole top region, the sweep makes a new left record, and the return pass rewrites the whole tape. That trip is quadratic in zone size, about 1e16 steps at the real sizes. Afterwards a fresh base-4 counter starts from a new wall on top of the recoded tape. So the machine is a multi-epoch shift-overflow counter, which matches the sheet class "Shift-overflow structural counter". Confidence: low (down from med), because the recoding rule and the epoch recursion are open. Not a cryptid so far: no Collatz-like branching was seen, but the recoding depends on zone parity (§3). Recommendation: more observation, aimed at the rebuild rule. This is a large job, so Dennis may prefer to park the machine (see §6).

New scripts (in scripts/; build the C tools with gcc -O2 -o X X.c): - topsim.py: the closed-form fast-forward (§1). - trip1.c: one exact trip, any tape size. - rebuild_split.py, rebuild_scale.py, rebuild_continue.py + runtok.c: the overflow trip with capped zones, and what follows it. - trace1.c, trace_helpers.py, sweep_forms.py, sweep_excursion.py: head-level sweep windows.

Data is in scripts/data/: topsim_events_to_13539937.*, topsim_fullsize_check_2005601.json, pre_overflow_13539937.json, rebuild_split.txt, rebuild_continue_S512.txt.

1. Fast-forward without a size limit

How topsim.py works: - Between events, closed form. Take the counter digits from the topmost digit J down to S0, with value v = Σ s_k·4^k. After N trips, digit k is ⌊(v+N)/4^k⌋ mod 4. Its zone gains the number of odd c in [⌊v/4^k⌋, ⌊(v+N)/4^k⌋), since a zone grows on leaving states 1 and 3. - Events, exact. An event is a carry that leaves the topmost parsed digit, or that has to cross a debris word not yet shown to be transparent. Each event is run exactly with trip1 on a tape where the zones below the event point are capped at 3 blocks. - Checks on each event. After the trip, the lower digits must come out exactly as predicted: state 0, zone+1, debris and wall unchanged. Their real zone sizes are then restored. A debris word that the carry crossed unchanged becomes trusted. - Validation: - It reproduces all 16 round-1 events from trip 19041 to 760417; the tape after each event is identical. - Capped and full-size runs agree on the K=9 events 1481313, 1743457 and 2005601. The full-size trips are 2.6e7 to 3.5e7 steps each. - Run: ./toktrack 2000000000 > tok2e9.txt (10 s), then python3 -B topsim.py tok2e9.txt 16979 80 out.json.

2. Top events to trip 13.5e6

There are 72 events with no halt. All turn-backs land at cells 32–296, so none is a left record. Spacing is 4^K trips:

Debris words shown to be transparent: - 9 words in all. - Two are new this round: 7 9 (over type A, trip 121441) and the old embryo region 1 1 1 7 1 9 1 3 7 9 1 3 1 3 1 1 1 1 1 3 1 1 3 9 (over type A, trip 1284705). - So an embryo region does end up as frozen debris under a new top digit.

What the top region looks like just before the overflow: - 10 1 1 3 1 1 1 19 1 19 1 1 1 7 1 3 1 7 7 7 1 9 7 7 1 7 1 7 1 1 1 7 (1 3)^11 1 1 1 9 1 1 1 9 7 9 1 3 7 1 1 3 9 1 3 1 3 7 9 7 7 1 1 1 3 9 1 3 - followed by the topmost digit 7 1 1 7 Z95, which is in state a3.

3. The overflow at trip 13,539,937 (about 1.27e15 steps)

Pre-event state: scripts/data/pre_overflow_13539937.json. Every digit is in state 3 (zones 95, 411, 1651, 6605, 26433, 105737, 423110, 1692473, 6769940), so the carry runs through all of them into the top region. - Left record. The sweep turns back 7 cells left of the old left end. This is the first left record since 1.8e8. - Leftmost token. The leftmost token records each left record: 4 (from trip 13) → 10 (trip 5089, the 1.8e8 record) → 16 (now). - Whole-tape rewrite. The return pass rewrites the whole tape: every zone, every debris word and the wall. The 1.8e8 record only rewrote the top two zones; this one goes all the way down.

With every zone capped at S blocks (rebuild_split.py):

What the capped runs show: - Time. The trip takes about 260·S² steps, so it is quadratic in zone size. - Length. The tape keeps its length, plus 10 cells. - Zone sizes. Each zone is cut into pieces of roughly fixed fractions; the bottom zone m becomes about 3m/4 − 1. - Parity. The piece pattern depends on the parity of m: S = 200, 202 and 204 give one pattern, 201 and 203 another. It may also depend on m mod 4 (not tested). - New tokens. New tokens appear, including runs of an 8-cell block 1 1 3. - No halt in any capped run (about 20 sizes, 2 ≤ S ≤ 600). - Real sizes. Z0 is about 6.8e6 blocks, so the real rebuild trip extrapolates to about 1e16 steps, roughly ten times all the time before it. A direct full-size run was stopped after several CPU-minutes.

4. After the overflow, a new epoch (synthetic: zones capped at 512)

• Simulation continued for 2e10 steps, 53,650 trips (rebuild_continue_S512.txt), with no halt and no further left record.
• A new wall sits at the bottom: 1 1 1 1 1 3 9 Z2 7 9 Z2 1 1 1 1 1 3 9 Z2 1 1 1.
• A fresh base-4 A/B counter grows above it: … 1 1 1 1 1 1 Z1654 7 1 1 1 1 Z6618 7 9 7 9 1 1 1 9 7 9 1 3 1 1 1 7 1 9 1 3 7 1 1 7 Z26494 [wall], with the S0 digit in state a3.
• The recoded old tape is the new top region.
• So the cycle repeats: counter → overflow → recode → new counter. Only one overflow has been seen; its rebuild alone (about 1e16 steps) is roughly ten times all the time before it.

5. Head-level structure (toward lemmas for Coq)

Measured on two trips, 14944→14945 and 15968→15969 (sweep_excursion.py): - In the left sweep, the head never goes more than 15 cells right of its running minimum before the turn-back. - In the return pass, the head never backs up more than 13 cells.

So a trip is two sweeps that each look only a bounded distance back. The head-level rules are then finitely many local rules plus the zone loops R1/R2. They are not enumerated yet. The left-sweep signal is not a function of (state, token) alone; it carries up to about 15 cells of context (sweep_forms.py).

6. What is open, and a decision for Dennis

• (a) The rebuild rule. Needed: how the return pass recodes a zone of size m (parity, maybe m mod 4) and each digit/debris word. This must come from an accelerated, rule-level model of the recoding pass, because the real trip is about 1e16 steps.
• (b) The epoch recursion. The tape at the start of epoch n+1 as a function of epoch n, and one family that holds every epoch's counter, top events and rebuild. The round-1 embryo/LE' gap is part of this.
• (c) A non-halting invariant across epochs.
• (d) The finite head-level rule set.
• Cryptid watch. If the parity/mod-4 dependence in (a) compounds across epochs, it could become pseudo-random arithmetic. That is not shown either way.
• Priority call for Dennis. This is a multi-session project (the shift-overflow SO* proofs in busycoq are the nearest templates). Continue with (a), or park the machine?

Decision (2026-10-10)

Question: Park #19, rather than fund a stage on its overflow/rebuild rule? Answer: park (Park (STUCK at deepen2)). Dennis: go with all recommendations (2026-10-10). Parked by Dennis 2026-10-10 (decision queue: park); deepen-2 findings are the re-entry point.

Holdout list 740 (2026-10-10)

Removed from the 740 list by equivalence, not solved: upstream Eqv_WordPairs.v TM83 (commit d3c52f5) proves it equivalent to 1LB---_1RC0RC_1LD1RB_1RE1LD_0RA1RF_1RD0LF, which stays on the list. Re-entry (if ever) targets that representative.