1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC

Status: STUCK after the funded size_invariant stage (confidence med: the mechanism is ruled exactly; non-halting reduces to one inequality, T_k + 1 <= I_k, with no inductive proof found; see "Funded stage (2026-10-10, size_invariant)") Class guess (agent / Dennis): Bell eats counter. A tm108-like bell of 110/010 blocks eats a binary counter with 3-cell digits. The eat size varies, so this is not BECv1. / – Spreadsheet notes / Discord thread: Results tab: "Bell eats counter", with no status, notes, sources or done-by. Classifications tab: Bell eats counter column. Not in the dyuan01 or UBRRBA lists (data/discord/). Not in solved_index (no byte-exact, notation or mirror match). The neighbours of mxdys templates are fair game (Dennis, 2026-10-10), so no Discord check is needed. In every holdout snapshot since 2024-06-14 (26/26). Pool: reserve R2 (reports/targeting.md §4.4). It is 2 transitions from tm108 (BECv1_6x2_solved.v:872) and 1 from #29 1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LB0RC, which another agent is observing in parallel. Viewer: https://bbchallenge.org/1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC

Observation

• Direct simulation (C core): no halt to 1e10 steps.
• The span grows like t^(1/3), mostly to the left: lo/hi = -383/69 at 1e6, -1929/263 at 1e8 and -9524/1065 at 1e10 (4,082 nonzeros).
• scripts/epochs.c (exact direct simulation plus a per-round parser) ran to 1e11. Its results are in epochs_1e11.txt and in the observe.json stats.
• qsim (Quick_Sim, block size 3, 200k loops, to step 3.4e7) proves 0 rules and does not accelerate (qsim.jsonl). compress track/snap on record alignment gives 183 skeletons per 400 snapshots. It is not the right view; the round-aligned view below is.
• Clean observation point. Take the E0→1RA turn whose next cell is the boundary b of the right part 1 (110)^e (010)^f 1 0^inf, giving 0^inf L A> 1 (110)^e (010)^f 1 0^inf. In every epoch this happens at every second round. The rounds in between turn deeper inside L; the depth is the carry. Scripts: scripts/rounds2.py (Python, prints L) and scripts/epochs.c (C, epoch summary).
• Bell = the right part. Within an epoch, e+f = N stays fixed. Every round: 1. A sweeps right, complementing 110→001 (R1), up to the 110|010 border. 2. It zigzags there and sweeps back left (R2/R3). 3. The result is e+1, f-1. The 110|010 border plays the role of BECv1's 00 marker.
• Counter = L. L gains +1 every two rounds as a binary counter.
• Pure form: L = 1 W(v) S, where W holds the binary digits (000 = 0, 001 = 1, MSB first, leading 1 = top bit) and S is a suffix such as 001 or 000 100 101.
• An overflow adds one 000 digit on the left (lo moves 3 cells left).
• INC2 is exact for these forms.
• Reset (bell eats counter). When f reaches 0, the next epoch has f' = N and the boundary moves left by 3e'-2 cells: the bell eats the low 3e'-2 cells of L. There are two cases:
• The last round of the epoch is odd (a deep turn): e' = 1 always.
• It is even (clean): e' ranges over 2..47 in the run. Sometimes the whole counter is eaten (N=17→32: all 40 cells of L, e'=15) and a fresh counter starts further left.
• After eats, L mixes 100/101 digits with 000 spacers and frozen (100)^k runs. An odd reset turns an in-progress carry into a (100)^k run, which a later even reset eats.
• The carry skips some blocks. For example, 1 000 100 000 100 101 000 101 000 101 → 1 000 101 000 100 100 000 100 000 101: block 6 (100) is passed over while block 8 (100) is set.
• So a 3-block bit reading of L is wrong. The exact carry and eat semantics on mixed words are not derived.
• Numbers from the blank tape: N = 16, 17, 32, 35, 39, 40, 41, 45, 46, 47, 68, 70, 72, 75, 76, 77, 82, 98, 106, …, 6,725 at step 6.7e10. |L| stays between about 13 and 121 cells, and N/|L| ≥ 1.4 after epoch 20, growing (about 90 at 6.7e10).
• Halting transitions to watch: D reads 1 (D is entered from C1 and F0), and E0 with two 0s ahead (E writes 1, then A/B/C/D land on it).

Figures (img/; every label field is in observe.json → diagrams): - blaze_1e8.png: --mode blaze --steps 1e8 --blaze-engine wasm --as-site. - rounds_aligned.png: custom, from scripts/round_strip.py rounds_3e7.txt 2.5e5 4.7e5 img/rounds_aligned.png 80 112 3. The rounds file comes from scripts/rounds2.py 3e7. This is the most telling figure: triangles are epochs, and the left word grows and shrinks at the resets. - reset_every40.png: --from-config @<config at step 290000> --mode every:40 --steps 24000 --scale 2. - default_site.png: --as-site.

Candidate rules

All are checked by simulation. scripts/validate_rules.py 200 writes validation.json, with random n/k/v/e/f and random contexts l, r.

Open: (a) the carry automaton on mixed words (INC2 for general L); (b) the eat automaton, i.e. predicting e' and L* from L; (c) a language for L closed under both, with a size condition.

Closure fuzz (scripts/fuzz_lang.py, scripts/fuzz_replay*.py): - The naive language "1 (x0b)^k, no 11, last cell 1" with random (e, f) halts 51/300 times, so it is too loose. Several of those starts are also invalid, for example e = 0. - Real left words from the run with random small (e, f) halt 2/300. Both halts have N < |L| (N = 11, |L| = 31 and N = 12, |L| = 57). - Real left words with N ≥ 0.3|L| + 1..20 halt 0/400 over 2 epochs each. - So the invariant needs the right L language and a bound N ≳ c|L|.

Template check

Nearest proved neighbour: tm108 1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LE_0LB0RC, verify/BECv1_6x2_solved.v:872 (solve_BECv1 tm108 (Build_BEC_cert_v1 B A E A [0] [1] [1] [] [] [1;0;1] [0;1;0] [0;0] [] [] [0;0] [1;1] [1;1;1;0;1;1;0;1] [0;1;0;0;0] 1 0 0)). It differs from ours in E1 (1LE vs ours 1LB) and F0 (0LB vs ours 0LD).

scripts/template_check.py (→ template_check.json) runs all 12 of tm108's cert hypotheses on both machines: - tm108: 12/12 (sanity check). - Ours: 9/12. - These hold: HL1, HL3, HL4, HL5, HR1, HR3, HE0, HE1, HE3. - These fail 0/25: - HL2, the binary carry 1 <E → <E 1, which needs E1=1LE. - HR2, the 00 marker step, which uses F0. - HE2, the marker birth at the right end.

Applies: partly. These carry over: - the sweep lemmas and the HE0/HE1/HE3 pieces.

These do not carry over: - the counter (3-cell digits), - the marker (a 110|010 border), - the eat size (3e'−2 cells with e' = 1..47, not the constant a = 1).

mxdys's BECv1 search would have failed for exactly these reasons.

Cryptid check (ground rule 6)

Not flagged, but this is a borderline case.

The abstract dynamics are N_{k+1} = N_k + e'_k: - e'_k = 1 when epoch k ends on an odd round. - Otherwise e'_k = g(L_k), the eat size, where L_k is the counter after N_k − e_k increments since the last eat.

That is an arithmetic feedback loop, and the e' sequence looks irregular. However, no tested halt depends on it. Halting appears only for artificial starts with N < |L|, while the real run keeps N/|L| ≥ 1.4 and growing.

Whether g, and the L language, are regular is the open question. If g turns out to need the counter's value rather than a bounded window of its digits, revisit the cryptid flag.

Checkpoint A (Dennis)

(waiting: Q3 asks whether to spend a deepen stage or park)

Informal proof

Not started. Confidence is low, so it waits for Checkpoint A.

Formalization log

–

Outcome

–

Decision (2026-10-10)

Question: Spend a deepen stage on the left-word language and the eat size e', starting with an early cryptid test, or park R2 behind its sibling #29? Answer: deepen (One deepen stage (2 h), opening with a bounded-window test for e'). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, deepen)

Scope (decision deepen): first test whether e' is regular or needs the counter's value (stop rule: flag CRYPTID_CANDIDATE if it needs the value), then the carry/eat automaton on mixed words, a closure fuzz with an N vs |L| bound, and a proof-route choice. Scripts are in scripts/deepen/.

Result of the stop-rule test: e' is regular. No cryptid flag. The eat is one left sweep of the TM's left-moving states, which form a 5-state DFA (B0→1 C, B1→0 F, C0→1 E, C1→0 D, D0→1 B, E1→1 B, F0→0 D; it stops at E0 or F1 and halts at D1). Read in 3-cell units, the DFA gives a simple rule: e' and the leftover word are a "drop the suffix, then shift the grid by one cell" function of the digits. They do not depend on the counter's numeric value.

Unit view (G0 grid)

At a clean round, 0^inf L A> 1 (110)^e (010)^f 1 0^inf with L = P u_1..u_k 1. The units u end at L[-2] and are read MSB first: - z = 000 (digit 0), o = 100 (digit 1), s = 010 (spacer), t = 001 (a pending increment). - Prefix 10 is a leading s and 1 is a leading t; the missing cells are 0^inf. - Clean-round words to 1e10 contain only z, o, s, t (434,762 words; t in 482 of them).

This is the same unit alphabet and the same eat re-reading as #29.

Sweep tables (B reads a unit's last cell first; A starts at a unit's first cell): | rule | from → to | steps | random instances | |---|---|---|---| | UB_s / UB_o / UB_t | l s <B r → l <B 101 r, o → 111, t → 100 | 3 | 400/400 on each of 4 seeds | | UB_z (turn) | l 000 <B r → l 100 A> r | 5 | 400/400 ×4 seeds | | UA_D / UA_S | A> 111 → 000 A> (3), A> 101 → 010 A> (7) | | 400/400 ×4 seeds | | UA_T (bounce) | l A> 100 r → l <B 101 r | 5 | 400/400 ×4 seeds | | (halt) | B meets 101 or 110 (D reads 1) | | follows from the table |

Validated macro rules (umodel.py)

• INC (clean → deep → clean, one counter increment):
• B carries left through s/o/t (o→D, s→S, t→T) and sets the first z (or a new leading o at 0^inf).
• A returns right (D→z, S→s). At each T it bounces: T→S, and B restarts at the unit to its left.
• So every t a carry passes becomes s and adds one more increment to the part of the word left of it.
• Validated: random words over z/o/s/t 400/400 on each of 4 seeds (e+2, f−2 checked), plus the lockstep below.
• EAT, even (last round clean):
• Let j be the last unit in {z,t} (j = −1 if there is none, and then the eat runs into 0^inf).
• e' = 2 + #units after j, f' = N.
• The dropped units hold ns old spacers. Each one bounces the A sweep, and every second bounce carries, so W* = inc^⌈ns/2⌉(shift(u_1..u_{j−1})). The first round of the new epoch is deep iff ns is odd.
• shift re-reads the cells one cell to the right: (c=0) z→z, o→s, s→t, t→z; after a t (c=1) z→o, t→o, o→110 and s→101 (halting units).
• Validated: random words 400/400 on each of 4 seeds (e', f', first-round parity and W* all checked).
• EAT, odd (last round deep): e' = 1 and W* = shift(inc(W)). Validated 400/400 on each of 4 seeds.
• Eat-size DFA on the trajectory (eatcheck.py): all 1,082 resets from blank to 1e11 match (602 even, 480 odd). All even eats end at E0, never at F1 or a halt. In 4 of them the DFA runs past lo (no z left), and the j = −1 case covers those.
• Lockstep from blank (lockstep.py, mode-0 udump to 1e10):
• 434,229 of 434,229 within-epoch clean → clean transitions equal INC.
• 532 of 532 eats match in e', first-round parity and W*.
• To 1e11 (udump 1e11 0 | lockstep.py, results/lockstep_1e11.txt): 1,967,317 of 1,967,317 increments and 1,082 of 1,082 eats (e', first-round parity and W*), from blank.
• Epoch model (epochmodel.py: INC plus EAT, with fast binary addition once the word is t-free):
• From the step-241 epoch it reproduces the (Nold, e') sequence of all 1,079 later epochs to 1e11 exactly.
• Run on its own, it reaches N = 10^6 (92,514 epochs) and N = 10^7 (808,539 epochs, far beyond direct simulation) without leaving the rule set (results/epochmodel_1e6.txt, results/epochmodel_1e7.txt).

Non-halting argument (what is and is not shown)

• Two observations hold by inspection of the rules. For a word over {z,o,s,t}, INC is total and stays in {z,o,s,t}*, so rounds cannot halt. EAT is safe when the word has no t at the eat. A t in the eaten path, a final t, or a t o/t s in the kept part each lead to D reading 1. Other t contexts, such as t z in the kept part, are not modeled: the epoch model counts any t at an eat as a failure.
• t units are created only by eats (s→t) and cleared only when a carry passes them. So non-halting reduces to a size invariant: every pending t is cleared within the next epoch.
• To 1e10 no eat word contains a t (532/532), and t's last at most 49 rounds into an epoch. In the epoch model, clearing all t's never takes more than 1/4.6 of the epoch's increments for N ≥ 100, and 1/8.3 for N ≥ 10^5. Let h be the number of digits below the highest pending t. Then h ≤ log2 N − 3 throughout (≤ log2 N − 4 for N ≥ 10^5, ≤ log2 N − 5 for N ≥ 10^6; the margin is 16× for N ≥ 10^6).
• The slowest clearings sit just below powers of two: N = 16,361 (2^14), about 65,500 (2^16), 524,283 (2^19) and 4,194,268 (2^22, 131,017 increments). These are the counter's top-digit overflows. The margin still grows there: 4.6×, then 8.3×, then 16×. So the arithmetic does reach the safety question, through N's binary expansion, but only with growing slack. The invariant proof has to handle these overflow epochs.
• The size bound is genuinely needed (nfuzz.py, 4 epochs, 300 samples per band, 2 seeds):
• Real epoch states with N replaced by a random value in [N/2, 2N]: 600/600 safe.
• N in [3|W|, 10|W|]: 13/600 fail. N in [|W|, 3|W|]: 42/600 fail. N in [1, |W|]: 87/600 fail.
• Random z/o/s words with N ≤ 4000: 71/600 fail.
• Every failure is a t still present at the eat.
• Cross-check by direct TM simulation (nfuzz_direct.py, 120 real states with N in [1, 3|W|], 3 epochs): all 3 model failures halt in the TM, and the 117 model passes do not halt within the step budget. So these failures are real halts, not artefacts of the conservative model.

Open. - The inductive proof that the pending-t height h stays below log2(N) − 2 (equivalently, that the t's clear within ~N/4 increments). It must follow from how the eat word is built: the overflow digits form a spacer-free top block, and the spacers live in the low part. It is not derived yet. - The init segment before step 241. - Step counts per macro rule, which are not derived (the rules are validated on configurations).

Proof route: not BECv1. The invariant couples the digit structure to N (BEC-style), so a plain regular CTL/RWL certificate is unlikely. The natural route is a hand-written busycoq proof in the BECv7 style (counter as a digit list, unary bell, the shift as a list map), proving the size invariant as a lemma. #29 has the same z/o/s/t alphabet and the same shift map, so a shared counter/shift lemma is plausible.

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

Question: Spend one stage proving R2's size invariant (every pending t clears before the next eat) and then write proof.md, or park R2 until #29's eat work gives a shared lemma? Answer: size_invariant (One stage (2 h): derive the size invariant, then proof.md). 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, size_invariant)

Scope (decision size_invariant): search natively on the validated epoch model for an inductive size invariant, check it to N = 1e7 and on random states, then write proof.md if it closes. Exit rule: if no inductive form is found within the stage, report STUCK and name the arithmetic it would need. Scripts and results are in scripts/sizeinv/ (results/). Coq was not used.

Outcome: STUCK at one inequality. No inductive invariant was found. The reduction is much sharper than before, though: non-halting from the step-241 epoch now follows from a single bound on the total value at each epoch start (R1 below).

Balls-and-gaps view (a restatement of the validated INC/EAT rules)

• The non-digit units s/t are balls. A ball's gap is the number of digits (z/o) to its right. A t is a pending increment of weight 2^gap. INC adds exactly 1 to (digit value + sum over t of 2^gap).
• Lemma A (by hand, from INC). A t at gap h with digit value d below it turns into s within 2^h − d INCs. Each INC either passes it, or raises the digit value below it by at least 1 (a lower t that is passed adds 2^h' through its bounce), and that value stays below 2^h.
• Lemma B (by hand, from INC/EAT): gaps never grow.
• A ball's identity is its distance from the right end: INC inserts only at the left, the eat drops a suffix (even) or nothing (odd), and the shift is unit-wise on t-free words.
• After an eat, a ball's gap is the number of z units of U* to its right. That is at most the old gap, minus 1 at an even eat.
• Checked: 20,596,783 ball-eats on the trajectory to N = 1e7 (firstt.py, results/firstt_1e7.txt), and 743,436 from random starts (reduce_rand.py, seeds 11 and 12). 0 violations.
• Lemma C (first t-epoch suffices).
• Each o unit of the eaten word U*_k becomes a ball (an s) at gap h0 = #z to its right. It stays inert during epoch k+1 and is a t from eat k+1 on.
• Its gap never grows (Lemma B) and the INC count I_k never shrinks, because Nold strictly increases.
• So it suffices that 2^h1 <= I_{k+2}, where h1 is its gap in W_{k+2}. The balls of the start word szt are checked directly.
• Lemma D (by hand): the general case. Unless V_k is a power of two and eats k and k+1 are both odd, every ball born at eat k has 2^h1 <= V_k / 2.
• The top 1-bit gives h0 <= bitlen − popcount − [even], and every other 1-bit gives h0 <= bitlen − 2.
• V*_k = T_k + I_k + [odd], where T_k is the total value at the epoch start: digit value plus the sum over t of 2^gap.
• So these births are safe whenever T_k + 1 <= I_k.
• Trajectory to 1e7: 7,454,109 births. The maximum of 2^h1/I is 0.286 (at N = 13), and 0.250 for N >= 1024 (at N = 16,359).
• Random starts: 188,785 births, and none breaks 2^h1 <= V*/2.
• Lemma E (sketch): the special case, V*_k = 2^m with both eats odd.
• Exactly one ball is born, at gap m, and T_{k+1} is the full potential of W_k's balls.
• The overflow past 2^m is Δ = (s-ball potential of W_k) − (digit value of W_k) + floor((c0_k + e_k − 1)/2). Δ >= 1 when W_k's top unit is an s.
• So h1 = Z_m(Δ + 1) <= m − 1, provided Δ + 1 < 2^m.
• I_{k+2} = 2^m − T_k + (c0_k + e_k)/2 >= 2^(m−1), by T_k + 1 <= I_k.
• Observed: 3 special eats on the trajectory to 1e7, none after N = 8,139 (N = 11, 238, 8,139). The maximum ratio is 0.33, or 0.126 at N = 8,139.
• Random: 414 special cases (379 of them with T + 1 <= I), 0 violations.
• The formulas for I_{k+2} and Δ match exactly on 300/300 random special cases (special_check.py, results/special_check_21.txt).

So everything rests on R1: T_k + 1 <= I_k at every epoch, plus Δ + 1 < 2^m in the special case. - Observed: R1 holds at all 808,539 epochs to N = 1e7 (results/firstt_1e7.txt). - T/I peaks at 0.875 for N in [16, 32), 0.41 for N >= 64, and 0.284 in the 2^13 octave. It stays <= 0.13 for N >= 2^14 to 1e7 (results/binned_1e7.txt).

Why R1 did not close

• The recurrence. T_{k+1} = a + sum over balls of 2^(Z_gap(V*_k) − [even]), where Z_g(x) counts the zeros among the low g bits of x.
• When V*_k = 2^m + δ with small δ, Z_gap = gap for every ball above bitlen(δ). The whole ball potential P then moves into T.
• P itself grows at each eat by sum over 1-bits of 2^(zeros below), which is about 2^(m − popcount δ).
• Crossings are long. V* ≈ N/2 + T moves by only about e/2 per epoch, so crossing 2^m takes many epochs. At N = 16,0xx..16,4xx that is about 100 epochs at 2^13. P and T pile up there: P/N reaches 0.41 and T/I reaches 0.28.
• The crude bounds (Z_g <= g, and sum over 1-bits <= x) only give T_{k+1} <= T_k + P_s(W_k) at odd eats, which does not close.
• Native search: size summaries alone are not inductive. Candidates: Ja = {T+1 <= I, every t clears}, Jb = Ja + {every ball 2^gap <= (N−1)/2}, Jc = Jb + {P <= N/2}, Jd = everything at 1/4.
• Uniform random states: all four hold over one epoch, apart from 1/2000 breaks of Ja and Jb (randinv.py).
• Random states tuned so that V* = 2^m + δ (δ in −2..2, 4, 8, 16) break them within 3 epochs: Ja 44/2000, Jb 601/2000, Jc 668/2000, Jd 1614/2000 (results/randinv2_2.txt).
• The real trajectory itself breaks Jb and Jc at its two post-special epochs: 2^D/N = 0.538 at N = 238 and 0.503 at N = 8,140.
• From tuned Ja states, 1,497/1,500 stay safe for 20 epochs. The other 3 hit a t at the eat in epoch 2, and all 3 have a top ball with 2^14 >= N/2 or P >= 0.9N, which is off the reachable range (results/randsafe_3.txt).
• So an invariant has to carry the structure of the crossing, not only sizes.

The arithmetic it would need: a crossing lemma. As V passes 2^m (V = 2^m + δ_k, where δ_k is driven by e_k and T_k), the sum over balls of 2^(Z_gap(2^m + δ_k)) must stay <= c·2^m with c < 1/2. The loop is self-limiting: a larger T means a larger δ, so more ones in the low bits, smaller gaps and a smaller T. Nothing here proves that. - A possible route is scale invariance. Near a crossing only δ and the low part of the word matter. For m >= m0, a finite crossing automaton over (δ mod 2^r, low word) might then be checkable natively, with the epoch model covering m < m0. This was not attempted (budget).

Still open: R1 (with the Δ + 1 < 2^m side condition), the crossing lemma behind it, the init segment before step 241, and step counts per macro rule. proof.md was not written, because the invariant did not close.

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

Question: R2's size invariant is reduced to one inequality that needs a crossing lemma near powers of two: park R2 until #29/R3's size-invariant stages report, fund an R2 crossing-lemma stage now, or park it for good? Answer: wait_shared (Park until #29 / R3 report on the same lemma). 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. Waiting (auto-applied wait_shared, 2026-10-10): R2 parks until the joint R3/R2 crossing-lemma stage and #29 report on the same size lemma.

Joint crossing stage (from R3, 2026-10-10)

Run from R3 (machines/1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RA---_0RA0LB, notes "Funded stage (2026-10-10, crossing)", scripts in its scripts/crossing/). It was native only, with no Coq. R1 is not proven for R2, so R2's status stays STUCK (parked).

What R3 got: - An exact integer epoch model: - A word is (digit value, multiset of j depths), with potential Y = v + Σ 2^depth. - The b=0 steps act on the potential U as E: U → (U+2)/2^μ − 2, B0: (U+2)/2^(r+1) − 1, and B1: U + 1. - It matches R3's token model on 100,000/100,000 epochs and runs 1e7 epochs in about 2 minutes. - Lemma S (paper, checked on 100,000 trajectory epochs and 59,887 random states): - Every eat shift lowers the top j by at least one depth. - So the bell after epoch e is safe whenever zb(Y_e) ≤ bitlen(N_e) − 1 + s_e, with the exact-power case Y_e = 2^m handled separately. - In particular it is safe whenever Y_e < 2^(bitlen(N_e)+1). - R3's remaining gap is the Big-Y lemma: - It concerns epochs with Y_e ≥ 2^(m+1). Only 3 occur in 1e7 epochs (N to 1.44e8), each right after an exact-power pair (Y = 2^m twice). - It is not proven, and the candidate C0 is not inductive on random near-crossing states. - A warning on margins: R3's safety margin first fell to its minimum, 1.000 bit, at epoch 350,274 (N = 2^22 − 4,693). The prep stage had seen 2.3 bits to 1e5 epochs. A rare deep crossing therefore first appeared at N ≈ 2^22.

What may transfer to R2 (untested here; for the next R2 stage): 1. Eat shift buys one bit. R2's Lemma B already gives gap − 1 at an even eat. An R2 version of Lemma S would need 2^h1 ≤ I only up to that bit, so R1 (T_k + 1 ≤ I_k) might be relaxed at even eats. 2. Exact-power pair = R2's special case. All of R3's L failures are Y = 2^m exactly, in pairs, the first with an eat shift and the second without. That is the analogue of R2's V = 2^m with two odd eats. In R3 the pair itself is safe by Lemma S, with a structural 1-bit margin. The open part is only the epoch after it, the analogue of R2's Δ + 1 < 2^m. 3. Test R1 past N = 1e7. R2's R1 checks end at N = 1e7 ≈ 2^23.3. An integer epoch model like R3's would reach many more crossings cheaply. The lesson from R3 is that a margin minimum can first appear late.

Not done here: - no R2 model run; - no proof of R1 or of Δ + 1 < 2^m.