/machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/rocq/log.md · raw

Machine #3 formalization log (rocq/)

Round 1 (2026-10-10)

Layout

rocq/cc.sh FILE.v: compiles a copy in a temp dir (ulimit -s unlimited, -v 8000000, native on).
rocq/rules.v: low-level sweeps + K-level macro rules (compiles, ~6 s).
rocq/trace*.py: tape tracers used to find the sweep milestones.

Low-level structure found (all proved by plain `es`, symbolic powers)

A macro step = Start (3 short bounces; A -> B entering pair 1) + one long rightward sweep in state B + a turnaround + one leftward sweep + an end phase at the left edge. - Rightward sweep over a pass pair [p,q+1,0] leaves the region 0 (01)^p 110 (01)^q 11 (left list reg p (q+1) l), the leading 0 being the boundary cell. - Two leftward modes: - Dec mode (state D arrives reading the region's trailing 0): PassL turns the region into [p+1,q,1]; EndPh rebuilds (10)^(h+4) 11001. - Ov mode (D arrives reading the region's last 1, its boundary 0 already on the right): OvL turns reg (p+1) q into (01)^(p+1) 0001 (10)^q (needs p>=1); OvEnd builds (10)^2 11001 (10)^(h+5) (01)^(p1-1) 0010 (needs p1>=2). - Turnarounds: Borrow (d=1, q>=2), MergeB (d=1, q=1, any continuation r: covers DecMerge and DecMergeTail with one lemma), MergeE (q=1, then 0^inf), EndT, EndLastT, OvT, X2T (needs k>=1), and X1Sw (Dec-mode milestone over a q=1 region switches to Ov mode). - List lemmas PassesR, PassesL, OvPasses by induction on the pair list, with LP = left fold of reg, RP = right fold of pair words, OvR = Ov-mode output.

K-level rules proved (proof.md section 2 numbering)

Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR (End), EndLast, X2, Ov, X1: every rule of the table, each as K h P T -->+ K h' P' T'. Ov/X1 outputs are ovp/ovpX (re-pairing functions). init : c0 -->* K 2 [(11,11,false)] TN by esx (956 steps), compiles.

Pitfalls hit

es overshoots a target whose right side differs only by a power rotation ([1;0]^^(S t) *> [0;0;1] vs 1 >> [0;1]^^t *> [0;0;0;1]): it keeps stepping and gets stuck later. Fix: pick the milestone/form es reaches (or the next natural stop).
es stops when the head must read a power w^^n whose first period is not a shift-rule period (e.g. E entering [1;0]^^p): state such lemmas with ^^(S p).
Under the sym scope, tuples (p,1,true) parse 1 as a symbol: write 1%nat.
okR x (a let-pattern Definition) cannot be destructed by an as [..] pattern after inversion: use hnf in Hx; destruct Hx.

Kill file state at end of round 1

1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v = rules.v + init0 (c0 -> K0, 956 steps) + init (c0 -> base E-start K(2;(95,68,0),(34,33,1),(10,15,1),(1,24,1);-), 78,710 steps, esx, ~30 s) + rule-table comment. No nonhalt yet (check_kill cannot pass). Everything compiles. So the "finite chain K0 -> overflow-6 base" of proof.md 3.7 is not needed: direct execution works.

High-level plan (rounds 2-4): a PER-STEP invariant J, not a per-cycle `period` lemma

Use progress_nonhalt_cond with index i = (h, P, T, phase, c4) and C i = K h P T, so every macro rule is one -->+ step and J only has to be preserved by single rules. Ghost phase: E1 (regular E-cycle before End), E1t (after X2), T0 (T2 start, before X2), E2/E2t (after End), L1 (EndLast-type L-slot before EndLast), LX (X1-type L-slot), L2 (after EndLast); ghost c4 (L-slot after a T2 start, before its DecMergeTail).

Key quantities (all per pair j, N = #pairs, n = N - j = #pairs to the right): - tv_j := value of digits d_j..d_N (d_j least significant) = touches left in this countdown. dv of the suffix starting at j. Dec_k: tv_j -1 for j <= k, unchanged for j > k. - extra(phase,n) := 2^n (E1, E1t, L1), 52^n (T0), 0 (E2, E2t, L2, LX). - Rt_j := tv_j + extra = touches pair j still gets before the cycle's re-pairing. - Phat_j := p_j + Rt_j, Qhat_j := q_j - Rt_j (as integers). A touch keeps both, and keeps p+d and q+d mod 2. End/X2 touch the last pair without flipping its digit, and End/EndLast/X2 match the extra-term switch exactly (checked by hand: Phat, Qhat unchanged). - hhat := h + 4Rt_1 (every step touches pair 1, so h grows 4 per touch of pair 1). - DecMerge at k (H := tv_{k+1}): fused pair inherits pair k+1's Rt (Qhat_fused = Qhat_{k+1}, Phat_fused = Phat_{k+1} + p_k + 3); pairs j > k+1 unchanged; pairs j < k: Phat drops by 2^(k-j) H + [phase 1] 2^(N-1-j), Qhat rises by the same.

J clauses (validated in rocq/jcheck.py + jrand.py: base orbit 26 overflows incl. X1/X2, and 1,900 random INV+(e)-style starts, many at the thresholds, 4 overflows each: 0 failures): - all p,q >= 1; h = 2 mod 4. - E phases (L = N, or N+1 in T0; interior = j <= N-1, all j in T0): Eq: Qhat_j >= 22^n + 1 (E1,E2,T0) / 2^n + 1 (E1t,E2t); Ep: p_j + d_j odd (T0 top pair: even), Phat_j >= 32^(L-j); far pair Qhat_N >= 1; (e1) Phat_1 >= 2^(L+2) + 32^(L-1) - 3; (e2) Phat_2 >= 2^L + 32^(L-2) - 1; hhat >= 32^(L+1) - 6; L >= 3; T = TN / TA 1 / TB k>=3. - L phases (Lproj = N (L1, LX) or N+1 (L2); f_j = N-j (L1, LX) or N+1-j (L2); c = 4 if c4 or LX else 5): Eq p-blocks: Phat_j >= c2^(f_j); Ep q-blocks (j >= 3): Qhat_j >= 1 or q_j+d_j even; in L1 while the last digit d_N = 1: q_j >= tv_j - 2^(N-j) + 2 (no run-out in the first half); pairs 1,2: Qhat_1 >= 2^Lproj, Qhat_2 >= 1; hhat + 6 >= 2^(Lproj+2); far end: L1 last pair Qhat_N = 0, x-pair Qhat in {-2, 0} or >= 1; LX: Qhat_{N-1} = Qhat_N = 1. Why it closes: merges to the right keep Phat_j >= c2^f for any c >= 3 (loss < 22^(f-1)+2^(f-1)); merges only happen in the second half of L1 (d_N = 0), so H <= 2^(N-k-1) and hhat loses < 2^(N+1) = the drop of 2^(Lproj+2) (this replaces the reviewer's missing "pair 1 gets

= 2^(L*')-2 touches" lemma); the fused block inherits Phat_{k+1}. Ov/X1 map the L2/LX clauses onto the E1/T0 clauses exactly (worked out per pair: new q_{j+1} = old p_{j+1} etc.). Note: this per-step J does NOT need proof.md's r' >= 2r-3 (G3) nor the fusion bound.

Rocq plan: Fixpoint dv, AllSuf (predicate on every suffix: per-pair clauses only depend on the suffix: n = length-1, tv = dv, last digit), lemmas dv_touch, dv_merge, dv_lt (dv S < 2^|S|); then Jstep : J i -> exists i', K.. -->+ K.. /\ J i' by phase/rule case analysis with lia (introduce 2^n as variables + doubling facts), and nonhalt from init + base satisfies J.

Also in round 1

rocq/dv.v (compiles, standalone): dv (digit value, pair 1 least significant), dv_lt (dv P < 2^|P|), dv_dec (a Dec lowers every touched suffix value by 1), dv_merge (dv before = dv after + 1 + 2^|Z| * dv(next pair :: R)), dv_ones, AllSuf. To be pasted into the kill file when J is formalized (needs touch unified with rules.v's).
Random J tests exercise every rule: over 200 starts x 4 overflows, DecMerge 603, DecMergeTail 135, X1 15, X2 112, EndLast 385.
check_kill on the round-1 file: FAIL, only theorem_text (no nonhalt); forbidden tokens, structure, tm string all PASS.

Next steps (round 2)

Define J in Rocq (per-suffix clauses via AllSuf; use nat inequalities like q + 2 >= tv + ex instead of negative Qhat), index type, C i := K h P T.
Decomposition lemma: J -> one of the 9 rules applies (split at the first digit 1).
Preservation per rule (touch/merge lemmas on suffix clauses, Ov/X1 re-pairing by induction on the list), then nonhalt = multistep_nonhalt + init + progress_nonhalt_cond, with J base by vm_compute/lia.

Round 2 (2026-10-10)

J formalized (rocq/J.v, standalone, compiles in ~28 s)

Per-pair clause PC ph c4 h i p q n tv = 1<=p /\ 1<=q /\ PN ph c4 p q n tv /\ PI ph h i p q n tv: PN matches on n (0 / 1 / >=2), PI on the index i (1 / 2 / other). Parity is stated on p+tv and q+tv (tv = d mod 2), so no digit case split is needed. AllI Pr i P = Pr on every element with its 1-based index and the list to its right; PCx = Lift PC computes n = length, tv = dv.
Per-rule arithmetic obligations ob_* (touch, merge, merge-tail, fuse, far, End, EndLast, X2, Ov head/step/base, X1 head/step/base); list-level lemmas inv_Dec, inv_Merge, inv_MT, inv_End, inv_X2, inv_EndLast, inv_Ov (generic AllI_ovp), inv_X1 (AllI_ovpX); shape helpers Z_okL, borrow1 (a q=1 run-out only in L phases, index >= 3, L1 second half, LX n>=2), q2_V0, p1_V0, L2_c4_V0, AllI_okRO, AllI_len.
Differences from the round-1 Python J: the E far pair also has p + Rt >= 3 (needed so x >= 3 at the Ov); L1's first-half clause is stated unconditionally as q + 2^n >= tv + 2 (equivalent given q >= 1); L-phase q-blocks at n >= 2 (L1/LX) or n >= 1 (L2) must have good parity (the Qhat >= 1 alternative is only for the x-pair / top pair). All proved, so these are the real clauses.
Tactics that mattered: ZifyNat must be imported for lia to handle mod 2; lia with many implications + mod is 3-5 s per goal, so clauses are matches on n and i and every obligation destructs n/i first (cr = cbn -[Nat.modulo]; split hyps; repeat split; lia): 25 s for all. |-> lexes as |- > in intro patterns: write [-> | [-> | ->]]. Make tri a Notation, not a Definition, or rewrite misses @cons tri vs @cons (nat*nat*bool) terms.

Step lemma and nonhalt (rocq/Jtm.v)

State st = (h, P, T, phase, c4), Cf s = K h P T, J s = P <> [] /\ TC phase c4 T /\ AllI (PCx phase c4 h) 1 P. TC: E1/E1t/LX: TN (c4 = false); L1: TN; E2/E2t: TA 1; T0: TB k, k >= 3; L2: TA t, t >= 2.
Jstep : J s -> exists s', Cf s -->+ Cf s' /\ J s', by split1 (first digit 1, or all 0): digit 1 with q >= 2: Dec (all phases); q = 1: borrow1 restricts to L phases, then DecMerge, DecMergeTail (L2 only), DecMergeEmpty impossible; all digits 0: E1/E1t End, E2 Ov to LX (x = 4, decided by lastOK_dec) or L1, E2t Ov to L1 with c4, T0 X2, L1 EndLast, L2 Ov to E1 (c4 = true impossible: top pair would have q = 0), LX X1.
J_base by cbn; repeat split; lia; nonhalt = multistep_nonhalt init + progress_nonhalt_cond.
Assembly: rocq/assemble.py OUT [--dev] = round-1 rules (rocq/rules_r1.v, a copy of the round-1 kill file) + J.v body (standalone header and copies of ovp/ovpX/okL/okR/okO/touch dropped) + Jtm.v + rule table. --dev drops init/nonhalt (no 30 s esx). Dev compile 36 s (native off).
Pitfalls: String shadows length (bridge does Import Coq.Init.Datatypes.); BusyCoq's notation c -[ tm ]->* c' makes -[ a token, so cbn -[Nat.modulo] breaks parsing of the NEXT sentence: write cbn - [Nat.modulo]; eapply on a lemma whose first premise mentions a not-yet-instantiated phase (?ph <> LX): solve that premise last.

Result (round 2)

tools/check_kill.sh on the kill file: RESULT: PASS, exit 0 (report in rocq/kill.out): compile 67 s with native on; coqchk -norec finished in 24 s (no timeout); Print Assumptions of nonhalt: closed (0 assumptions). sha256 91861259c71ce3338425a86a465c4af5b854f63f071737b8cd7feaa36713fcbf.
No flaw found in proof.md's argument. The formal proof uses a per-step invariant rather than proof.md's per-cycle INV+(e) and lemmas L5'/L6. L6 (pair-1 touches) is replaced by the projected-h clause (h + 4*Rt_1 + 6 >= 2^(Lproj+2)) plus "merges in L1 only in the second half" (the first-half clause q + 2^n >= tv + 2), and L5' by the Phat bounds p + Rt >= c*2^f (c = 4 or 5).
To rebuild: edit rocq/J.v / rocq/Jtm.v, then python3 rocq/assemble.py OUT (round-1 rules come from rocq/rules_r1.v).

Kill packaging (2026-10-10)

Independent audit: check_kill --json PASS at 14:04:09Z (17/17, compile 69.4 s, coqchk 24.4 s, 0 assumptions); holdout line 53 of the 778 list.
Fresh human-readable run for the submission: PASS at 14:06:34Z, compile 69.3 s (native on), coqchk 24.3 s, closed. sha256 unchanged (91861259...fcbf) before and after.
status.json = KILLED_NONHALT / done. Package: submission/ (.v, proof.md copy with a §4 map from sections to lemma names, check_kill.txt, README.md, discord.md: 1,752 chars + <LINK>, not posted). notes.md ## Kill, STATUS.md line, atlas/rocq-notes.md packaging datapoint.