W5-3 · 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC (740 line 134)

Observe stage, 2026-10-13. Sheet class: Bell eats counter (results.csv: class only, no status, no "Done By"; no hit in data/discord/*.txt). Not in busycoq verify/ (vendor or upstream HEAD 9cf9e88) byte-exact or up to renaming/mirror.

Checks

• Byte-exact entry of data/holdouts/BB6_holdouts_740.txt, line 134 (holdouts.py contains); on all 26 snapshots since 2024-06-14.
• No claim: results.csv row has only "Bell eats counter"; classifications.csv lists it under Bell eats counter.
• Siblings: none. Canon (renaming + mirror) from each of the 6 starts against the 740 and 778 lists: only start A is on a list. Its group in 2026-10-07_eqv_1590.txt is a singleton. Starts B..F halt within 10 steps from blank.
• Nearest proved tables (scripts/nearest.py, all 6x2 machines in data/solved_index.tsv, any renaming/mirror): distance 3: 1RB1RA_1LC0RD_1RF1LD_1LE0LE_0LB0RA_---0RC (Indv2.v) and 1RB1RA_1LC1LE_0RF1LD_1LE0LD_0LB0RA_---1RC (RWL_mod_v3.v), both decider proofs, no hand-written rules to reuse. Mechanism template: BECv5.v TM1/TM2 (our W4-2's template).

Configurations

• D(N): the binary digits of N below its leading 1, lowest first, written 1 -> 11, 0 -> 00. D(N) 11 0^inf is N with its leading 1 as the final 11. In busycoq terms this is BinInc [1;1] N on the right.
• Count configuration M(a, X, b, N) = 0^inf 10^a X 10^b 011 B> 0 D(N) 11 0^inf, X in {1, 0}: B reads the 0 just left of the counter. X is a one-cell phase defect in the 1010 word (an extra 1 or an extra 0).
• Eat configuration E(p, N) = 0^inf 10^p 011 B> 0 D(N) 11 0^inf (no defect). Note M(0, 0, p, N) is the same tape as E(p, N).
• Post-eat 0 mod 4 shape K(q, N) = 0^inf 10^q 111 011 B> 0 D(N) 11 0^inf.

Rules (exact tape equality; scripts/validate_eatpost.py, validate_eat6post.py, validate_model.py, validate_r1.py)

Every count costs one pass: the E/B sweep runs left over 10 pairs to the defect, fixes it, and A runs right over 01 pairs and 1s into the counter, which is incremented by the usual carry (D erases a run of 11 digits). At an eat, the E/B sweep finds no defect, runs into the blank left edge, and a C/F sweep (C> 01 -> 10 C>) shifts the whole word by one cell and enters the counter's low end.

Eat to eat (scripts/model.py)

With e = digits eaten and f(N) the counter after the eat: - N odd: e = 1, f = (N+1)/2. N = 0 mod 4: e = 2, f = N/4. N = 2 mod 8: e = 3, f = (N+6)/8. Then p' = p + 1 + e + [p odd] and N' = f(N) + p' + [p even]. (The defect re-enters at the right end and walks the whole word: q+1 counts for a post-eat word 10^q 1, plus one pair of growth when q is odd.) - N = 6 mod 8, N = (2m+1)2^(t+3) - 2 (t = number of trailing 1s of (N-6)/8): E(p,N) -> E(p+7+t, m+2^t+t+1); N = 16m+6: E(p,N) -> E(p+7, m+5). After EAT4 the 1^(2t+1) block turns into a second defect over the next counts; it walks left 2^t+t pairs and cancels the 00 defect, leaving no defect, i.e. an immediate second eat at small N. Precondition: p + 7 >= 2^t, the same as EAT4's. It is sharp: for t = 2..7 and p = 2^t-16..2^t+3 (m = 0, 1, 3) the model holds exactly when p + 7 >= 2^t. The 1 failure in 856 random instances (p = 50, t = 6) is below it. - Validation: random constructed E(p,N): 206 + 300 (mixed, p <= 2000, N < 2^23) + 200 (N <= 64, incl. N = 1) + 150 (6 mod 8, p near 2^t): 855/856 (the one failure violates the precondition). Blank run: scripts/mev.c dumps every count/eat configuration to 1e11 steps (work/mev_1e11.txt). All 2,091 eat-to-eat transitions, from the first eat E(0,1) at step 31 to E(7367,197) at step 99,939,266,761, equal the model (0 mismatches). Eat types in the run: odd 1,056, 0 mod 4 516, 2 mod 8 254, 6 mod 8 265.

The N = 6 mod 8 transient, step by step (traced for t = 2, 3, 4; not yet a validated rule set)

Start: T = 0^inf 10^(p+7-2^t) 0 10^(2^t-1) 1^(2t+1) 011 B> 0 D(m+1) 11 0^inf (EAT4). The 00 defect at the left stays put; everything happens to its right. 1. Block stage, t+1 counts: the 1^(2t+1) block becomes 1^(2t), then 1^(2t-2), ..., 1^2, and then a 00 defect at the right end of the word. 2. Walk stage: the new defect walks left by INC1/INC0 (the rules are local: the E/B sweep stops at the first defect it meets), 2^t - 1 more counts. 3. Cancel: two 00 defects one pair apart (... 0 0 1 0 0 ...) leave no defect, i.e. E(p+7+t, m+2^t+t+1), and the next count is an ordinary eat. Total counts 2^t + t, matching the eat-to-eat formula. For t = 0 the start is 10^(p+5) 1 10 1 (an 11 defect next to an extra 1) and the same cancel happens after 4 counts.

Non-halting argument (sketch)

• Invariant I(p,N): p >= 20 and 1 <= N <= 2p.
• N odd: N <= 2p-1, so f <= p and N' <= p + p' + 1 <= 2p' since p' >= p+2.
• 0 mod 4, 2 mod 8: f <= p/2, N' <= p/2 + p' + 1 <= 2p'.
• 6 mod 8: 2^(t+3)(2m+1) <= N+2 <= 2p+2 gives m + 2^t + t + 1 <= p/4 + log2 p + 2 <= 2p', and the precondition p + 7 >= 2^t holds with slack (2^t <= (p+1)/4).
• Exhaustive check (scripts/inv_check.py): all 4,005,582 states with 20 <= p <= 2000, N <= 2p+2 map into I with C = 2; with C = 0 (N <= 2p) 1,000,620 states for p <= 1000, 0 failures; min 6 mod 8 slack p - 2^t - t = 14 (at p = 20).
• Start: blank -> E(21, 6) at step 3,097 exactly (0^inf 10^21 011 B> 0 0011 11 0^inf, checked with tools/sim.py). I holds there (6 <= 42).
• So non-halting follows from the rules above once each is proved for all parameters (busycoq: multistep_nonhalt to E(21,6), then progress_nonhalt_cond with P = I and BigStep E -> E).
• Abstract run (scripts/abstract_run.py): 2,000,000 eats from E(0,1), p = 7,056,392 at the end; N/p < 2 throughout (max 1.9999996); min 6 mod 8 slack p - 2^t = 80 after eat 20; t up to 19.

Halting and the cryptid check (ground rule 6)

• The only halt is F0: C reads 0 then F reads 0 in a C/F sweep (C0 = 1RF). scripts/csweep.c: all 514 C/F sweeps to 1e9 steps start at the blank left edge, i.e. inside eats; counts never start one.
• Every eat case is validated exactly with no halt, and the invariant does not care which case comes next.
• The order of eat types is pseudo-random (N mod 8 is close to uniform: 1/2, 1/4, 1/8, 1/8), but nothing has to be predicted: every branch keeps I. Not cryptid-like.

Template comparison (BECv5.v TM1, 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB)

• Same architecture: a binary counter BinInc (TM1: LC0 n := BinInc <[0;1] n on the left; here BinInc [1;1] N on the right, so RBinInc_spec instead of LBinInc_spec), a budget word with a one-cell defect (TM1 R n m = [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^m), one budget pair per count (RIncs), an eat of low counter digits (ROv: LC0((2k+1)2^i-1) -> LC0 k <* [0]), BigStep and progress_nonhalt_cond with a linear invariant (TM1: a <= 1+b; here N <= 2p).
• Different: here the defect walks away from the counter and the eat happens at the far blank edge after a C/F sweep over the whole word. The eat removes 1, 2 or 3 low digits by N mod 8, and N = 6 mod 8 adds a two-defect transient. Two defect types (extra 1 / extra 0) alternate every count. TM1's LIncs' (shifted counter) has no analogue; our eat leaves a clean counter.
• Rulefit's affine fits quoted at selection (A1(a+64c+128, ...) etc.) are local linearizations of R1, whose step 2^(k-1) is exponential in the hub's 1-block; they are superseded by R1 and the eat model.

Files

• scripts/hub.c, hubparse.py: hubs (A at the right end) from blank (work/hubs_3e10.txt).
• scripts/mev.c: count/eat configurations from blank (work/mev_1e11.txt; E = eat or post-eat with no inner defect, X = irregular word, e.g. two defects); mev1.c: same from a constructed tape.
• scripts/model.py (eat-to-eat map), abstract_run.py, inv_check.py, validate_*.py, eatseq.py.
• scripts/phaseview.py, ratio_plot.py (custom figures), trace.py / raw.py / mtrace.py / ev.py / ctr*.py (exploration).

Informal proof (2026-10-13)

• proof.md: complete informal proof (Checkpoint B pending). 16 exact low-level rules; count rules INC1/INC0/INC011/OVF; eat rules EAT + Y1..Y4; walk lemmas W, W2, W0, B; macro rules M1..M5 with closed form; invariant J: 1 <= N <= 2p (the p >= 20 above is not needed); start E(2,4) at step 165.
• The N = 6 mod 8 transient is a misaligned fixed-width counter Q_k(x,y) = D_k(x) 0 C(y) (first eat), counted up, eaten once more, overflowed (OVF: the 1^(2t+1) block), then the block stage B(t) and the cancel walk W0. The "EAT4" row above is M5 phases (a)-(e); "EAT3" is Y3(0) + OVF of width 0; R1 is not needed.
• First G configuration from blank: G(1, C(0)) at step 7 (INC1 -> E(0,1) at 31).
• check_proof.py (self-contained): 100/100 PASS (seeds 1, 2 default; seed 1 --full). Logs: work/check_proof_*.log.

Skeptic round 1 (2026-10-13)

• Verdict sound, 7 minor gaps, all fixed in proof.md (review log there). New checks in check_proof.py (108 total): Q_k(x,y) for odd y is not a counter word (y = 0 is C(x)); every TM step of 177/191 direct E(p,N) runs (seeds 1/2; all 66 6-mod-8 boundary cases) and of the blank run to 3e6 (2e7 --full) is tested for E-form: the first eat configuration is always the predicted one; H form S(2,4) at step 171; N < 2p strictly after E(2,4) (max N/p 1.9999996 at E(5598694, 11197386) within 2e6 eat configurations).
• Counting convention fixed: eat configurations (stored run 2,092, fresh 174 / 337 with --full) vs eat-to-eat transitions (2,091, 173 / 336).
• proof.md now has a public part (above "Appendix (working copy only)", lints 0 errors) and the working-copy appendix + review log.

Kill

• 2026-10-13: KILLED_NONHALT. Kill file 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v (530 lines, sha256 75932a97949d61ba11f16e0b8a6d0d6adf05f2e1a63231b44f0acddf0661da1a), adapted from verify/BECv5.v Module TM1 (architecture only). Imports Individual62 + BinaryCounter_v2.
• check_kill PASS three times on the same sha256: round 1 (rocq/check_kill_round1.log), the independent auditor, and a fresh packaging run (2026-10-13T10:09:16Z: compile 3.4 s native, coqchk -norec pass 1.0 s, Print Assumptions closed, all 17 checks PASS).
• Proof shape (rocq/log.md): HF/EC form (G/E after TS); left lemmas L1/L0/L011/LEat + right lemmas as Inc r r' (RInc via RBinInc_spec, IncQ for Q_k, Inc00); walks Wk/W2/W2Q/Bk/W0k; BS1..BS5 = M1..M5; step_J (Even_or_Odd twice, lowbitS_cases) + progress_nonhalt_cond with J: 1 <= N <= 2p; init 171 steps to EC 2 4.
• Package: submission/ = the .v, public proof.md (rewritten from the working proof.md: header + summary + §1-§7 math unchanged, §8 rewritten as the .v mapping, §9 evidence; writeup_lint 0 errors 0 warnings), check_kill.txt (fresh run, verbatim, contains local absolute paths), README.md, discord.md (1,601 chars before the link; not posted, fill in ).
• Auditor's minor remark (not changed): Definition C (counter) and Definition Q (misaligned counter) reuse the names of the framework's state constructor C and state type Q inside the file; harmless (state C is never used after, theorem re-checked with absolute names). A maintainer may prefer Cn / Qk.
• Not done: Discord post and upstream PR (Dennis's call). Checkpoint B notes: none on file at packaging time.