Machine #12 formalization log (1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF)

Round 1 (2026-10-10)

• Compile helper: rocq/compile.sh file.v (temp dir under the scratchpad, ulimit -v 8e6, one coqc; NATIVE=yes to test native).
• Working file: rocq/tm_part.v (grows into the kill file).
• Design change vs proof.md section 7: no small-step mstep/mrun model and no TL simulation relation. Instead a big-step frame semantics Life x R o (frame of value x on top, right word R): Fin R' = it comes back on top with value 1; Pop c R' = it created c children and its last child finished, popping it. Four constructors (L_fin, L_cf, L_cpf, L_cpp) = proof.md's "frame reading".
• TL (translation) becomes Life_shape: a Pop outcome only depends on the frame value through "enough budget" (z >= c+1), 15 lines by induction on Life. No |S| case analysis needed.
• TM bridge Life_tm: Life x R (Pop c R') -> conf (x::L) R -->+ conf L R' for every L (induction on Life, using push_ok/pop_ok which are R1/R2 instances).
• DONE (compiles, 1.8 s): tR1, tR2, tR3, tR3c (all plain es), conf encoding (lsep/lside/rside), updt (push R-update), push_ok/push0_ok/pop_ok, Life, Life_tm, Ep, Ep_tm, Life_shape, frame_step, U0, U1, U2, ruleS, TRF/TRX0/TRX1 (TR prefix + continuation), Xin0/Xin1, replay (induction on Orb), ruleT, ruleX.
• Concrete rules all close with one search tactic lf (eassumption | L_fin | eapply L_cf/L_cpf/L_cpp with lia and reflexivity side goals, recursive). Symbolic parameters must be written S-headed (S (S b)), not b+2.
• Marker words by absorption indices: mw P from the index list, valid_from s P (odd steps), cnt/ind/cost.
• DONE (same round): list library (rocq/lists_part.v) and the theorem part (rocq/thm_part.v): Core/Inv, stepU, stepS, stepT_nabs, stepT_abs, step_lemma, main : forall Lm, Claim Lm, init (solve_init, 50 steps), nonhalt. The kill file is tm_part.v ++ lists_part.v ++ thm_part.v plus the header and the rule-table comment (874 lines). It compiles in about 3.5 s, and Print Assumptions nonhalt gives Closed under the global context.
• check_kill: PASS (exit 0; compile 4.2 s native, 0 assumptions, coqchk pass 1.3 s, sha256 117e6cd7...). Output is in rocq/check_kill.out.

How the invariant was formalized

• Marker words are given by their absorption-index lists P = [I_1..I_m] (mw P). valid_from s P says each index is odd above the previous one, which is the same as even gaps. α = cnt P n = #{p < n}, [n ∈ P] = ind P n = cnt P (S n) - cnt P n, and cost = 2 + ind.
• Orb Q n W is the orbit with the absorption-law costs built in (O0 / OS with Ep W (cost Q n) W'), so AL never appears as a separate statement.
• Inv P n W uses one predicate Core P k a b Q for both word types: k = n for a T-word T(a, n+α) and k = n+1 for an S-word S(a, n+α-1). Core says Q = Qi ++ Qe, |Qi| + a = b+1+ind P k, every q in Qi has q+2+ind P k <= a, and Sh (k+3) a Qe (filter (k <?) P) (Sh u v = Forall2 (q+u = p+v)). The EXT clauses become exact shifted copies of the unabsorbed indices, and the absorption exception and the merged case aff = -1 are both the + ind P k terms. With this form no case split is needed on aff = -1 or α = m.
• Parity enters through one lemma, parity_in : valid_from s P -> In n P -> n + cnt P n + s odd. It gives "n ∉ P at S-words" and "n+1 ∉ P at non-absorbing T-words" (so Qe >= a-1 there).
• Composition of shifts: sh_compose (filter_lt_app + Sh_filter + filter_filter_lt + Sh_trans) and in_transfer (Sh_in + filter_in) carry inner Core facts to the outer word. These are the same two lemmas in both T cases; only k, k' differ (a-1, n+2 vs a-2, n+1).
• Measure: Claim Lm := forall Q k, k + |Q| <= Lm -> valid Q -> exists W, Orb Q k W /\ (1 <= k -> Inv Q k W), by plain induction on Lm. The inner calls are (Q, a-1) with measure n+m (T) and (Q, a-2) with n+m-1 (X). filter_cnt_len + Sh_len give |Qe| = m - cnt P (S n).
• Top: progress_nonhalt_cond with A = nat * list nat, C (n,W) = conf [] (3::2::W), P (n,W) = Orb [] n W /\ (1 <= n -> Inv [] n W). No determinism lemma is needed, because the step lemma takes the given W.

Pitfalls hit

• R, L, A..F are constructors (dir, states). A hypothesis named R1 shadowed the lemma R1, so the TM rules were renamed tR1/tR2/tR3. match o with Fin R => ... fails ("constructor of dir"), so use W as the pattern variable.
• cbn unfolds Nat.ltb into match; use cbn [filter length] together with cnt_cons_lt/_ge rewrites.
• exists [], [] cannot infer the type: write (@nil nat).
• eapply Sh_eq; [apply Sh_map with (d:=2) | reflexivity | lia] leaves an evar for lia. Prove the Sh fact first as an assert, then [apply Sh_map ...; exact H | reflexivity | lia].
• frame_step takes equalities y' = y - 1, z' = z - c + 1 as premises. Leave those goals open and finish with ; lia after exact H has instantiated the evars.

Kill packaging (2026-10-10)

• Fresh check_kill (human-readable) at 16:25:12Z: PASS, 17/17 checks, compile 4.1 s native, 0 assumptions, coqchk 1.3 s, sha256 117e6cd7... (unchanged). Output: submission/check_kill.txt.
• status.json -> KILLED_NONHALT / done (previous content saved as rocq/status.prev.json).
• submission/: the .v (same sha256), proof.md (built from the working copy by rocq/make_submission_proof.py: header/status lines, §7.1 .v map, §8 gaps 1-2 marked closed), check_kill.txt, README.md, discord.md (not posted).
• notes.md: Status line + ## Kill; STATUS.md: one line; atlas/rocq-notes.md: packaging datapoint.