W4-2 · 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (740 line 224)

Observe stage, 2026-10-10. Sheet class: Bell eats counter (no status, no claim, no Discord thread). Not in any proof upstream byte-exact; holdouts.py solved only finds the Eqv_v3 TM493 equivalence (its mirror).

Checks

• byte-exact entry of data/holdouts/BB6_holdouts_740.txt (line 224); also on every list since 2024-06-14.
• no claim: results.csv row 1015 has only the class; no hit in data/discord/*.txt.
• siblings by canon (all 6 starts, renaming + mirror) on the 740 list: none. 349 (1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---) does not share the table. Its Eqv_v3 TM518 twin 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is this table mirrored (L<->R) and renamed F->A, A->B, ..., E->F, started in its A = this table's F (canon match, mirror included; corrected 2026-10-11, skeptic round 1). From F, the blank run enters the same rule system (first configuration K('',0,1) at step 14) on its own orbit (work/abstract_startF_3e6.out). A start-independent invariant would therefore cover 349 through TM518.

The configuration family

K(w, n, m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf. A reads the last cell of the left word w. This is the template's w <| R n m (BECv5 TM1/TM2 use exactly this right side R n m).

Blank start: K('',0,0) at step 5, K('',1,0) at step 14, then K('1',0,1) at step 32.

Rules (all validated by direct simulation with tools/sim.py, scripts/validate_rules.py)

• R1 bounce (n >= 1): K(w,n,m) -> K(phi(w), n-1, m+1). The head leaves the boundary, does one left step phi on w and one right step on R n m, then comes back to the same cell.
• phi(w): if the last cell is 0, set it to 1. Otherwise take the last adjacent pair 00 (0^inf counts), set its left cell to 1 and every cell to its right to 0. (A reading 1 goes to F. F skips 1s leftwards because F1 = 1LF, and on a 0 writes 1 and goes back to A. A on 0 writes 1 and B erases back to the boundary.)
• TM1 (F1 = 0RB) and TM2 (F1 = 1LB) instead stop the scan at the first 11 they read. That single cell is the only difference.
• Overflow (n = 0): let f = phi(w) = x 1 0^q.
• R2 q even: K(w,0,m) -> K(x, m+1+q/2, 0) (the boundary moves q+1 cells left). This is the template's ROv.
• R3 q odd, x = x' 00 (or x empty): K(w,0,m) -> K(x', 0, m+(q+3)/2) (a reset: the right side swallows 2 more cells).
• R4 q odd, x ends in 01 or 11: halts.
• R5 q odd, x ends in 10: nested eating; no closed form (in random tests it sometimes halts).
• phi^j accelerated (rules.phij): the cells below the lowest 1 at an odd offset form a plain binary counter on their even offsets. When it fills, the next step lands in the part above. Validated against iterated phi.

Counters and big steps

• std(N): digits 01 = 1, 00 = 0, least significant digit next to the head (= the template's LC0 N = BinInc <[0;1] N).
• pk(N) (packed, N >= 2): the top two bits share one pair 1t, and the rest are std digits. phi = +1 on both, and the encoding never changes under phi.
• With N = (2k+1)2^i - 1 and b = 1+i+m, L = bitlen(k):
• std(N), m -> pk(2k+b), b when k is a power of 2 or 2k+b >= 2^(L+1); std(b), b when k = 0; otherwise a dirty word phi^b(std(k)0).
• pk(N), m -> std(2r+b), b with k = 2^(L-1)+r, r > 0, when 2r+b >= 2^L; std(k+b), b when k is a power of 2; std(b+1), b+1 when k = 0 (an all-ones counter: reset first); otherwise dirty phi^b(pk(k)0).
• So the counter alternates std / pk every cycle (Fig counter_rows). Compare TM1: N' = b-2k, invariant a <= 1+b; TM2: N' = b, invariant a = b.
• A dirty word is the transient after the overflow left the counter shifted by one cell (H0 = H followed by an extra 0). The orbit of std(k)0 becomes pk(2k+j) at j0 = 2^(L+1)-2k, and the orbit of pk(k)0 becomes std at j0 = 2^L-2r. Before j0, the overflow sees a dirty word. 2.8% of overflows do (473,792 of 17,000,000 cycles).

Where halting could come from

• Clean counters always overflow with q even (or the harmless all-ones reset). Only dirty overflows can have q odd.
• In a dirty orbit, q is odd exactly at the landings on odd offsets, about log2(k) points per orbit:
• R points, ending in 00: resets, harmless. Hit once from blank (cycle 27, step 199,243). Near misses at even distances 2, 4, 6 later. When an R hit is forced at 5 near misses, the dynamics recovers and runs 100k more cycles with no danger.
• N points (10) and H points (01/11): for std orbits N sits at value 3·2^(L-1), i.e. b+1 = j0-2^(L-1). For pk orbits H sits at b+1 = 2^(L-1)-2r. Hitting one needs b < 2^(L-1) <= k, i.e. N > 2m and N low in its octave.
• Measured from blank, abstract rules (validated against the direct C simulation: all 1,002 overflow configurations to 1e10 steps match):
• 17,000,000 cycles (m = 4.25e7, about 5e22 TM steps by the fit steps ~ 0.68 m^3): no H/N hit. Only 1 dirty reset and 4 all-ones resets.
• Closest approach over the first 6,000,000 cycles: H points >= 0.287·m away, N points >= 0.376·m away. The overflow always comes after them, a stable fraction of m, not a shrinking gap. The margin mu (distance to the H/N value in units of 2^(L-1)) stays >= 0.40 (pk) and >= 0.61 (std) over 400k cycles.
• Reading: the separation looks like an inequality invariant on (type, N, m) plus the dirty state, not pseudo-random luck. The invariant is not found yet. Simple bounds hold empirically (std: N < 2m; pk: N - m <= 2^floor(log2 N); m >= 0.44·2^floor(log2 N)) but do not exclude the H point by themselves.

Template comparison (BECv5.v TM1/TM2, about 140 lines each)

• Same: LC0 (std counter), R n m, LInc0, LIncs (std increments: F only ever reads 0), RIncs (R1's right half), and ROv for std counters (R2 with q = 2i, x = H0).
• Different: LIncs' (TM1: H0 counts down to LC0 0; TM2: to LC0 2^(i+1); here: H0 becomes the packed counter pk(2k+j)), a second counter encoding pk with its own ROv/LIncs, the dirty transients, the reset rule R3, and the invariant (progress_nonhalt_cond).
• Rulefit's "A0(4n+13,4m+3,2k+1)" parity-mixing reset is R3 at a dirty overflow.

Cryptid check (ground rule 6)

• The abstract system has halting branches (R4, and R5 sometimes), so non-halting rests on avoiding specific points.
• Avoidance is by a margin proportional to m (>= 0.29·m), not by a 1-in-N chance per cycle. Treating the hits as random (about 0.03 dirty overflows per cycle, about log2 m danger points per orbit of length about m) predicts a few hits within 17M cycles (25 octaves of m). None occurred, and the gap never shrinks.
• Verdict: not cryptid-like on current evidence. The invariant still has to be found and proved.

Files

• scripts/rules.py (phi, phij, std/pk, overflow, bigstep), scripts/validate_rules.py (-> work/validate_200.json), scripts/abstract_run.py, scripts/ovf.c (direct C overflow-configuration dump).
• work/overflow_configs_1e10.txt (direct, 1,002 rows), work/abstract_startA_17e6.out, work/danger_distance_6e6.out, work/abstract_startF_3e6.out, work/explore/ (exploration scripts).

Decision (2026-10-11)

Question: Fund one 2 h stage to find an invariant on (type, N, m) that keeps every overflow off the halting points, start proof.md with it open, or park? Answer: hunt (One stage (at most 2 h): find and test the invariant, then write proof.md). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, hunt)

Run 2026-10-11 (Dennis funded hunt: "go with recommendations"). Scripts in scripts/hunt/, outputs in work/hunt_*.

What was done

• Dirty orbits in closed form. The T-count of an orbit is 2·(O-cell barrier) + (E-cell counter), and phi adds 1 to it.
• gen 1, std(k)0: odd landings at T_g = 2((k>>g<<g)+2^g), one for each 0-bit g of k above its lowest 1. The landing is N if bit g+1 is set, else R. The top landing at 2^(L+1) is a reset with empty x.
• gen 1, pk(k)0 (r = k - 2^(L-1)): the same with r, the H point at T = 2^(L-1) (g = L-2), and an even merge at 2^L.
• gen 2, at a dirty overflow that is not a landing: x has E-bits K = k_s>>u and O-bits g = v>>(u+1). It merges into a clean counter at T_x = 2^(lowK+1).
• closedform.py gives one clean-to-clean step B covering 17 cases: clean, k = 0 / power of 2, top reset, pk merge-at-overflow, gen-1 N/H/R, gen-2 g=0 / merged / merge-at-overflow.
• Exact parity fact found: in clean steps N' - m' is 2k, 2r or 0. So N = m (mod 2) except after pk with k = 1, which gives N = m+1, and rare gen-2 g=0 steps, which give N = m+3. In the class N = m, i = 0 can never occur twice in a row. This parity was the missing correlation. A cell closure that treats i as free leaks into the H region (signed H margin -0.86·m). With parity-tagged cells it closes at once and keeps the margins (H >= 0.31 m, N >= 0.39 m).
• Invariant I (inv3.py):
• always 1 <= m <= N;
• parity class (N = m mod 2): std even 2N <= 3m+6, std odd N <= 2m+3, pk even N <= 2m+3, pk odd 2N <= 5m+6;
• broken parity: N <= m+3.
• The asymptotic constants are the fixed point of the max-ratio recursion (std even 9/7 and pk odd 16/7 on the real run, relaxed to 3/2 and 5/2 to absorb the parity-broken states).
• Safety: every N/H/R landing at an overflow needs b+1 <= 2^(L-1). That is N >= 2m+4 for i = 0 and N >= 4m+7 for i >= 1, and I forbids both.
• Under I only std i=0, pk i=0 and pk i=1 states in the parity class are dirty. Each sits in its final gap: barrier 3·2^(L-2) or 2^(L-2), T even so u >= 1, and n+1 > 2^(lowK+1), so gen 2 merges before its overflow (no gen 3).
• Closure: a hand case analysis covers every case of B (proof.md §6) and is checked by script (below).
• proof.md written (draft, as the funded option says): rules, closed-form B, I, Lemma S (safety), Lemma C (closure), init, 349 via start F, check list.

Results (numbers)

• B = phi iteration (cf_vs_phi.py, seed 2, rerun after the fix): 60,000 random states, 0 mismatches. Another 110,000 cross-checks at m up to 2^60 inside closure_random.py.
• B = direct TM (cf_vs_tm.py, tools/sim.py, random + constructed landing instances): seed 13, up to 100 instances per case, 1,587 instances, all equal (work/hunt_cf_vs_tm.json). Rare cases: std gen2 g=0 42, pk gen2 g=0 40, pk gen2 merge-at-overflow 4, std gen2 merge-at-overflow 1. The check caught one wrong closed form: a pk gen-1 R reset with k>>(g+2) a power of 2 leaves std(kp), not pk. It is fixed, and the case cannot occur under I. Gen-1 N landings are recorded only (no closed form).
• Exhaustive closure (closure_check3.py): all states with I and m <= 400 (83,499) and 401..1300 (772,875): 0 failures, 0 dangers. The closest approach is pk(2050, 1024): the H point is passed by 4 steps, in the final gap where it must be.
• Lemma checks (lemma_check.py):
• L1, who is dirty: dirty states are std i=0 (11,416), pk i=0 (47,943) and pk i=1 (3,612), all in the parity class.
• L2/L3, final gap, u >= 1, merge before overflow; L4, closure.
• 856,374 exhaustive states (m <= 1300) + 1,000,000 random (m up to 2^60): 0 failures.
• The first lemma draft wrongly claimed pk odd is never dirty. The check caught it (pk(133, 53), i = 1), and the i = 1 case is now in proof.md §5.3.
• Random boundary closure (closure_random.py): 200,000 (to 2^48) + 2,000,000 (to 2^60) + 2,000,000 (to 2^14): 0 failures.
• Real run (traj_inv.py): I holds at all 17,000,000 clean overflow states from blank (m = 43,683,205 at the end; work/hunt_traj_inv_17e6.out). Paths: 473,792 dirty two-cycle steps, 1 dirty step ending in an empty-x reset (cycle 27), and 4 all-ones resets.
• Start F (349 via TM518): (std, 0, 1) -> (std, 2, 2) -> (pk, 5, 3) -> (std, 6, 5), ...; I holds at 999,999/999,999 states after the start (work/hunt_traj_inv_startF_1e6.out).
• Figure img/ratio_classes.png (Fig 6): (N-m)/m per class on the first 1,000,000 cycles, with I's bound per class.

Still open

• The landing lemmas (gen 1 and gen 2) are derived from the validated phi closed form and checked by script. In Rocq they need phi^j lemmas on interleaved E/O words; nothing in BECv5 has them.
• proof.md has had no skeptic review yet (Checkpoint B, non-blocking).
• Next: formalization from BECv5 TM1/TM2 (packed counter, dirty orbits in their final gap, resets with empty x, I as the progress condition). The earlier estimate was 2-3 Rocq stages.

Informal proof stage (2026-10-11)

proof.md is now a complete informal proof (Checkpoint B pending, non-blocking). check_proof.py is new and self-contained: 133/133 PASS with seed 1 --full and seed 2 default. Logs: work/check_proof_full_seed1.log, work/check_proof_seed{1,2}.log. The hunt draft is kept as work/proof_draft_hunt_2026-10-11.md.

What changed from the hunt draft

• Low-level rules as exact TM runs.
• L0/L1 (the left step is phi): 1 or 2e+3 steps, with a proof.
• RS: an 8-row chain, 10n+7 steps. TM1 and TM2 run it identically, so BECv5 RIncs is reusable verbatim.
• OV0/CD/OVe/OVo: q+8 or q+14 steps; halts at step q+9 when x ends in 1.
• From these step formulas, every overflow time of the stored direct run comes out exactly, to step 9,998,414,763.
• One general phi lemma, SW, on W(e,o) words with an arbitrary high word Hi:
• (i) the counter below the lowest O-bit increments;
• (ii) the sweep lands on an odd cell, and the two cells above it are known;
• (iii) the carry leaves into Hi as phi(Hi·1)·0^(2h-1).

The sweep corollary (T-count, barriers) and O3–O6 replace the draft's "gen 1 / gen 2 landing lemmas", which had been stated but not derived. SW(iii) is needed only for four high words: 0^inf, 1, 101 and 11. - The 17-case step B is cut to 11 macro rules that can occur under I: S0 S1 S2 S3a S3b P0 P1 P2 P3 P4a P4b. Each has an exact precondition, including the gen-2 merge condition n ≥ 2^(h+1)-2g. Lemma S shows under I that no other case occurs: - std is dirty only with i = 0 in class P, and pk only with i ≤ 1 in class P; - each dirty state is in its final gap with u ≥ 1, and n > 2^(L-1). - Lemma C is redone per rule with D = N'-m'. Every inequality step of Lemmas S and C has its own check. - Halting. E is entered only by D1. In RS it reads a 0 that B wrote, and in OVo it reads x's last cell. Inside the macro rules OVo occurs only with x = 0^inf (S2, P0). - Lemma plan against BECv5 TM1/TM2: - verbatim: RIncs, LC0/LIncs (TM2), ROv (TM1); - new: the W(e,o) side, SW as digit shift rules on tm' = flip tm, O3–O6 modelled on TM2 LIncs', general OV, BigStep per rule, and I as progress_nonhalt_cond. - Start F (349). K(0^inf,0,1) at step 14, then (std,2,2) at step 73 (not 63), then (pk,5,3) and (std,6,5).

Check sizes (seed 1 --full)

• Exhaustive closure: m ≤ 1300, 856,374 states. Per rule: S1 310,432; P2 472,561; P4b 51,019; S3b 11,369; P1 8,214; P0 878; S0 677; P4a 536; P3 441; S2 200; S3a 47.
• 300,000 random boundary states up to m ~ 2^60.
• Macro rules against direct TM simulation: 30 states per rule.
• I holds along 2,000,000 blank-tape macro steps (m = 5,148,737).

Next

Formalize (2–3 Rocq stages). Order: OV and SW digit lemmas first (the new parts), then O3–O6 as sideRLs lemmas, then the BigSteps, then the arithmetic of Lemmas S and C, one lemma per rule.

Skeptic round 1 (2026-10-11)

The verdict was "sound", with two minor gaps. Both are fixed in proof.md and check_proof.py, and status is now CHECKPOINT_B. - 349 is a mirror. Eqv_v3 TM518 tm is this table mirrored and renamed, started in F. It is not "started in F" alone. - For Rocq the reduction is the Skelet15.v pattern: TM518.eqv, then Flip.flip_halts_c0, then Permute.perm_nonhalt with f = (A->F, B->A, C->B, D->C, E->D, F->E), then execute for 73 steps from F;; tape0 to S(std,2,2), then an exported nonhalt_I : forall s, I s -> ~halts tm (S s). - Flip.v's functional_extensionality_dep is already in the kill baseline. - Mirroring every side lemma, as the skeptic proposed, is only the fallback. - Still to do: time TM518's solve_eqv (fixed NG parameters) alone before relying on a copy of it. - Where a macro step ends. Each macro rule ends at the first clean overflow state with N >= 1. (std,0,M) is an intermediate state inside S2 and P0, outside I, and S0 leaves it. BigStep_S2 and BigStep_P0 are composed with BigStep_S0, and S(std,0,M) is never a progress_nonhalt_cond state. The text changed; no rule or bound did. - check_proof.py: 147/147 PASS with seed 1 --full, seed 1 default and seed 2 default; it had 133 checks before. - New F checks: the mirror/rename string identity, the Eqv_v3 strings and eqv, 349 and this table on the 740 list, the Perm table, and a lockstep run (1e6 steps with --full). - New B checks: endpoint = first clean state with N >= 1; the direct TM's overflow states = the abstract trace; (std,0,M) only in S2/P0, once, outside I, then S0. - A scratch mutation run (start in A, or two states swapped in the renaming) makes the new F checks fail.

Kill

KILLED_NONHALT (2026-10-11). check_kill PASS, independently re-verified (audit: one --json run, PASS, all 17 checks, coqchk pass 26.7 s, the whole .v read; holdout membership confirmed at 778 line 240 / 740 line 224). - Kill file: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v, 1,217 lines, Individual62 only, 105 Qed, no Admitted. sha256 20521ad7e52872407bf6a03250bdd5064676def5b770fd65ab06eb49026238f1 (same as the round-2 PASS and the audit run). - Fresh packaging run (2026-10-11T17:59:26Z): RESULT: PASS, exit 0; compile 65.8 s (-native-compiler yes), coqchk -norec pass 29.6 s, Print Assumptions closed (0 entries). Log: rocq/check_kill_final.log (= submission/check_kill.txt). - Proof: init0 (32 steps to K 1 0 0 1 = (std,1,1)), then progress_nonhalt_cond with P := I and step_I (11 macro rules BS_S0..BS_P4b, coverage Cov_S3/Cov_P4, closure C_S1/C_P1/C_P2/close_*). Template: BECv5 TM1/TM2 (same table except F1). - Package: submission/ = the .v, a public proof.md (rewritten from this folder's proof.md; mathematics unchanged, new §8 maps it to the .v, §9 lists the numerical checks without script names; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh human-readable run), README.md, discord.md (not posted; 1,538 characters before <LINK>). - Still open: 349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (740 line 349, sheet row 1038) is covered by the same mathematics (proof.md §7.3) but not formalized; route in status.json family_note. Checkpoint B had no notes from Dennis when this was packaged.