Rocq log, machine #8 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB

Round 1 (2026-10-10)

Approach: token view (proof.md §0). Right of the lead the tape is a word over T0 = 00, T1 = 01, TZ = 100. Processed tokens on the left are P = (10) and PZ = (010). - Window lemmas AT0, CT1, CTZ, CT0, EPZ, EP, FP, FPZP (= UF), ENDl, B1, BN, ENDZX: all es, under 1 s in total. - Csweep: C passes any T1/TZ word (induction). - retf: the leftward E/F return as a total function on processed tokens, with soundness retf_spec (induction on length, because the UF rule eats two tokens). - Counter ctr gs v: digits b Z 1 Z^g, LSB first; the last digit is its bit only, so the digits above the carry are never read. IncC (C sweep + carry + return) and IncL (A> T0 Z^a ... -> <F T0 Z^a ...) compile. - Observation: T(f) depends only on the position of the first 0 bit of the tail (the return rewrites a word of processed 1s and Zs). So the 16,384-entry table reduces to 14 + 2 concrete retf computations; no table in Rocq is needed.

Proven this round (rocq/T1.v, compiles, 0 admits, native off for speed)

• Window lemmas: AT0, CT1, CTZ, CT0, EPZ, EP, FP, FPZP, ENDl, B1, BN, ENDZX (all es).
• Csweep: C passes any T0-free token word (induction).
• retf + retf_spec: the leftward E/F return as a total function on processed tokens, proved sound by induction on length ps (the UF/FPZP rule eats two processed tokens, so structural induction on ps directly does not go through; induction on a length bound does).
• Counter ctr gs v (digits b Z 1 Z^g, LSB first, last digit = its bit), with ctr_even/odd, ctr_hd_even.
• IncC (C-sweep carry, induction on gs) and IncL (A-entry carry: A> 00 Z^a D(v) -> <F 00 Z^a D(v+1)).
• Bnc (left bounce: 0inf <F 00 100 X -> 0inf A> 00 100 100 X) via es+const_unfold.
• Inc (normal-mode increment, IR->IR): 0inf A> 00 100^(S a) D(v) -> 0inf A> 00 100^(S(S a)) D(v+1), for S v < 2^(S (length gs)). Lead a -> a+1, value v -> v+1. This is proof.md rule Inc.
• OvRet (the overflow return, the crux): for any T0-free w, A> 00 (tw w) 00 (tw rest) -->* <retf E (prc w ++ [P]) (T1 :: rest)>. C sweeps the all-ones body to the first 0 of the tail, turns (CT0), and the leftward return is the finite automaton retf. This removes proof.md section 9's 16,384-entry T(f) table from the Rocq plan: the tail answer is retf applied to the processed prefix up to the first tail 0; no per-f case table is needed, and retf_spec makes it sound against TM.step for every tail.

Key reductions / lessons

• T(f) table (16,384 entries) is unnecessary: the return is retf, a 4-rule token transducer (E/PZ->TZ, E/P->T0 flip to F, F/P->T1 flip to E, F/PZ/P with a 0 ahead -> FPZP two-token eat). tail_ret in rocq/py/tok.py matches the real per-first-zero-position behavior for all 14 slot positions + the 5 ENDCARRY growth cases.
• retf_spec needs induction on a nat length bound, not structural induction on the token list, because FPZP consumes two processed tokens at once.
• follow Bnc then finish: the first token-peeling rewrite block already normalises the RHS too, so the A-form target closes by reflexivity.
• Tokenisation convention: right of the lead the tape is a word over T0=00, T1=01, TZ=100; processed tokens are P=(10), PZ=(010). (001)^a 00 = 00 (100)^a so the normal lead reads as T0::TZ^a.

NOT yet done (for rounds 2-4)

• Pause rules P100/WX/P010/ZX/ZXN/ZXP (follow chains of IncL/B1/IncL/END-family, in pause-mode wall context (100)^n 1). The window lemmas BN/ENDZX are already proven.
• The boundary step after OvRet: deciding N vs S from the final retf mode (F->N via BN, E->S via BS), and building NO/PO/SILENT/SILENTP. Needs a BS lemma (not yet stated) and the re-tokenisation of the processed gap-2 digit (proof.md 4.3).
• The forward overflow sweep framing: pin w = all-ones counter body (ctr gs (2^N-1) is all T1/TZ, noT0) + R-block + tail-ones-prefix; feed to OvRet. Need noT0 (ctr gs (2^N-1) ...).
• Macro invariant INV (M, s, kappa, f) and the 4 paths S/P1/P1S/P3 (proof.md section 5): the linear interval arithmetic. This is the bulk of the remaining work.
• init (92,299 steps, esx from c0) + nonhalt via progress_nonhalt_cond with P = INV.

Round 2 (2026-10-10)

Working file: rocq/T2.v (T1.v + new sections). Compiles, 0 admits, ~2.7 s native off. - Pause rules as generic wall lemmas: TwoInc (= P100, P010, WX, ZXP1: IncL, B1, IncL, END), ZXg (= ZX, ZXN: IncL, B1, IncL, ENDZX), ZXP2g (IncL, BN). Walls are left streams L <* [0] <* [1;0] etc., so each concrete wall shape is just a choice of L. - Tail layer done (proof.md 4.2 + 4.4 without any table): tailw/tailx (15 named bools + end-unit list), Lst y z S (L as a stream predicate), TailRet (C-sweep to the first 0 + retf), Tail10 (10 -> E, front 01), Tail0z (0z -> F, front 1z after the x flip), Tail11 (13 first-zero leaves generated by rocq/py/gen_tail_v.py, + Tail11_end = ENDCARRY by e_split + parity: retf_PP/retf_PPP + the two 31-token returns F1E_ret/F1F_ret). Each leaf is one exact (TailRet PRE REST m OUT I eq_refl l (const 0)) closed by conversion. - retf_app (composition when the first part is fully consumed), RB lemmas RB_E2/RB_F2/RB_E1/RB_F1, shift4, digit/counter views dig, LD, ctr_ones, ctr_zero, body_ones, body_zero. - Overflow core done: OvN1 (H=1, tail returns E -> N, H'=0), OvN0 (H=0, tail returns F -> N, H'=1, r1+1), OvS1 (H=1, tail returns F -> S). Stated for any left context l, so they serve both NO/SILENT (l = 0inf) and PO/SILENTP (l = pause wall after B1). - Lessons: busycoq's LibTactics exists takes at most ~6 comma/space args: chain exists a; exists b. Number literals default to sym scope in this file: write O, 1%nat. Don't name a stream S. follow (H _) with an evar fails ("Cannot infer placeholder"): use eapply evstep_trans; [apply H|]. For final stream equalities, assert tw L1 *> S = tw L2 *> S' and prove it with change ([0;1] *> S0) with (tw [T1] *> S0); rewrite <- Str_app_assoc, <- tw_app; f_equal; f_equal then list algebra (cbn [app] before rewrite <- !app_assoc to push conses). - Macro layer (same round): KP W p gs v H St = one IR shape for normal (W = 0inf) and pause mode. P100s, WX, Incs, P010s, Zone/Zones (zone list innermost first; value map zv, gaps zg, lead zp; the no-overflow side condition is only on the FINAL value, propagated back by zv_ge: 2^|L| * v <= zv L v), ZXN, ZXP (= ZXP1 + ZXP2), wall algebra wallOv, wallPO, zw_LD_gen. NOrb, POrb, SILENT, SILENTP take the tail behaviour as abstract hypotheses OvNp/OvSp (instances OvNp1, OvNp0, OvSp1 from OvN1/OvN0/OvS1). - Paths: pathS, pre1 (NO e0 + pause + PO#1 e1, shared), pathP1, pathP1S, pathP3, with Q = 2^(length G + r1), M = 4Q, gval G + 6 + kappa = Q (= the write-up's c = M/4 + kappa). INV needs only gaps >= 2 (not >= 7) for the rules. step: INV closed (case split by front unit, Tail11's two answers, and the s-interval). init: solve_init to KX 121 [28] 5 St0 (92,299 steps; checked first by a Python sim). nonhalt via multistep_nonhalt + progress_nonhalt_cond. - RESULT: Print Assumptions nonhalt: Closed under the global context. T2.v ~1180 lines, compiles in ~9.5 s (native off), max RSS ~530 MB. Kill file assembled from T2.v. - Progress (-->+): AT0p (es on a -->+ goal) makes OvSweep, OvN/OvS1, NOrb and SILENT strict; POrb/SILENTP use progress_evstep to drop back to -->. - Arithmetic lessons: keep set (G' := ...) opaque in lia goals (unfolding it in the goal breaks the link to gval G' = ... facts; give length G' = S (length G) by reflexivity instead); rewrite !Nat.add_succ_l, !Nat.pow_succ_r', !pS normalises 2^(length (g::G) + S r) to 4 * 2^(length G + r). KP_eq (p = p' -> v = v' -> KP .. = KP ..) + lia matches lemma outputs to the next lemma's inputs. fw H := eapply evstep_trans; [exact H|] (exact = conversion) is needed whenever wall lists differ only by reduction of concrete prefixes / lpow (S n). - check_kill PASS* (2026-10-10 23:03Z, tool_version 4): kill file sha256 0ddf7487...a879a1, 1327 lines / 1613 sentences, compile 10.2 s native on, coqchk -norec pass in 3.2 s, 0 assumptions ("Closed under the global context"), framework HEAD 0940bb9. The kill file = header + rocq/T2.v (minus its Print Assumptions) + rule-table comment.