Machine #14 formalization log

Machine 1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB. Kill file: machines/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB/1RB---_1LC1RE_1LD0LC_1LE1LC_1RF0RE_1RA0RB.v (built from rocq/m14_base.v plus a header and the closing rule table; keep the two in sync, or edit the kill file directly from round 2 on).

Compile (one at a time, outside vendor/): rocq/cc.sh <file.v> Kill [builddir] (default builddir $TMPDIR/m14_build). It runs

eval $(opam env --switch=bb6); ulimit -s unlimited; ulimit -v 8000000
cp <file>.v $SCRATCH/Kill.v && cd $SCRATCH && coqc -Q <repo>/vendor/busycoq/verify BusyCoq -Q <repo>/vendor/busycoq/verify/BigInt BigInt -native-compiler yes Kill.v

The whole file currently compiles in 3.0 s with 455 MB (1,000 lines).

Round 1 (2026-10-13)

Architecture

The proof is split at Theorem U. Everything above it is about unit words only, with no machine steps:

nonhalt  <==  AbsDefined  :=  forall t U, Reach t U -> exists U', Pops (rk t) U U'

• Reach is the record-level dynamics. It starts at Reach XC U0 and steps with Reach t U -> Pops (rk t) U U' -> Reach (rnext t) (rF t ++ U').
• Pops k means k times "three carries (Inc), then the first unit is P and is removed". This is exactly the W-rule use of Lemma N.
• nonhalt_of_abs : AbsDefined -> ~ halts tm c0 is proved (init + windows + progress_nonhalt_cond).
• So the remaining work is pure unit-word mathematics: proof.md sections 3-7 (conveyor, Lemma T, invariant) and section 6 (Theorem B).

Proved in round 1 (all in the kill file, no axioms)

Machine layer, done - ArrS r r' := forall l, l {{B}}> r -->* l <{{C}} r', the arrival on a side. - Unit lemmas arr_Z, arr_D1, arr_P, arr_W (by step/follow/execute). They take the arrival on the rest as an argument, so they hold for every left context. - Units: unt = uD0 | uD1 | uP | uS1 | uSP | uW (do not use S1/D/A... as names: S1 is a Sym constructor and A..F are states). Related definitions: enc, Rs w = enc w *> const 0, and shift, which returns None on a hit (S1, SP or W). - Inc is an inductive relation (no stacked heads; a hit is simply not derivable). - inc_arr (Theorem U) is proved by induction on the Inc derivation. Inc_det is proved too. - Window runner wrun on lcfg = (left cells, head, right cells, state). - The left side is followed by 0^inf and the right side by an opaque side X. - It applies the W rule (wready/wpop, sound by arr_W + inc_arr) and stops when the head leaves the window to the left. - wrun_spec gives -->+ for any unit word, given Pops k. - window t : Pops (rk t) U U' -> rcfg t U -->+ rcfg (rnext t) (rF t ++ U'). All 8 record types are proved by one vm_compute, and they reproduce proof.md section 4 exactly (pops 3/12/2, F lists). - init : c0 -->* rcfg XC U0 (203,465 steps): cconfig_evstep_dec_spec with n = 1e6 and vm_compute, under 1 s.

Carry library, started - IncN with add/split/det/snoc. - P transparency: IncN_P, IncN_P_inv, IncN_Ps, IncN_Ps_inv. - IncN_digit, and the r-digit counter IncN_digits: t carries on digits r v ++ rest pass ((v mod 2^r) + t) / 2^r carries up. - Wall rotor wall_feed: t carries on wallu b :: r give Ps f ++ wallu (odd (t+b)) :: r', with f = (t+b)/2, whenever Pops f r r'. - So a conveyor wall is literally "f Inc3Pops on the rest". - Inc3Pop_P, Pops_Ps, Inc3Pop_wall and Pops_add/Pops_split support it. - C1 (Lemma C1).

Closed zone system, interface fixed - cs_step Z D j Z' D' j' (relational): exists m A Y, IncN m Z (Ps A ++ Y), notP Y, m = D + pj j + 3A, no fixed point m' < m, shift Y = Some Z', D' = D + A, j' = S j - CSreach, starting from Z1 = S1 D0 D1 D1 D1 D0 D1, D = 0, j = 1. - Executable step csf (fuelled incf/incNf, cs_loop to the least fixed point). csf_sound includes the minimality clause. - C0_reach : CSreach [S1 D0 D1 D1 D1 D1 D1] 16 17: this is C(0), proved by vm_compute through csf_sound.

Upward flow (Lemma L item 1), done - IncX X e X': X passes e carries up, and every shift lands inside X (shiftX refuses to escape). - IncX_flow: IncX X e X' -> IncN e Y Y' -> Inc (X ++ Y) (X' ++ Y'). IncXN_flow is the n-carry version. - The executable incXf is covered by incXf_sound.

check_kill (round 1)

rocq/check_kill_r1.log: FAIL only on theorem_text ("expected exactly one top-level Lemma/Theorem nonhalt, found 0"). - Every other text check passes: args, input, framework, framework_build, forbidden, structure, tm_text and integrity. - The Rocq layers did not run. - This is expected: nonhalt can only be stated once AbsDefined is proved.

What remains (the plan for rounds 2-4)

AbsDefined needs two independent developments.

(I) Zone: the closed system never gets stuck

Target: forall J, exists Z D, CSreach Z D J for every J ≥ 1. Since cs_step is deterministic, this means the orbit is infinite. Every IncN m Z .. inside it is defined, and shift never hits. - It comes from proof.md section 6: Theorem B for every b, plus C0_reach as the base. Lemmas Z0 and Z1 are not needed in this formulation, because "defined" is built into cs_step. - Needed: 1. Upward flow: done in round 1 (IncX_flow, IncXN_flow, incXf_sound). 2. Bulk feed engine. The representatives have feeds near 2^56 (endgame) and T0 = 2^19, so single carries are far too slow (about 6e10 carries). This needs a verified bulk feed: - a digit block takes t carries at once (IncN_digits); - P passes them; - S1 takes 1 and becomes P; - SP/W go through wall_feed firing by firing (zone walls dissolve after a few firings). 3. Lemma L / L' as Coq theorems about two runs (member vs representative, cut R, Δ ≡ 0 mod 2^R). - The per-step core is upward flow for the first T0 carries, then counter arithmetic after T0 (IncN_digits), then the value bookkeeping H' = (H/2^a + Δ)/2^b. - The representative checks (H0)-(H2) and κ are a boolean checker run by vm_compute, with a soundness lemma. 4. Lemma E (3 steps) and Lemma P (5 steps) on closed forms: digits/bin arithmetic with lia/nia on 2^k. 5. Lemma VF (1,304 one-step representatives at R = 8), the endgame (smaller split: R = 12, 4,094 residues), the nested range 11 ≤ v ≤ 50 (80 runs), the small classes (655 runs) and the class recursion (well-founded induction on K, switching to the induction hypothesis from v > 50). - Size estimate: the largest part, 2-3 rounds.

(II) Conveyor + Lemma T + record invariant (proof.md sections 3-5 and 7) - Represent the conveyor as walls with absolute positions: bw base [(x1,b1);...;(xk,bk)] z Z = Ps(x1-base) ++ wallu b1 :: Ps(x2-x1-1) ++ ... ++ wallu bk :: Ps(z-xk-1) ++ Z - One record step = (rk t) times "feed 3 carries at the bottom, then base += 1", then prepend rF t (new walls, R = 0). - Per-bottom-carry lemma by induction on the wall list: - wall_feed gives the wall's firings as Inc3Pops on the rest. - Pops on the rest follows from "IncN (3f) rest (Ps f ++ ...)" plus "the leading P count after 3i carries is ≥ i". For a wall above, it moves ≥ 1 per 3 carries. For the zone, the leading P count is the wire plus drops: this is the absorption condition. - The top wall can be absorbed mid-feed. Its firing is then Inc_W with shift landing in the zone, not a pop, and the next wall becomes top. Several absorptions can happen in one record step (Y→Z steps absorb 3). - The zone part of the invariant is: zone = inc^m(CS_J) with its leading P units moved to the wire. The absorption happens exactly at the least fixed point m = c + 3A(m) with c = D_J + p(J mod 8). - This is Lemma T: c = 3(43 + D_J - b_J) - E_then(J), and E_then(J) is read off wall J-1's absorption. - The bracket 43 - 3b_J + 2b_{J-1} + s_{J-1} + H_{J-1} must be computed from the birth tables (proof.md section 4) and checked equal to p(J mod 8). That is a finite check; J = 1..6 uses U0's walls. - Invariant Inv(n, J) as in proof.md section 7 (explicit in n and J, with the R chain from the youngest wall). Closure is the per-carry lemma + the Lemma T algebra (lia with floors) + (I). - Size estimate: 1-2 rounds.

Tactic notes (round 1)

• WORKED: unit lemmas with the IH as an argument. do k step. follow H. execute., where H : ArrS r r' = forall l, l {{B}}> r -->* l <{{C}} r'. follow unifies the left context through tl/hd without help.
• WORKED: a finite window with an opaque right side as a function (wrun on lcfg, sound by lstep_spec and wpop_spec) instead of tactic stepping. All 8 windows (1,700 steps, 17 W-rule uses) check in one vm_compute.
• lc X (l, m, r, q) is convertible to l *> const 0 {{q}}> ... / <{{q}}, so the window lemma follows from wrun_spec with only Rs_app + Str_app_assoc rewrites.
• WORKED: init via change (rcfg XC U0) with (cconfig_to_config ([], rg XC ++ enc U0, 0, C)) then cconfig_evstep_dec_spec (n = 1000000), vm_compute, reflexivity.
• PITFALL: cbn in H unfolds 3 * A to A + (A + (A + 0)) and unfolds Fixpoints deeply, so later destruct (f x) eqn:E / Nat.eqb matching fails ("No primitive equality found", unfinished bullets). Use cbn [f] in H.
• PITFALL: D, A, B, ... are state constructors, so let '(Z, D, j) := s and | Some (m, A, Y) => treat them as constructors (type error "constructor of inductive type state"). Use lower-case pattern variables. Numerals 0/1 in match n with 0 => ... are Sym (sym_scope is open): use O/S, or nth on a nat list.
• PITFALL: destruct (Nat.eqb_spec m x) does not rewrite the Nat.eqb inside a hypothesis. Use destruct (Nat.eqb m x) eqn:E; [apply Nat.eqb_eq in E | apply Nat.eqb_neq in E].

Round 2 (2026-10-13)

New idea: families instead of representatives

Lemma L (two runs, a representative and a member) is replaced by a one-run statement. - Once X (the part below the cut) is clean after the first T0 carries, the rest of the step acts on X only through c mod 2^r. - So one concrete run of X at the smallest feed covers a whole affine family of states. - A family (X, y, ay, D, j, aD) stands for, for every u >= 0: zone X ++ bin (y + ay u), D + aD u, j + aD u - κ of Lemma L becomes the coefficient ay. - While ay is odd, the cut shrinks. - When ay is even, fnorm pulls digits from Y back into X. - T0 is the family base's own feed (T0 = c0). No separate T0 is needed: it works for all 4,829 runs.

Proved in round 2 (dev files rocq/r2/{Zone,SC,EG}.v; assembled single file rocq/r2/Kill_r2_hdr.v)

Binary words - binp/binN/bin (bin through N, so Inc (bin v) (bin (S v)) is a 3-line induction on positive). - IncN_bin, bin_eq/bin_pos, digits_app_bin, bin_ones, digits_val, val_lt.

Carries through a cut - XN t X e X' := forall Y Y', IncN e Y Y' -> IncN t (X ++ Y) (X' ++ Y'). - Closure lemmas XN_P/digit/S1/SP/W/add. - The bulk feed xfeed : nat -> N -> list unt -> option (list unt * N) with xfeed_sound. - Digits halve the count, P passes it, S1/SP take one carry. - W fires once: 3 carries go up, then shiftX, and the rest passes the new P.

Clean words are counters - XN_clean: allb cleanu X = true -> XN t X ((val X + t) / 2^(ndig X)) (fill X (val X + t)). - fill_mod: the X part depends only on t mod 2^(ndig X).

cutstep (the locality step)

XN T0 X e1 (Ps A ++ X1) -> dhead X1 -> XN (c + 3A - T0) X1 e2 X2 -> T0 <= c -> c = D + pj j ->
IncN (e1 + e2) Y Y' -> shift (X2 ++ Y') = Some Z' -> cs_step (X ++ Y) D j Z' (D + A) (S j)

This includes the least-fixed-point clause. Y is arbitrary: any word with IncN e Y Y' works, so a marker P in Y is fine.

Families - fam, fz, fstep, frun, canonb. - fstep_sound : fstep R F = Some F' -> forall u, CS (fz F u) (fz F' u). - canonb_sound, frun_sound : frun n R F = true -> forall u, exists b', CSplus (fz F u) (Cst b'). - Fallback for concrete runs (aD = 0): when the absorption shift lands above X, as in the o0 = 1 direct runs (the shift lands on the overflow D1), the full shift is applied to X2 ++ bin y.

Theorem B pieces (all proved, no axioms) - small_classes : b + 2 = o 2^k -> odd o -> k <= 40 -> exists b', CSplus (Cst b) (Cst b'). - 327 direct runs + 328 families (o mod 16, cut k + 9): sc_all, vm 5 s. - Value forms: vfl (heads at positions 0..3, marker P at L), vlow (the low R digits), vfl_split, vlow_mod. - Rows: phrows (phase table of proof.md 6.2), vfz, off_end, VFe k Om (the value form at off_end(k)). - eg_family: one egok k0 Om0 R check covers every (k, Om) with k ≡ k0, Om ≡ 0 (mod 2^R), k >= k0 and Om >= Om0. - endgame : 41 <= k -> (k+9) mod 2048 <> 0 -> 1 <= U -> exists b', CSplus (VFe k (U 2^(k+5))) (Cst b'). - 4,094 families, cut 12, base Om0 = 2^46: eg_all, vm 23 s. - nested : k + 9 = s 2^v -> odd s -> 11 <= v <= 50 -> 1 <= U -> .... - 80 families (s mod 4), cut v + 2, base Om0 = 2^(v+10): ns_all, vm 1 s. - E_low: E(K) of proof.md 6.5 for every K >= 41 with nu2(K+9) <= 50 (no induction hypothesis). - Python prototype of the runner (mirrors the Coq functions): rocq/r2/fam.py, vf.py, nested.py.

What remains

(I) Zone 1. Lemma VF (descent from off 20 to off_end). - Plan: a generic one-step lemma from cutstep with X = the low 8 digits (heads, plus the marker for 5 <= L <= 8) and Y = binP (L-8) (V/256) (marker in Y), or bin (marker in X). - Per-class concrete check of phase 1 with T0 = 2^12, and the X3 / next-form match. - Classes: 12 entry offsets + off mod 256 for L >= 9 + (off mod 256, L) for 5 <= L <= 8. - Plus the three affine identities of proof.md 6.3 item 3, checked per class: mu + 2^a = 2^(a+b) mu' alpha + 2^a = 2^(a+b) alpha' q0 + e1 + floor((val X1 + K)/2^nd) = floor((alpha'(off0+1) + beta')/2^nd3) These use Z for the negative w and the 3·2^(L-1) term. - Then induction on off. 2. Lemma E (17 → 20) and Lemma P (12 → 17), by hand on closed forms with the bin lemmas plus cutstep. Steps whose shift lands far up (17 → 18, 13 → 14) need a direct cs_step proof. 3. Identification (plant end = VF level 2 at off' 17), the class recursion (well-founded on K, K' = v − 10, from v > 50), Theorem B, then forall J, exists Z D, CSreach Z D J (from C0_reach and j' > j).

(II) Conveyor + Lemma T + record invariant. Unchanged from round 1's plan.

Tactic notes (round 2)

• PITFALL (cost 20 min): cbn [negb] in H on a hypothesis holding an unfolded big definition (fstep, which contains xfeed 4000) makes Qed hang, even though the tactics finish in 3 s.
• The kernel conversion goes astray.
• Fix: rewrite if_negb_true in H with if_negb_true : (if negb true then x else y) = y (instant).
• Bisect Qed time by closing the remaining goals with a dummy hypothesis Hno : forall x, shiftX x = None -> False (exfalso; apply (Hno [uS1]); reflexivity), so Qed still runs.
• PITFALL: inversion H on Some (.., 3 * N.of_nat a, ..) = Some .. reduces N.mul 3 _ to a match on N.of_nat a, and later rewrites find nothing.
• Use injection H as <- <- <-.
• Wrap such terms in an opaque helper (n3 a := N.of_nat (3 * a) with n3_spec).
• PITFALL: sym_scope again. = 0, = 1, [1; 3; ..], replace x with 0 and Nat.eqb k 0 in a goal all read 0/1 as Sym.
• Write O, 1%nat.
• For N.to_nat 2, use change (N.to_nat 2) with 2%nat; replace fails with "Terms do not have convertible types".
• PITFALL: && is not andb under busycoq's scopes ("The term No has type {..}+{..}"). Fix: Local Open Scope bool_scope.
• PITFALL: never let a nat like s0 * 2^v - 9 (v up to 50) reach vm_compute: Out of memory at 4.5 GB. Family bases are N throughout (off_endN, egL, egV, egF take k0 : N).
• PITFALL: lia/nia with x mod 2^n = 0 hypotheses in context can run for minutes. clear them, or give lia a minimal context (clear -Hc; lia).
• WORKED: per-family soundness as one generic lemma (eg_family) plus one boolean check over all classes (forallb .. (upto 4096)), extracted with forallb_forall and upto_In.

Kill file and check_kill (round 2)

• The kill file now holds everything: 2,291 lines; one coqc in 133 s at 2.6 GB.
• That breaks down as about 23 s ×2 for eg_all, 5 s ×2 for sc_all, about 10 s for fstep_sound's Qed, and about 40 s of nia/lia in the bridge lemmas.
• From round 2 on, the kill file is the source of truth. rocq/m14_base.v is the stale round-1 body.
• rocq/r2/{Zone,SC,EG}.v are the dev splits (they Require M14.Base); rocq/r2/Kill_r2_hdr.v is the installed copy.
• rocq/check_kill_r2.log: FAIL, only on theorem_text (no nonhalt yet, as expected).
• args, input, framework, framework_build, forbidden, structure, tm_text and integrity all PASS.
• From Coq Require PArith NArith is accepted.

Round 3 (2026-10-13)

Proved in round 3 (dev file rocq/r3/VS.v, now appended to the kill file as sections 18-22; no axioms)

Counter words and the generic step - ctr Yc := forall n e, IncN e (Yc n) (Yc (n + e)), with the instances ctr_bin and ctr_vfl m. - vfl [] m n = digits m n ++ P :: bin (n / 2^m) is the digit word with the marker P at height m (vfl_nil). - astep: one cs_step on X ++ Yc n from the phase-1 fact XN T0 X e1 (Ps A ++ X1), a clean digit-headed X1, and shiftX of the phase-2 fill landing in X. The new upper value is n + e1 + (val X1 + t) / 2^ndig X1. - Splits of value forms at a cut: - vfl_split_hi: marker above the cut, upper part vfl [] (L - R); - vfl_split_le: marker at or below the cut, upper part bin; - vlow_L: the low part does not see the marker height once it is above the cut.

Lemma VS (one descent step), symbolic - vsok fx r r' off0 Lc: a boolean check, implemented as vsrun (computation) plus vscond (conditions). - It runs the first 4096 carries on the low 8 digits vlow (vh r) Lc 8 (V mod 256). Lc = 5..8 means the marker is in X; Lc = 9 means L ≥ 9. - The rest of the carry phase is residues in Z: t0, t0 mod 2^nd, t0 / 2^nd. The absorption shift is shiftX. - It checks the next form's low part X3 = vlow (vh r') L2 nd3 (V' mod 2^nd3), the λ and d bookkeeping, and three integer identities: vz/256 + e1 + t0/2^nd = vz2/2^nd3 mu + 2^(8-nd) = mu' 2^(8-nd3) alpha + 2^(8-nd) = alpha' 2^(8-nd3) (skipped for the entry rows, fx = true, where off is fixed) - vs_gen: vsok .. = true, off = off0 + 256 g, Ω = 256 w, (L = Lc ≤ 8 or L ≥ 9 = Lc), no truncation (wn + 3 2^(L-1) + 256 ≤ μΩ + α off + wp) and c ≥ 4096 give CS (vfz r k Ω off) (vfz r' k Ω (S off)) - The arithmetic is ar_main, a lemma on plain variables. The machine part is vs_core. - Python prototype: rocq/r3/vs.py, all 12 + 1,280 classes pass. rocq/r3/vs_truth.py cross-checks the tables against concrete closed-system steps (19,269 steps, 0 mismatches). - The tables: - enrows: the entry table of proof.md 6.2, as vrows. - row1 off: entry row for off ≤ 31, else phrow (off mod 8). - en_all : forallb en_ok (upto 12) = true and ph_all : forallb ph_ok (upto 256) = true (5 marker classes each), by vm_compute in about 0.7 s. - Row bounds: rowok, row1_lam. - vs_en, vs_ph: the step for an entry row and for a phase row. - descent: chains the steps, using CSstar (with CSstar_snoc and CSstar_plus). - VF1: for k ≥ 41 and o ≥ 1, CSstar (vfz (row1 20) k (o 2^(k+5)) 20) (VFe k (o 2^(k+5))) - VF2: for v ≥ 12 and S ≥ 2, CSstar (vfz (phrow 1) (v-10) (S 2^v) 17) (VFe (v-10) (S 2^v))

Kill file and check_kill (round 3)

• The kill file is now 2,960 lines.
• The new sections are 18-22, placed after E_low and before the rule table.
• It imports From Coq Require Import ZArith. mid-file (ZArith is on check_kill's allowlist).
• It uses Strategy expand [en_ok ph_ok]. (not a forbidden token).
• Backup of the round-2 file: rocq/r3/Kill_r2_backup.v.
• One coqc of the whole file takes 292 s and 3.5 GB; the round-2 file took 148 s on the same machine today.
• rocq/check_kill_r3.log: FAIL, only on theorem_text (no nonhalt yet, as expected).
• args, input, framework, framework_build, forbidden, structure (8 Requires, including the mid-file ZArith), tm_text and integrity all PASS.

What remains (zone: Lemmas E and P, identification, recursion, Theorem B; then the conveyor)

Lemma E (17 → 20): three steps via cutstep with a concrete low part and a bin/vfl [] upper part. Prototype numbers, with P := 2^(k-3), o = 2q + 1 and b = o 2^k - 2: - 17 → 18 - Zone: S1 :: bin V17, V17 = 32(b+1) + 30 = 256 o P - 2. Split X = S1 :: digits 8 254 = [S1; D0; D1 x7], Y = bin (oP - 1). - Phase 1: xfeed 4000 4096 X = (P :: digits 8 253, 16), so A = 1. - c = 32b + 64 = 256 oP. Phase 2: val X1 + t = 256(oP - 15), so X2 = D0^8 and e2 = oP - 15. Y' = bin (2 o P) = bin (2^(k-2)(2q+1)). - The shift lands in Y. Needs shift_D0s, bin_pow_odd (bin (2^i (2q+1)) = D0^i D1 bin q) and the full shift on X2 ++ Y'. - Result: D0^(k+6) S1 bin q, D = 32b + 17, j = 32b + 18. - 18 → 19 - c = 256 oP + 1. X = D0^8, A = 0, e1 = 16. X2 = [D1; D0 x7], e2 = oP - 16. - Y = digits (k-2) 0 ++ S1 :: bin q receives oP carries. It passes q to S1 :: bin q, which gives s1w q := if q = 0 then [S1] else P :: bin (2q - 1). - The shift lands on digit 0. - Result: S1 D0^(k+4) D1 (s1w q), D = j - 2. One lemma covers q = 0 and q ≥ 1. - 19 → 20 - c = 256 oP. X = S1 :: D0^8, A = 1, X1 = digits 8 255, e1 = 15. X2 = [D0; D1; D0 x6], e2 = oP - 15. - Y = digits (k-3) 2^(k-4) ++ s1w q passes 2q + 1 carries into s1w q, which gives P :: bin (4q) in both cases. - The shift lands on digit 1. - Then show that the result equals vfz (row1 20) k (o 2^(k+5)) 20: vfl [[]; [S1]] (k+4) V20 with V20 = q 2^(k+6) + 2^(k+3).

Lemma P (off' 12 → 17): five steps of the same kind. - 13 → 14 has a wall SP at digit 3 whose shift lands at digit v + 1, above any concrete X. - So it needs a symbolic XN chain: XN_W with a symbolic digits n (2^n - 3) block, plus shiftX (repeat D0 m ++ D1 :: w). That is an XN_digits lemma (the XN analogue of IncN_digits), or a direct IncN proof.

Identification and recursion - Identification: VFe K Om at off_end(K) in phase 4 is off' = 12 of the plant. The plant end (off' 17) is vfz (phrow 1) (v-10) (S 2^v) 17 (algebra on the closed forms). - Class recursion: strong induction on K. - Base E_low (v ≤ 50). - For v > 50: Lemma P, then VF2, then the induction hypothesis at K' = v - 10 < K. - Theorem B for k ≥ 41: E1-E3, then VF1, then E(k). Small classes cover k ≤ 40. - Then forall J, exists Z D, CSreach Z D J, from C0_reach and CSplus_j.

Conveyor, Lemma T and the record invariant (proof.md sections 3-5 and 7): not started. The plan is unchanged from round 1.

Lemma E, started (dev file rocq/r3/E.v, compiles in 6 s against M14.Kill = the round-2 kill file and M14.VS = rocq/r3/VS.v)

• Helper lemmas:
• bin_pow_odd: bin (2^i (2q+1)) = D0^i D1 bin q;
• shift_D0s;
• digits_pow2: digits (S i) (2^i) = D0^i [D1];
• s1w q with IncN_s1w : IncN q (S1 :: bin q) (s1w q);
• odd_half, pj17, pj18;
• cs_step_conv: converts D' and j'.
• E1 (off 17 → 18) is proved: CS (Cst b) (D0^(k+6) S1 bin q, 32b+17, 32b+18) with b = (2q+1)2^k - 2 and k ≥ 41.
• E2 (off 18 → 19) is proved: CS (D0^(k+6) S1 bin q, ..) (S1 D0^(k+4) D1 (s1w q), 32b+17, 32b+19), for q = 0 and q ≥ 1 alike.
• Both use cutstep with a concrete low part. The phase-1 fact comes from xfeed_sound with reflexivity, phase 2 from XN_clean and fill_mod, and the shift is either shiftX_app or shift_D0s + bin_pow_odd (E1, where the shift lands in Y).
• Next:
• E3 (19 → 20). The numbers are in the plan above: X = S1 :: D0^8, X1 = digits 8 255, e1 = 15, X2 = [D0; D1; D0 x6], e2 = oP - 15, Y = digits (k-3) 2^(k-4) ++ s1w q, which passes 2q + 1 carries.
• Then the identification with vfz (row1 20) k (o 2^(k+5)) 20.
• Then move E.v into the kill file. Note: 0 in change .. with 0 is a Sym; write O.

Round 4 (2026-10-13)

Result: the zone part (I) is finished

zone_forever : forall J, 1 <= J -> exists Z D, CSreach Z D J is proved, no axioms. With it, Theorem B for every b (thmB) and the closed-system orbit as a function (CS_next, CSreach_det). Dev files (each compiles in about 3 s on top of M14.Kill): rocq/r4/E.v (section 23), rocq/r4/P.v (sections 24-26), rocq/r4/C.v (sections 27-29). They are appended to the kill file before the rule table (rocq/r4/Kill_r4b.v is the assembled candidate).

Lemma E (section 23). E3 (off 19 -> 20) by cutstep with X = S1 :: D0^8, plus E_id (the off-20 form is vfz (row1 20) k (o 2^(k+5)) 20, via vfl_row20), and LemmaE : CSplus (Cst ((2q+1) 2^k - 2)) (vfz (row1 20) k ((2q+1) 2^(k+5)) 20) for k >= 41.

Lemma P (section 24). Generic helpers that make every plant step a few lines: - IncN_dig_q r v t p v': t carries on digits r v leave v' and pass p, given v + t = v' + 2^r p. - XN_clean_q: the phase-2 fact with an explicit value and pass count. - pstep: one closed-system step from a concrete low part X (phase 1 by xfeed_sound + reflexivity, then the clean rest), the counter Y above it, and a shiftX landing in X. - cs_nodrop: one step with no drop on a zone with a digit at the bottom (used for 13 -> 14, where the wall SP fires and its shift lands at digit v+1 far above any cut; the IncN chain is written by hand with Inc_W3 and IncN_dig_q). - P12 .. P16, LemmaP, P_id (plant end = vfz (phrow 1) (n-7) ((2Q+1) 2^(n+3)) 17), VFe_plant (VFe K Om for 8 | K+9 is the plant start). States are parametrised by n = v-3 and Q with the step number 8 * gP n Q + i, gP n Q = (2Q+1) 2^n - 8; pjg gives pj (8g + i) = pj i.

Recursion and Theorem B (sections 25-26). - EK : 41 <= K -> 1 <= U -> exists b', CSplus (VFe K (U 2^(K+5))) (Cst b'), by lt_wf_ind: v = nu2(K+9) <= 50 is E_low; otherwise plant + VF2 + IH at v - 10 with U' = 32 S. - thmB b : exists b', CSplus (Cst b) (Cst b'): small_classes for k <= 40, LemmaE + VF1 + EK for k >= 41. - all_Cst, CSreach_down, zone_forever.

Conveyor foundation (sections 27-29). - cs_step_det, CSreach_pos, CSreach_det, CS_next (every reached state has its next step; from zone_forever + determinism). - leading_P (every word is Ps a ++ y with notP y), IncN_le. - Pops_wall: f pops through a wall that is not the top wall: Pops ((3f + b)/2) r r' -> Pops f (Ps a ++ wallu b :: r) (Ps (a + (3f+b)/2 - f) ++ wallu (odd (3f+b)) :: r'). - Birth data wb (Z, U0 frame), wsb, wH (U0 walls 0..5 in absorption order 32 20 12 7 3 1 / W W W SP W SP / H 0 0 0 0 0 9; then phase (w-6) mod 8 from proof.md 4 with H = 36, 6, 9 on the last wall of each group) and bracket : 1 <= J -> p(J mod 8) = 43 - 3 b_J + 2 b_(J-1) + s_(J-1) + H_(J-1) (14 cases by vm_compute + period 8).

Pitfalls (round 4)

• From Coq Require Import ZArith mid-file shadows our shift with Coq.ZArith.Zpower.shift for everything after it ("The term repeat uD0 m ++ w has type list unt while it is expected to have type Z"). Fix: import ZArith in the header (From Coq Require Import PArith NArith ZArith.), so our later shift shadows it. Dev files never saw this because they import ZArith before M14.Kill.
• cbn on a goal containing 2 ^ 51 (nat) never returns (unary). Keep big powers symbolic; prove v + 5 <= 2^v from Nat.pow_gt_lin_r instead of comparing with 2^51.
• change A with B silently does nothing when A does not occur syntactically (here [x;y] ++ (u :: d) ++ r vs [x;y] ++ u :: d ++ r), and the next eapply then unifies with the wrong split. Pass the low part X to pstep explicitly or match the exact association.
• Nat.div_unique concludes q = a / b; do not put symmetry before it when the goal already has that shape.
• rewrite digits_snoc' picked the first digits in the goal (on the other side of the equation); give the argument (digits_snoc' n).

Plan for the conveyor (part II), worked out this round

The zone side is now a black box: from any reached CSreach Z D J there is a unique cs_step with fixed point m, A, Y*. What remains is AbsDefined, that is the record invariant of proof.md 7 and its closure. Design:

1. Skip the U0 walls and interval 0 by computation. Run the unit-word dynamics concretely (an executable Pops built on incf, sound by incf_sound) from U0 for about 3 cycles (24 records, 51 carries per cycle), until walls 0..5 are absorbed. Prove those Reach steps and their Pops by vm_compute. From that record on, every live wall has periodic birth data (w >= 6) and every interval is a real cs_step (J >= 1), so interval 0 (33 carries, not a cs_step) never needs a general proof.
2. Shifted frame (+1) so all positions are nat: b' = b + 1, base' = 1 at XC XD XE ZD ZE and 0 at YC YD YE, zone bottom z = 44 + D_J + A.
3. Wall data and positions. R_w = carries received since birth; f_w = (R_w + s_w)/2 firings; position p_w = b'w + f_w; state W iff R_w + s_w odd. Chain: R(w-1) = H_(w-1) + 3 f_w. At a record the youngest wall has R = 0, so every R is a function of the record and J.
4. The word from position p upward, as a relation WdR w p R u (recursion on the wall number w, oldest first): - live w (R < Rabs w): u = Ps (p_w - p) ++ wallu (odd (R + s_w)) :: u' and WdR (w-1) (S p_w) (H_(w-1) + 3 f_w) u'; - absorbed w (R >= Rabs w, with Rabs w = 2(44 + D_(w+1) - b'w) - s_w): u is the zone of interval w+1 seen from p: exists Z D A Y, CSreach Z D (S w) /\ IncN m Z (Ps A ++ Y) /\ notP Y /\ m <= m*_(w+1) /\ u = Ps (44 + D + A - p) ++ Y with m = R - Rabs w. D(w+1) is unique by CSreach_det, so this is a functional description without choice.
5. Cascade lemma (the only real induction): WdR w p R u -> p <= p_w R -> exists u', Inc u u' /\ WdR w p (S R) u', by induction on w. - SP: the head becomes W, nothing above changes (f unchanged). - W, not the absorbing firing: IncN 3 above by the IH (three times), then the shift lands on a P because p_(w-1) grows by at least one per 3 carries (or the wall above is absorbed and is a P). The result is the same word with p_w + 1: Ps (p_w - p) ++ P :: SP :: ... - W at the absorbing firing (w is top, zone count reaches m): 3 x = c + 3 A(m) - m with c = D + pj = 3(44 + D - b'_J) - E_J (this is bracket), so x = 0 exactly at m = m. Before m, x >= 1, because m' <= c + 3 A(m') holds for all m' <= m (induction on m', using minimality and A monotone). The shift is shift Y*, which cs_step provides, and the word becomes Ps (p_w + 1 - p) ++ Z_(J+1) with 44 + D_(J+1) = p_w + 1. - Mod 3: m is a triple boundary, because m = c + 3A ≡ c ≡ -E_J (mod 3), and the boundaries of interval J are the m ≡ -E_J with m >= r.
6. Record step. Pops k U U' comes from k applications of the cascade (3 carries each) plus the pop. The leading P count after 3i carries is at least i, since the youngest wall fires floor((3i + s)/2) >= i times. Then prepend rF t: new walls with R = 0, and the old youngest has R = 3 rk = H (36, 6 or 9). The placement table of proof.md 4 gives the gaps >= 0 (a finite check).
7. Assemble. Inv(t, U) := exists J and the zone data with WdR (youngest) base 0 U. Show Inv for the concrete state after step 1, closure under ReachS, and from it AbsDefined (the Pops of each step exists). Then Lemma nonhalt : ~ halts tm c0. Proof. apply nonhalt_of_abs, AbsDefined_proof. Qed.

Estimate: items 1-7 are about 600-900 lines, roughly one full round.

Update: the conveyor (part II) is done too, and nonhalt is proved

The plan above was implemented the same day, with one change: interval 0 is not skipped by a concrete run. Wall 0's rest is described directly as the counter bin (60 + m) (Zone0), which needs no closed-system step. Print Assumptions nonhalt in the dev chain (M14.Kill + E + P + C + Cv): Closed under the global context. Dev file rocq/r4/Cv.v (sections 30-32, about 620 lines, compiles in 7 s on top of the others).

• Section 30: data and the word relation.
• bq w (birth index + 1, nat), fw w R = (R + s_w)/2, posw = bq + fw, Rab w D = 2(44 + D - bq w) - s_w (the carry count at which wall w is absorbed, with D = D_(w+1)).
• ZoneR J m p u: the zone of interval J after m carries, seen from position p. It holds the CSreach state, IncN m Z (Ps A ++ Y), notP Y, no fixed point below m (nofix), and u = Ps (44 + D + A - p) ++ Y.
• WdR w p R u (Fixpoint on w): either w is absorbed, and u is ZoneR (S w) (R - Rab w D); or w is live, and u is Ps (posw - p) ++ wallu (odd (R + s)) :: u' with u' = WdR (w-1) (S posw) (H_(w-1) + 3 fw), or Zone0 for w = 0.
• Can w R: if w is absorbed, the zone can take one more carry.
• Section 31: cascade : WdR w p R u -> Can w R -> exists u', Inc u u' /\ WdR w p (S R) u', by induction on w.
• Absorbed: zone_carry.
• Live SP: the head becomes W.
• Live W: three IH calls (their Can comes from Can_lt and the key identity m* + Rab w' D = R' + 3 (44 + D1 - bq W - f), which is bracket_nat + cs_step). Then either:
  • absorption (S R = Rab): the zone count is exactly m, IncN_det identifies Y with the step's Y, and the shift is the step's;
  • a move: x >= 1 by below (m' <= c + 3A(m') up to m*) plus nofix, or because the wall above moved (fw_add3).
• Wall 0 against Zone0: f = 10 is the absorption, and bin 93 shifts to Z1.
• Section 32: the record invariant.
• RInv t U := exists Y, 5 <= Y /\ (Y+2) mod 8 = rph t /\ WdR Y (rbase t) 0 U.
• Pops_bottom: k pops through a live youngest wall.
• WdR_push: put a newborn wall below; data from wd and mod8_S'.
• RInv_step for all 8 record types, RInv_U0 (the six U0 walls pushed onto wall 0), Pops_det, Reach_RInv, AbsDefined_proof, and Lemma nonhalt: ~halts tm c0.

Kill file (round 4)

The kill file is now the assembled rocq/r4/Kill_r4c.v (4,407 lines). It is the round-3 file plus sections 23-32 before the rule table, with ZArith moved into the header imports, the structure list in the header extended, the Checked line updated, and the rule table extended. Backup of the round-3 installed file: rocq/r4/Kill_r3_installed_backup.v. check_kill log: rocq/check_kill_r4.log.

Tactic notes (round 4, conveyor)

• WORKED: describe the unit word above a position as a relation (Fixpoint on the wall number with a Prop disjunction absorbed/live). The closed-system state comes from CSreach plus CSreach_det, so no choice is needed for D_J as a function of J.
• WORKED: a one-carry cascade lemma with a Can precondition (only the absorbed zone needs room for the carry). The caller discharges it by the identity m* - m = 3 (remaining firings), which also gives the mod-3 fact for free.
• PITFALL: destruct (Nat.odd ..) eqn:Ho also rewrites hypotheses, so a later rewrite Ho in Eu fails ("Found no subterm"). Use try rewrite.
• PITFALL: f_equal on Ps a ++ Y = Ps b ++ Y leaves Ps a = Ps b, which lia cannot do. Use replace on the count.
• PITFALL: cbn in P on (S Y + 2) mod 8 = S 7 mod 8 unfolds the mod into Nat.divmod. Feed the residue with a lemma and eq_refl instead (mod8_S').
• PITFALL: nth i phb 0 inside %Z still reads 0 as Sym; write 0%Z.

check_kill (round 4): PASS

rocq/check_kill_r4.log: RESULT: PASS -- this is a kill (exit 0). - File sha256 a4144ade7c58e6c1ff15e9f905ed01bb0ec5c945e0ced0acc6cba043e050c65e, 4,422 lines. - Compile 317.9 s. - coqchk -norec passes in 300.9 s. - Print Assumptions nonhalt: closed (0 assumptions). - All checks pass: args, input, framework, framework_build, forbidden, structure (8 Requires, ZArith now in the header), tm_text, theorem_text (line 4343), coq, names, compile, tm_rocq, theorem_rocq, isolation, assumptions, coqchk and integrity.

Next: independent audit and packaging. The submission write-up (submission/proof.md) must pass writeup_lint. The title line of proof.md still says "Rocq formalization not started", which is stale.

Packaging (2026-10-13)

• Fresh check_kill on the unchanged kill file (sha256 a4144ade…): PASS, compile 315.6 s native, coqchk -norec pass 299.9 s, 0 assumptions. Log: rocq/check_kill_submission.log; sanitized copy in submission/check_kill.txt.
• submission/ written (see notes.md ## Kill). No change to the .v.