1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (pool #30)

Status: KILLED_NONHALT (2026-10-10; see ## Kill at the bottom). Not a cryptid candidate. Class guess (agent / Dennis): Bell eats counter, partial eat with residue (sibling of #10) / - Spreadsheet / Discord: results.csv row 1053, class "Bell eats counter", status/notes/sources/done-by blank; listed in classifications.csv only. Not in data/discord/*.txt. Byte-exact in data/holdouts/2026-10-07_778.txt (line 748). Forensics: eqv group size 1 (no known twin). Viewer: https://bbchallenge.org/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC

Observation

• 1e9 steps: no halt; span -274..7445 (7,720 cells), 4,642 nonzeros (sim_1e9.jsonl). 137 epochs (left records in A) by 1e9; each epoch moves the left edge by exactly 2 cells; epoch length grows faster than cubic in the epoch index.
• qsim (block 3, 20k loops): 4 single-use diff rules, nothing recursive (qsim.jsonl). compress track: record skeletons scatter; head-local ones repeat (compress_track.txt).
• Hub K(a,b,X) := 0^inf (110)^a 0 (011)^b C> X 0^inf (normalized: X never starts with 011). This is the same hub as #10 and the same marker bounce as FractalBEC (mirrored: w1 = 011, w0 = the 00 around the marker).
• Left record L(k,T) := 0^inf <A 101 (001)^k T 0^inf. Every epoch: L -> K(1,k+1,..) -> bounces -> eats -> next L.

Micro-automaton (derived by hand from the table, checked by the rules below)

Moving right (F split by predecessor): A: 0->1,B / 1->0,Fa. B: 0->1,C / 1->Fb (kept). Fa: 0->A / 1: (q-1,q):=(1,0), D at q-2. Fb: 0->A / 1->Fb (kept; this is where C1=0RE differs from #10, which goes to B). C: 0: write 1, turn, D at q-1. C: 1 then 0: (q,q+1):=(1,1), Fb at q+2. C: 1 then 1: (q-1,q,q+1):=(1,0,0), D at q-2. Moving left: D: 1->0,E / 0: halt. E: 1->0,E. E on 0 at p: p-1=1 -> (p-1,p):=(1,0), D at p-2; p-1=0 -> (p-1,p):=(1,1), Fb at p+1 (turn). So the only halts are D reading 0: (a) Fa turning when the cell two to the left is 0 (pattern F0,A1,F1 in a right pass), (b) E finding 010. The left sweep of a bounce turns at the marker and never enters (110)^a; that is why a is inert until b runs out.

Rules (all validated: scripts/val_rules.py, seeds 1 and 2, data_val_rules_{1,2}.json)

Clean counter words: tail_0..3 = '', 0001, 000010001, 000110001; D(k,s,v) = (v0 01 001000)(v1 01 001000)...(v_{k-1} 01) tail_s (LSB first) holds the value n = 2^(k+2)-4 + s*2^k + v; D(1..3) = 1, 010001, 110001; D(k,4,0) = D(k+1,0,0) as words. E(0,s,0) = tail_s, E(j,s,u) = 001000 D(j,s,u).

Clean epoch (residue 0001, e.g. epochs N=16, 32): K(1,N,D(1)) counts D(1..N+1); at a=N+1 the clean counter is eaten: odd value -> E2 (only the LSB is eaten, the rest +1 becomes the next residue 11 E(...)); even value -> E1 drops the LSB digit (value halves), gives b=2, one bounce adds 1, repeat (cascade) until odd or empty. Template (FractalBEC tm10) by contrast eats the whole counter every epoch: in the same hub notation its left records are L(k,0001) with k = 1,5,13,29,61 (k -> 2k+3), and its counter digits are 2 cells, not 3 + a 4-stage tail.

Residue epochs (not yet exact)

• Most epochs start from X0 = 11 E(j,s,u) (from E2) or from an eat at a non-clean counter (75 of 138 eats to 1e8 are not clean D words; their spacers carry extra 001 groups, e.g. 1 01 (001)^5 000 ...). E1 then gives b = (number of 001 groups), i.e. the extra groups become extra bounces.
• Digestion: the first bounces absorb one leading group every 2 bounces (b stays), then the counter passes through a short transition and continues as a clean counter (img/epoch48_counter.png).
• Forced-eat scan (scripts/scan_eats.py; scratch run to 3e7 = 52 epochs): forcing the eat after j bounces halts only for 1-2 consecutive j inside the digestion window: N=48: j=24,25; N=84: 8,9; N=94: 16,17; N=104: 11; N=162: 42,43; N=344: 54,55; N=702: 57. No unsafe j in [N/2, N+40) for any epoch; the real eat is at j ~ N. Unsafe j does not depend on a. Random multi-epoch walks with random eat times halt (2 of 450), so the safety is NOT regular: it needs "eat time > digestion time".
• Scan from the 1e9 orbit (data/scan_eats_1e9.jsonl, background run, 68 of 136 epochs at write time, N up to 1,029): the same 7 epochs have unsafe j (listed above), max unsafe j / N = 0.54 (N=48 only; every other epoch < 0.32), no bounce ever halts, no unsafe j in [N/2, N+20) after N=48.

Non-halting argument (sketch, not proved)

Every regime from the blank tape is R / B / W / E0 / E1 / E2 plus the digestion phase. Halting needs an eat at an unsafe counter state. Unsafe states occur only while the residue is digested, which takes O(len X0) bounces, and len X0 = O(log N) while the epoch has N bounces and N grows every epoch. Missing: (1) an exact rule set for the digestion and for non-clean counters (inc on words with extra 001 groups), (2) a proved bound "digestion time < N" on the reachable residues, i.e. an invariant like #10's Lemma N but with large slack (observed max unsafe j / N = 0.52 at N=48, otherwise < 0.3).

Cryptid check (ground rule 6)

Branching is on low bits of the counter (E2 vs E1 cascade c -> c/2+1), the epoch size grows additively, nothing is x3/2 or Collatz-like in the halting condition. The open condition is a size inequality with large slack, not a parity coincidence. Not a cryptid candidate.

Template check

verify/FractalBEC.v line 269, tm10 = 1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC; mirrored = 1RB0RF_1RC1RF_1LD1RB_---0LE_1LA0LE_0RA0LC, only C1 differs (1RB vs our 0RE). RInc (marker bounce) = our rule B on the block side: same. LInc (counter +1, 2-cell digits d1=[1;0]) and Ov/P0 (the whole counter is eaten and expanded fractally, f(i+1)=2f(i)+2): do not carry over (our counter has 3-cell digits + a 4-stage tail; our eat is partial, E1/E2). Verdict: partly. Closer in spirit: #10 (C1=1RA), which has the same hub, a different counter encoding (bit0 + 3-cell digits, inert/pending groups) and is STUCK on its Lemma X.

Checkpoint A (Dennis)

Questions in observe.json -> checkpoint_questions. decision.json: the call on proof work.

Files

scripts/common.py (builders, parsers, D/E words, orbit events), scripts/val_rules.py, scripts/scan_eats.py, scripts/plot_epoch.py; images in img/.

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

Question: Fund one deepen stage on #30 (exact digestion rules, abstract epoch map checked against the TM, and a proof idea for 'eat after digestion'), or park it as STUCK next to #10? Answer: deepen (One deepen stage (about 2 h)). 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, deepen)

Result: STUCK at the pre-agreed exit. The size invariant ("the eat comes after the digestion") is not proved, so the stage stops with the reduced lemma below. Not a cryptid candidate. #10's stop rule fired because its safety needs exact equations such as P = 2^B. Here the open condition is a size bound with slack that grows like sqrt(N). The worst case also has an exact closed form: it doubles every 2 digits.

Notation

• Chunks: a = 001, b = 101, z = 000.
• A block is c = d01 (001)^e: a digit d (a-block if d = 0, b-block if d = 1) followed by e extra a's.
• Grammar G (aligned words): '', a bare tail, or c (z c)* [z tail], where tail is 1, 010001 or 110001 (= Dn(1..3)) and the exponents e are arbitrary. The clean D(k,s,v) words are the case e = 1 for every block except the last, which has e = 0.
• O2 words: a 2-cell prefix P in {00, 01, 10, 11}, then a G word, or z then a G word. Every residue is O2: E2 leaves '11' a^e0 z W.

New exact rules (scripts/fs_val_rules.py, seeds 1 and 2, data/fs_val_rules_{1,2}.json)

A bounce is one hub-to-hub run. Rule B (validated at observe) makes it independent of a and b.

How digestion runs. - D1/D3 eat the residue one chunk every 2 bounces. Only 1 b is used per chunk, because the hub absorbs one 011. - At an a-block, D5 adds 1 to the rest and the eating goes on. - At the first b-block, D6 fires. - The right sweep turns 10 101 (001)^e 000 into 11 100 (011)^(e+1). This builds a sub-hub 1 (110) 0 (011)^(e+1) C> R. - The sub-hub runs a whole sub-epoch inside this one bounce. Its sub-eat then goes back through the main word and leaves a^m z Y. - After D6 the top block toggles, so Y is incremented once every 2 main bounces. Its absorptions go into a^m. These are the O2 rules again, one level down and at half speed. - The same thing repeats at every D6 below that. The counter is fractal. This nesting is why digestion takes about 2^(k/2) bounces.

Orbit to 1e11 steps

• Run: scripts/fs_orbit.c, a C logger with main-hub detection matching common.events(). 1e9 steps take 5.3 s.
• Data: data/fs_orbit_1e11_LE.txt, data/fs_orbit_1e11_eats.txt, summarized in data/fs_analyze.json.
• Size: 519 complete epochs, N up to 12,668, 1,022 eats, no halt.
• Every eat after epoch 2 is at a G word. The 1,020 such eats split as E1g 500, E2g 515, E0 2 and bare tails 3, and all of them match the rules above.
• The only 2 non-G eats are in the N = 3 transient epoch, and they do not halt.
• Digestion cost β is the b used until the hub word is back in G and stays there.
• Worst share of the budget: the b left when digestion ends is at least 0.467·N (minimum at N = 45).
• β/N ≤ 0.127 for N ≥ 1000, and ≤ 0.051 for N ≥ 6000.
• β ≤ 6.52·sqrt(N) overall.
• First blocks reach up to 34 a's, and other blocks have exponents up to 24.
• Figure: img/fs_digest_share.png (observe.json diagram 5, not primary).

Exhaustive digestion (scripts/fs_digest.c, scripts/fs_analyze.py gen-clean; data/fs_digest_clean_k1-12.txt.gz)

• All clean residues a z D(k,s,v) for k ≤ 12 (32,760): all re-enter G and stay there for 30 more bounces.
• The maximum β for each k is attained at v = 1 (s = 2 for odd k, s = 1 for even k). It is exactly:
• 2^((k+9)/2) - 7 for odd k;
• 5*2^((k+4)/2) - 7 for even k.
• Equivalently β_max(k+2) = 2*β_max(k) + 7, and β_max(k) ≤ 22.5·2^(k/2).
• The formula matches all 12 values.
• Long first blocks: a first block a^e0 adds exactly e0 - 1 to β (24/24 cases, e0 up to 33).
• 400 random non-clean residues (inner exponents up to 24): all OK, with (β - e0)/2^(k/2) ≤ 39.5. Inner exponents cost more than the first block, because each extra a sits one nesting level deeper.
• This was cross-checked against the Python TM on 25 random residues, with 0 mismatches.

Unsafe eats (observe scan, now identified)

• Forcing the eat halts only at 11 z Dn(3) (= 11000110001) and 00 Dn(3) (= 00110001). This happens in the epochs N = 48, 84, 94, 162 and 344.
• In the epochs N = 104 and 702, the halt comes from E1g eats at a nested word a^m z (O2), which cascade into those two words.
• All of these lie inside the digestion phase.

Reduced lemma (open)

Lemma D. Take an E2 eat K(N-1, 1, b a^e0 z W) on the orbit. Then digestion from K(1, N, '11' a^(e0+d) z inc(W)) returns to G without halting after β ≤ N - 2 b-steps.

Together with GI, E1g, E2g, E0 and R (all exact and closed over G), Lemma D gives non-halting. It needs three pieces: - (D-a) A closed rule for D6, and for inc on nested words a^m z P V'. The sub-epoch inside one bounce and its eat through the outer word are the missing piece. The D6 outcome census does not close at depth 1 (53/1200 deeper nests). - (D-b) β ≤ 22.5·2^(k/2) + (e0 - 1) + (inner-exponent term), by induction on nesting depth. The exact doubling law above suggests that such an induction exists. - (D-c) A size bound: N ≳ 2^(k+3) at E2 eats, plus exponents of size o(sqrt N). On the orbit the exponents are at most 34 while N reaches 12,668.

Still open / next

• D6 is the bottleneck. A stage could aim at an exact recursive statement of D6 (sub-hub K'(1,e+1,R), sub-bounces, sub-eat) and a proof of the doubling law.
• If that closes, Lemma D becomes a 2-epoch size induction with slack that grows like sqrt(N).
• The Coq side would need a nested (fractal) counter. The FractalBEC bounce (rule B) carries over; its eat does not.

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

Question: Fund one more stage on #30's D6 nesting step (exact recursive rule plus a proof of the doubling law for digestion), or park it as STUCK? Answer: nest (One stage on D6 / nested digestion (about 2 h)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, nest)

Result: D6 closes into an exact recursive rule, and the rule set is now closed. A rules-only model reproduces every TM epoch to 1e11 steps. Lemma D (the eat comes after the digestion) now has a concrete proof plan, and every link in it is checked on 8,000-12,000 model epochs. Confidence is high for the mechanism and the non-halting argument. proof.md still has to write out lemmas V, K, X and fix the constants. Not a cryptid candidate.

D6 exactly (scripts/nest_model.py, scripts/nest_val.py)

• D6: K(a, b+1, '10' 101 a^e [z R]) -> K(a+1, b, a^(k+1) z Y) in one bounce. Here (k, 000 Y) is the first left record of an ordinary epoch started at K(1, e+1, R). R is the rest, a G word, or '' when there is none.
• The right sweep builds the sub-hub 1 (110) 0 (011)^(e+1) C> R. Its sub-epoch is a plain epoch: G bounces (GI) and E1g eats until the first E2g, E0 or tail eat. There is no digestion inside it, because it stops at its first left record.
• At that point the sub-record <A 101 (001)^k 000 Y meets the 1 on its left (not a blank). It turns into a^(k+1) z Y, and the main bounce finishes normally (d = 0).
• Validated against the TM on 1,200/1,200 random instances (seeds 1, 2; e ≤ 10; R random G, '' or none; random a, b). The prediction comes from the model's own epoch map, which uses no TM. A first exploratory run of 300/300 compared against the TM sub-epoch, and 200/200 more with e in 10..40 (seed 3).

Nested words and inc on them

• The census's "deeper nests" are flat. Each D6 puts one block in front of the O2 word: H ::= G | O2 | c z H, where O2 ::= '11' a^x z W | '01' a^x z W | '00' W | '10' W.
• inc on H:
• HT: a-block z H -> b-block z H.
• HC: b-block(e) z H -> a-block(e+d') z H', where (H', d') = inc(H). The inner absorption goes into the block, so the hub gets d = 0.
• D1-D6 apply to the innermost O2 word.
• D5 also works with no rest: '10' a-block -> '01' a-block z 1.
• 8 constant end-of-word words T (10, 00, 11, 10 tail2, 10 tail3, 10 00 tail2, 10 01 z tail2, 10 01 a z 1), as a table. They occur when a sub-epoch eats the word down to its tail.
• Tail eats:
• K(a,1,1) -> L(a, 000 01 a z 1)
• K(a,1,010001) -> L(a, 000 10 00 010001)
• plus E0 and Et3 from before.
• Validation (seeds 1 + 2, against one TM bounce each, random a ≤ 60, b ≤ 60):

• In the whole-epoch check, 13 residues were skipped because the model predicts an eat at a non-G word there. Data: data/nest_val_{1,2}.json.

The model is the TM (scripts/nest_orbit.py, data/nest_orbit_517.json)

• The model is built only from rules: R, B, GI, HT, HC, D1-D6, T, E1g, E2g, E0, Et1-Et3.
• Started at the TM's third left record L(7, 000010001), it reproduces all 517 later TM left records to 1e11 steps exactly (k and T). It never uses a TM fallback and never meets an unknown word.
• Rule uses: GI 2.95M, HT/HC 30,052 each, D6 1,128, D5 1,161, E1g 1,355, E2g 1,392, T 506.
• Fast counting add_G (n GI steps at once on a G word with ≥ 1 block; no hub absorption happens there) matches iterated GI on 1,889/1,889 random cases. The fast model orbit equals the slow one for 200 epochs (scripts/nest_ff_check.py).

Cost recursion and the doubling law (scripts/nest_cost.py)

• Write J(w) for the own-level bounces until the word is in G, and A for the hub absorptions.
• Top level: β = J - A.
• D6: J = 1 + 2 J(Y). The new block is an a-block, so the nest is incremented on every 2nd bounce and never absorbs.
• J('11' a^x z W) = 2x + 2 + J('10' W).
• A top-level a-block strip costs e + d + 4. An inner strip costs 2e + 2d + 6.
• This recursion equals the TM's β on all 32,760 clean residues (k ≤ 12, data/nest_cost_clean.json).
• Doubling law, proved from the rules (k ≥ 3, any s):
• Let Y_k = '11' a z D(k,s,1).
• D(k,s,1) = b(1) z D(k-1,s,0).
• The sub-epoch K(1,2,D(k-1,s,0)) makes one bounce, to D(k-1,s,1), and then an E2g eat. So Y = '11' a z D(k-2,s,1) (k' = 2).
• Hence J(Y_k) = 4 + 1 + 2 J(Y_{k-2}) and β(k) = 2 + 1 + 2 J(Y_{k-2}), so β(k+2) = 2 β(k) + 7.
• Checked by the recursion to k = 40 for all s (data/nest_cost_family.json; β(40) = 20,971,513).
• The family is the maximum over all clean residues for k ≤ 15: TM-exhaustive to 12, recursion-exhaustive 13-15 (data/nest_cost_exhaust.json: 2041, 2553, 4089). Clean words are no longer needed for the proof plan below.

Proof plan for Lemma D (all links checked on the model orbit)

• Positions are stable. inc, E1g bounces and overflows change digit bits and append blocks at the top, but they never move a block's exponent.
• (K) Each D6 level consumes a contiguous run of at least 2 positions of W: the trigger b-block, the sub-epoch's E1g strips and E2g digit, and that level's own D5 strips.
• The parent block's exponent is Σ(consumed e) + 2·(#consumed) − 2 + (overflow d's).
• Level ℓ only uses positions ≥ 2(ℓ−1), so 2(L−1) + S ≤ kW. Check: 12,000 epochs, maximum 2(L−1) + S − kW = 0.
• (P) When digestion ends, the word is just these L blocks plus at most one remnant: k_post − L ∈ {0, 1} in 12,000 of 12,000 epochs. The counter restarts from a value below 2^(L+4).
• (V) Write m for the counter value n+4.
• The eat value is at most 2^(L+4) + N. The eat removes at least 1 digit.
• So m_W ≤ N/2 + 2^(L+3) + X + 1, which gives 2^(kW+3) ≲ N.
• Observed: m_W/N ≤ 0.517 for N ≥ 100.
• (X) Excess flow.
• The excess of a block is η = e − 1 (or e for the last block); clean words have excess 0. Let S_t(q) be the sum of η over positions ≥ q of W at epoch t.
• Step: S_{t+1}(q) ≤ S_t(2q+2) + 3k_t + 4 and x0_{t+1} ≤ S_t(0) + 3k_t + 5. Checked: 103,679/103,679 and 8,000/8,000 (scripts/nest_excess.py, data/nest_excess.json).
• Why the step holds: block q of the next W is post-digestion block q+h (h ≥ 1 digits eaten). That block merged positions ≥ 2(q+h) ≥ 2q+2. Each level creates at most 3 per consumed digit. x0 is destroyed by the top-level D1 steps.
• Unrolled: S_t(q) ≤ ⌈log2((k+2)/(q+2))⌉·(3k+4). Excess is O(log N · log log N); observed S_0 ≤ 0.26 × this bound. The largest exponents in the long run are x0 = 95 and e = 59, up to N = 3.49e6.
• Bound.
• Bnd = x0 + 2 + Σ_q 2^((q+1)//2+1)·(2η(q)+10) + 3·2^(k//2+2) + 20·2^(k//2+1) (scripts/nest_bound.py).
• On 8,000 epochs: β ≤ Bnd holds every time (β/Bnd ≤ 0.333), and Bnd ≤ N − 2 holds for every epoch with N > 784.
• With the worst-case profile from (X) and N ≥ 0.95·2^(k+3) from (V): Bnd(k) < N − 2 for every k ≥ 13, and Bnd(k ≤ 12) ≤ 40,110. So every epoch with N ≥ 40,112 is safe whatever its k.
• The finite rest, N < 40,112, is inside the model orbit, which is the rules' own orbit. The TM log checks it directly up to N = 12,668.
• Non-halting. Every eat then happens at a G word. G eats (E1g, E2g, E0, Et) never halt, and N never decreases. The only halts in the table need D reading 0, which only happens at a non-G eat.

Long model run (scripts/nest_long.py, data/nest_long.txt, figure img/nest_beta_sqrtN.png)

• Size: 80,583 epochs, N up to 3,493,246, with no unsafe eat and no unknown word (data/nest_long_summary.json).
• β/√N ≤ 6.54 overall (maximum near N ≈ 2,000) and ≤ 4.95 for N ≥ 2e5.
• β/N ≤ 0.0093 for N ≥ 1e5 and ≤ 0.0043 for N ≥ 1e6.
• Nesting depth ≤ 9. Exponents stay small: first block ≤ 95, inner ≤ 59. kW ≤ log2 N − 2.99.

Still open (for proof.md)

• Write (K), (P), (V) and (X) as lemmas from the rule statements, with exact constants. In particular, handle the edge cases where a sub-epoch or the top-level residue reaches E0/Et1/Et2 (rare: 3 top-level epochs in 6,000).
• D6 needs a "sub-epoch in a left context" lemma. Checked (scripts/nest_ctx.py, data/nest_ctx.json): a bounce and an E1g eat never move the head left of the first cell of (110)^a (400/400 each), and an E2g eat always does (400/400). So the sub-epoch cannot see its context until its left record. The exit through the outer hub still has to be written out; it is validated, not proved.
• Rocq: the bounce (rule B) is FractalBEC's RInc. D6 needs a recursive (nested) epoch map. The finite part of the argument (N < 40,112: 1,408 epochs) would have to be run inside Rocq or tightened away. This is heavy, and it is a priority call for later.

Files (nest stage)

scripts/nest_model.py (rules-only model, FAST counting), nest_val.py (TM validation), nest_orbit.py (model vs TM log), nest_ff_check.py, nest_cost.py (cost recursion), nest_mass.py, nest_excess.py, nest_bound.py (proof-plan checks), nest_ctx.py (left-context fact), nest_long.py + nest_plot.py (long model run, figure). Data in data/nest_*.

Informal proof stage (2026-10-10)

• proof.md written; check_proof.py (machine dir) validates every claim; results in data/check_proof_seed{1,2}.json and .log.
• New structure: a bounce is LP (word-local pass, exits as <A 100 X' for d = 0 or <A 101 000 X' for d = 1) followed by RP (region pass, 8n+4 / 8n+7 steps, any left context). Every word rule of the earlier stages is an LP rule built from 10 window rules (W1-W10) and 3 shift rules (S1-S3). D1/D3 are one rule (LP11) and D2/D4/HT are one rule (LP0).
• D6 is proved: a right pass of 3e+14 steps builds the sub-hub K(1,e+1,R) behind a 1. The sub-epoch reads nothing left of its marker until its final eat reaches first-1 in state E (pre-record L'). There it meets the 1 and W10 exits in 4 steps with a^(k+1) z Y.
• Lemma D: N = 2917 (was 40,112) with tau = 13 and c = 1. Open link: D.6 (c_t <= 1 overflows per digestion; checked on every epoch, argument sketched). N for c = 2..12 ranges from 4,757 to 1,844,287, all below the nest-stage model run (N = 3.49e6).
• status.json: stage informal_proof, status OPEN.

Checkpoint B, skeptic round 1 (2026-10-10)

• Skeptic: D.6 (c_t <= 1) fatal: inside the invariant c reaches 2 (k = 2), 4 (k = 16); D.4(b) false (TM: '11' z b(8) z t1, N = 100 gives x_{t+1} = 17); checker undercounted overflows inside add_G; minor: threshold mixed epochs, D.3 sentence wrong at tails, Phi termination, special residues. All confirmed.
• Fixes (proof.md section 5 rewritten):
• Lemma C (D.0), proved from the rules: 3*2^(k+c) <= 9*2^k + sum_q 2^(q+1) eta_q - 5. Positions and front; (P1) at most one extra unit per position; (P2) at most e+1 increments per front; potential Z = 2^f V never grows on consumption. Clean words: c <= 1. Also gives Phi termination (explicit fuel).
• D.3: merged blocks itemized; B_L gets bare-tail absorptions + tau_end <= T = 5 (end chain of '10' t2 5, '10' t3 2, Et2 1+4, Et1 2, E0 2, Et3 chain 2). D.4(a): S_{t+1}(q) <= S_t(2q+2) + 3(k+c) + T - 8 - 6q when positive; D.4(b): x_{t+1} <= S_t(0) + 3(k+c) + T - 1; D.4(r) resets after special residues / L = 0.
• D.6: running max kappa; fixed point G(kappa) (least G with max_k (k + Gamma(k,kappa)) <= G); invariant (I1)-(I4) by induction. D.7: F = {0..11}, N* = 14,796, closed-form tail for kappa >= 64.
• Finite part: 591 epochs (3..593), explicit rules-only orbit; first 517 = TM log to 1e11.
• check_proof.py: overflow counter now wraps GI, add_G and Et3 (orbit: c = 1 in 35.6% of epochs, still never 2); new claims D.0, D.3 end words, D.6C/D.6G, D.4a/b/c/r/x, D.7a/b/m/f/t/n, FIN beta <= N-2; adversarial section (in-invariant + unconstrained residues, skeptic's named cases, 40 TM epochs). ALL PASS seeds 1, 2 (~57 s each); --adv 12000 seeds 11, 12 ALL PASS (largest slacks: D.4(a) -5 vs -3, D.4(b) 2 vs 4).
• status.json: CHECKPOINT_B (no open link).

Kill

• 2026-10-10: KILLED_NONHALT. Kill file 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v (1,726 lines, 2,012 sentences, sha256 93a493f5531185781ddecc40b40ad3e5cf0c325326b42aa1d2631802611d90c0) proves top-level Lemma nonhalt: ~halts tm c0.. Header: "Adapted from verify/FractalBEC.v, tm10 (its RInc, mirrored)".
• tools/check_kill.sh: PASS 3 times on the same sha256, each with ulimit -s unlimited and ulimit -v 8000000, one check at a time. The watchdog showed about 21 GB available, and nothing was killed.
• Formalizer (round 2): compile 15.0 s (native on), coqchk -norec pass 67.8 s, 0 assumptions (rocq/log.md).
• Independent audit, --json (18:20-18:21 PDT): 17/17 checks pass, compile 15.33 s, coqchk -norec pass 66.3 s (no timeout, so the VM steps were re-checked), 0 assumptions. The audit confirmed the string is line 748 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, one grep -x -F match, list sha256 as in SOURCES.md). It read the whole file (ASCII, no CRs; Requires only Individual62 and Lia/String/List/Arith; no Module/Section/Variable/Context/Axiom/Opaque/Hint/Fail/native_compute; vm_compute only for closed numeric facts and the finite orbit) and compiled it independently: Print Assumptions nonhalt = "Closed under the global context", and Compute tm matches the string and the rule-table comment. Nothing suspicious. Wording nit, left as is: the header says the threshold is "computed for kappa <= 13"; the code checks κ ≤ 11 by forallb, bases κ = 10..13 by vm_compute, then a two-step induction.
• Fresh human-readable run for the submission, 18:30:15-18:31:40 PDT (checked_at 2026-10-11T01:31:40Z): 17/17 PASS, compile 15.5 s (native on), coqchk -norec pass 67.7 s, 0 assumptions (closed), 85 s wall (submission/check_kill.txt).
• holdouts.py lookup: in all 26 snapshots (2024-06-14 to 2026-10-07; line 748 of the 778 list), and line 710 of data/holdouts/BB6_holdouts_740.txt. holdouts.py solved: absent from busycoq verify/ (no byte-exact, renamed or mirrored proof).
• How the .v relates to proof.md:
• §3-§4 (window/shift rules, RP, LP, the eats, D6 as an LP constructor whose premise is a Phi, the restart) are formalized as written, as mutually inductive LP/Phi with sound (every left context).
• Lemma D follows D.0-D.3 (front, positions, nested levels, merged blocks) but replaces the excess-profile bookkeeping of D.4-D.7 (Lemma C's Γ, the fixed point G(κ), U(κ,q), N* = 14,796, 591 finite epochs) by potentials:
  • the Q potential 2^f (value + 2 qsum + pending) <= Q0 + 3*2^(f+len), so created positions stay below Pf κ = max(12, κ+3);
  • a weighted potential Pot with prepaid future positions for the cost (Dig_cost, weights 2^⌊(q+1)/2⌋, the same as D.7's) and for the merged masses (Dig_mass);
  • the invariant Inv κ N Y: N ≥ 17,705, N ≥ Nlo κ, k(W) ≤ κ, Mw ≤ Af κ, M2 ≤ Bf κ, x ≤ Xf κ.
• The finite part is 691 model epochs by vm_compute, from K(1,8,t2) (epoch 3) to K(1,17713,Y694) (epoch 694), with Inv 10 17713 Y694. Counting-phase termination uses the simpler Ψ potential (gcount).
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md: a public write-up built by rocq/submission_src/build.py (python3 -B rocq/submission_src/build.py proof.md rocq/submission_src submission/proof.md; header + working §0-§7 with 17 one-match asserted scrubs + new §8/§9; rebuild is byte-identical). §0-§7 keep their numbering and mathematics (the .v cites 3.x and D.x). A diff against the working copy shows only process and history wording: check_proof.py mentions, "first version", "observe stage", "Checkpoint B examples", nest_cost.JA, "nest-stage", the Dn(3) example, plus one D.8 bullet that points to the .v's threshold.
  • New parts: a header (holdout lists, template tm10 and the C1 difference, status, section map) and a Summary.
  • §8 "The formal proof": 8.1 what is kept from the template, 8.2 a write-up-to-.v table, 8.3 Lemma D in the .v (the potentials, Inv, N1/N2, a κ table, the finite part).
  • §9: the numerical checks, without script names, seeds or paths.
  • It has no review log, status lines or internal names. tools/writeup_lint.py: 0 errors, 0 warnings.
  • The working proof.md (sha256 2db1bee5…139b) is untouched. It still states its own invariant (N* = 14,796), which is fine as an informal proof; the public copy explains the .v's variant.
• check_kill.txt (the 18:31:40 run, verbatim), README.md (writeup_lint: 0 errors; 1 warning, for the holdout snapshot dates).
• discord.md: a draft of 1,609 characters plus <LINK> (source text in rocq/submission_src/discord_msg.txt). Not posted.
• Before posting:
• Search Discord #bb6 for the string. Sheet row 1053 is blank, and the string is not in our Discord exports.
• No Checkpoint A or B notes from Dennis were on file when this was packaged. If he adds any, fold them into proof.md and the submission copy first.
• check_kill.txt carries absolute local paths, as every earlier package does. Scrub them before attaching it anywhere public.
• Sibling #10 1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC (same hub, C1 = 1RA; 740 line 611) stays CRYPTID_CANDIDATE. The draft does not mention it.
• PR #15 (the #3 family) is still open; this kill waits in the same queue as the other claimed kills.

Same table, other starts (added 2026-10-11)

• W4-1 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB (740 line 590) = this table started in this machine's B (sigma A->E, B->A, C->B, D->C, E->D, F->F, no mirror; canon check: canon(#30, start B) == canon(W4-1, start A)). KILLED_NONHALT 2026-10-11, its kill file is this machine's .v renamed, with its own init and finite part; its status.json names this machine as parent.

• 7 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (740 line 381) = this table started in E, mirrored. Not killed (see its own dir).

• A sibling stage that labelled this machine "W4-1b" with W4-1 as its parent (delta proof) was SKIPPED on 2026-10-11: this machine is the template and is already killed (check_kill PASS, sha256 93a493f5...0c0), so a delta proof would be circular and nothing here was changed except this section.