W7-5 (line 274) formalization log

Round 1 (2026-10-14/15, claude): check_kill PASS

Kill file: 1RB0RD_0LC0RA_1LA1LC_1RE0LF_0RA1RF_1LB---.v (530 lines, 464 sentences, sha256 1dec277e5a7d867f2b1156f9dfd96ec8ca002ea41b77e9091c6007ed3af7dfc7). check_kill: PASS, exit 0: compile 7.9 s (native), coqchk -norec 1.35 s, 0 assumptions (closed). Output: rocq/check_kill_r1.txt.

Route (differs from proof.md section 5)

• Pass lemmas (proof.md section 3): S0, L1, L2, L3, L4, L5, L5e, L6, L7, RA1, RA3 (RA2 = RA3 with j = 0), RE1, RE2. Each is stated with arbitrary context l/r and symbolic exponents, and each closes with plain es: busycoq's use_shift_rule finds the shift rules Ch1-Ch6 by itself (objects of up to 5 cells). All 13 in 7 s. No separate shift-rule lemmas, no word re-cut lemmas.
• Configurations as token lists (w, ts): ts = words left of the head (Dg d0..d3 = P0..P3, Sw = 100), K w ts = lsd (base w) ts {{D}}> 0inf with lsd a fold_left of reversed words.
• The sweep as a function lpass w Lr T (Lr = unread words nearest first, T = processed tail as a list of tX/tS, followed by 1010 0^inf):
• Sw: T := tS :: T (L1);
• Dg d3: T := tX :: rmS T (L2; rmS removes the first tS);
• Dg d0/Dg d2: stop, step up, A-pass (L3/L4 + RA1/RA3);
• Dg d1: stop, rmS T, A-pass (L5 or L5e);
• left end with wall: O1 (L6 + A-pass); without: O2 = L7 + E-pass (RE1*, RE2), result = T minus its first and its last tS, then P3 s s s. The A-pass maps tX to P0. Soundness lpass_sound: induction on Lr; A-pass and E-pass by induction on a length bound with the decomposition T = X^j ++ rest.
• Invariant JL (new, much simpler than the epoch theorem): for every suffix of ts that starts with a digit, and for ts itself, #s >= #(P1,P3) + 2. Stated as JL (rev ts) 0, a fixpoint over the reversed list carrying n = #s - #odd of the part read so far. It implies every sweep is defined (the leftmost consumer always finds an s: #s(T) = pot(suffix) >= 2; O2 needs #s(T) >= 2, the whole-list clause), and it is preserved: the suffix from the stop digit (and every longer suffix) gains >= 1, and everything written right of the stop digit is P0/s ending in s s (or P3 s s s). Validated before coding by rocq/tokmodel.py: 4,000 random J-configurations (sweep defined, J preserved, sweep = TM next D-record) and 3,000 real sweeps from step 108, all pass.
• Start: init : c0 -->* K false [P1; s; s; s] (108 steps, solve_init); JL holds there (3 - 1 = 2).
• nonhalt: multistep_nonhalt + progress_nonhalt_cond with index (w, ts) and condition JL (rev ts) 0.

Tactics that worked / pitfalls

• L and R are constructors of busycoq's dir: a variable named L or R in a match pattern gives Found a constructor of inductive type dir while a constructor of list is expected. Use Lr, Rv.
• Under sym_scope, exists 0, [] reads 0 as a symbol: write exists O, (@nil tt). Open Scope nat_scope before the arithmetic section.
• <[1;0;0] is a parse-time reversed literal ([0;0;1]), so define left words directly as reversed literals (rdw), and exact (Lemma ...) then matches by conversion (no rewriting of lsd ... [Sw] needed).
• rewrite ?length_app in Hn |- * silently did nothing in Hn; use separate rewrite length_app in Hn steps.
• Dev loop: compile the pass lemmas once as Low.v with -R . Dev, iterate on Abs.v (From Dev Require Import Low, 1-2 s per compile), merge by script.

Files

• rocq/Low.v, rocq/Abs.v: the dev pieces (merged into the kill file).
• rocq/tokmodel.py: token-level sweep + invariant J, checked against the TM.
• rocq/cc.sh: one-file compile (memory cap, coqc count check).
• rocq/check_kill_r1.txt: the PASS run.

Open

• The public write-up should describe the .v's route: the invariant JL replaces proof.md section 5 (epoch theorem); sections 3-4 match the .v (lemma names identical, RA2 folded into RA3).
• Line 514 (start F, mirrored) is not covered by this file. A delta file needs phi, flip_halts/perm_halts (as in #7), and an entry run of 792 steps to B(2;7) = 1100 P0 s^7 P3 s^3, which satisfies JL (suffix from P3: 3 - 1 = 2; from P0: 10 - 1 = 9).