/machines/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC/rocq/log.md · raw

Rocq log, #30 `1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC`

Round 1 (2026-10-10)

Done (compiles, 7.9 s native, no Admitted)

Section 1: every finite run of the write-up as one es lemma, symbolic exponents, arbitrary left/right context: LP0, LP0z, LP11, LPC right/left (d=0/1), LP5 right/left, LP6 right pass, W10, RP0/RP1 (FractalBEC's RInc), E1g, E2g left pass (d=0/1), E0, Et1, Et2, Et3, restart (pre-record -> next hub), the six LPT constants. All closed by plain es first try (0.1-0.5 s each).
Section 2: word syntax word (t0..t3, blk d e w, p11 x w, p01 x w, p00 w, p10 w), enc : word -> side (ends in 0inf, so normalisation '10' = '1' etc. is a stream equality), mutually inductive LP w w' d / Phi a b w k y with re-parse constructors LP_eq/Phi_eq (enc w1 = enc w2).
Section 3: sound by Combined Scheme mutual induction: LP -> l <* 011 C> enc w -->+ l <A outp d (enc w'), Phi -> l <* (110)^a 0 (011)^b C> enc w -->+ l <E 01 (001)^k 000 enc y, all l. Compiled first try. D6 is LP_6: right pass, the sub-epoch as Phi in context l <* 0111, W10.
Section 4: epoch_tm : Phi 1 N y k y' -> K N y -->+ K (S k) y', init : c0 -->* K 8 t2 (solve_init, ~330 steps), nonhalt_of_inv P : P 8 t2 -> (forall N y, P N y -> exists k y', Phi 1 N y k y' /\ P (S k) y') -> ~halts tm c0.

Open: everything above Lemma H (the invariant P)

nonhalt = nonhalt_of_inv P for an invariant P carrying write-up section 5 (Lemma D). - Section 5: computable lpf/phif (nat fuel, one fuel unit per bounce/recursion) with model_sound (lpf n w = Some (w',d) -> LP w w' d, phif ... = Some (k,y) -> Phi ...), compiled after 3 small fixes (a subst ate a variable name: use _; eapply LP_eq; [reflexivity|] unifies the re-parse target with itself: give it, apply (LP_eq _ (blk true 0 t2))). - Aliases needed (same tape, other parse): '10'='1', '101' = b(0), '00'='', '001' = a(0), '10 00'='1', '10 00 1' = '10' a(0), and p10 (p10 (p00 t2)) = 101 000 010001 = b(0) z t2. The last one is the only alias the orbit needs beyond the hand list (found by rocq/model2.py, a Python mirror with a generic re-parser: 253 uses up to epoch 599, nothing else). - Validation: vm_compute of the model from K(1,8,t2) gives N = 8,16,18,32,34,45,48,62,68,84, 94,104,... = the TM's left records (data/nest_orbit_epochs.txt), and runs epochs 3..593 (the write-up's whole finite part, N < 14,796) in 0.8 s, ending at epoch 594 with N = 14,819 as in the write-up (D.8). The finite part is computationally free. - Section 6: counter words gw bs s (blocks LSB first + tail stage), ginc (= LP on G, ginc_LP), value gval (ginc_val: +1, tail stays <= 3, exponent-sum/length bookkeeping, absorption only at a bare tail). New, simpler than the write-up's Lemma P: the potential Psi = value + budget + sum of exponents - number of blocks is unchanged by every bounce (also by overflows) and drops by value-1 >= 3 at every E1g. So count_phase: every counting phase from a counter word with budget >= 1 ends in a pre-record (exists k y, Phi a b (gw bs s) k y), by lexicographic induction (Psi, b); the absorbing bounce at t3 is unrolled with the next bounce. Corollary LP6_total: D6 is a total rule on '10' b-block z R, R a counter word. - check_kill --text-only: everything PASS except theorem_text (no nonhalt yet).

Plan for rounds 2-4 (Lemma D)

Reduction already proved: nonhalt_of_inv P needs P 8 t2 and the per-epoch step. 1. Dig w w' n c (n LP steps from w to w' in G, c absorptions) and the bridges - top level: Dig Y (gw bs s) n c -> N >= n - c + 2 -> Phi (1+n) (N-n+c) (gw bs s) k y -> Phi 1 N Y k y (b is non-increasing, so b >= 2 before every bounce iff the final b >= 2); - nested: Dig w w' n c -> Dig (blk false e w) (blk false (e+c) w') (2n) 0 (LP_a / LP_b pairs); - prefix and strip steps: p11 x W -> p10 W in 2x+2 steps, x+1 absorptions; LP5 then LP0. 2. Existence + cost of Dig for ordinary residues p11 x (gw bs s) and the 3 special ones, by recursion over the levels (LP6 uses a strengthened count_phase that also returns the shape of the sub-residue: p11 x' (gw bs' s') with bs' = ginc^j of a suffix of bs, x' <= exponent + 1, or special). Cost bound in the pair-recursive form B(e0::e1::rest) = 2(e0+e1+8) + 2 B(rest) (the write-up's weights 2^floor((q+3)/2)), needs positions-stable exponent lists and a bound on created positions (write-up Lemma C; try a Psi-style potential first). 3. Strengthened counting phase: from gw bs s with budget b to the next residue, with the value bound (write-up D.5: m(W') <= (m + a + ...)/2 at the E2g) and the merged-block exponents (D.3/D.4). 4. Orbit invariant (write-up D.6, (I1)-(I4)) and threshold (D.7). Finite part: use phif (vm_compute) to reach a late epoch and check the invariant there. Because the model is so cheap, a fast-counting phif (n GI steps at once by gval arithmetic) would push the finite part to N ~ 1e7-1e8 and allow cruder analytic constants (slack factor ~5-15 at kappa ~ 20-25).

Round 2 (2026-10-10): `nonhalt` proved

The kill file now has top-level Lemma nonhalt: ~halts tm c0. (1726 lines, 14.6 s with native compile on; Print Assumptions nonhalt in the dev build: "Closed under the global context"). Developed as 5 dev modules importing the round-1 file as a library (scratchpad c30/dev/S7..S11.v, 1-5 s each), then merged.

Changed strategy for Lemma D (simpler than the write-up's D.4/D.6 excess profile)

Flat view of the nested digestion. Every step of the digestion either increments the counter word R of the unconsumed positions (ginc, or inside a sub-epoch GPhi) or consumes its front block; the nesting only scales the cost of a level-j own step by 2^(j-1) (LPs_nest: n inner LP steps = 2n outer steps, absorptions go into the block). Level j works at fronts f >= 2j-2.
Q potential QI Q0 f bs s p : 2^f (gval + 2 qsum(exps) + p) <= Q0 + 3 * 2^(f+|bs|) (p = pending bounces) is kept by every inc (an overflow adds exactly 3*2^P on both sides), every consumption, Et3; and 2^(f+|bs|) <= Q0. So all created positions stay below Ps with Q0 < 2^(Ps+1) (this is the write-up's Lemma C in potential form).
One generic weighted potential Pot v al be ga Ps f l = sum_i v(f+i)(al e_i + be) + ga * sum_{q in [f+|l|,Ps)} v q (future positions prepaid). Pot_ov: an overflow (bump of the last exponent + new 0 block) costs at most (al+be) v(P) and leaves a slack v(P) for a bare-tail absorption. GPhi_pot transports it through a sub-epoch for any (v, al >= 1, be >= 2, ga >= al+be+1) and any level weight U <= v (charges the record k).
Instances: cost Pot w 2 8 11 with w q = 2^((q+1)/2) (Dig_cost: 2^l n <= Pot + 2^l(2x+2) + 13 w(Ps)); merged exponents Pot v 1 3 5 for (u1 = 2 w(l-1), v = w), (u2 = 2^l, v = 2^(q/2)), (u = v = 1) (Dig_mass); Dig_len: 2(l + |bsp|) <= Ps + 3.
Counting phase: GPhi_rel (exponents of the next W are those of the post-digestion word shifted by h+1 >= 1, +1 at most), GPhi_val (2 gval(W') + a <= gval + k + 2), GPhi_rk (a + b <= k + 1).
Invariant Inv k N y: N >= 17705, N >= Nlo k = 2^(k+3) - 8*2^((Pf k+3)/2), and y = 11 a^x z W with |W| <= k, Mw = sum w_q e_q <= Af k, M2 = sum 2^(q+1) e_q <= Bf k, x <= Xf k (or y special). Pf k = max 12 (k+3). Contraction: 2 Mw' <= Mw + 5 Ws(Pf) + 6 w(Pf) + 2 Ws(k') (positions of B_j are >= 2j-2, B_j lands at j-2).
Numerics: N1 (72^k + Bf k < 2^(Pf k + 1)) and N2 (Costf k + 2 <= 17705 or <= Nlo k) by forallb + vm_compute for k <= 11 and a 2-step induction above (recurrences Ws(P+2) = 2Ws(P)+3, w(P+2) = 2w(P), Af(k+2) = 2Af(k)+21, Costf(k+2) + 10(k+3) = 2Costf(k) + 121, Nlo(k+2) = 42^(k+3) - 16*2^((k+6)/2)). Bases at k = 10,11 / 12,13.
Finite part: orbit 100000 691 8 t2 = Some (17713, Y694) by vm_compute (1.3 s), orbit_sound via model_sound
epoch_tm; Inv 10 17713 Y694 by vm_compute. Python bound script: bounds.py (this directory; python3 bounds.py 12 prints Pf/Af/Bf/Xf/Costf/Nlo per kappa).

check_kill (round 2): RESULT: PASS -- this is a kill (exit 0)

sha256 93a493f5531185781ddecc40b40ad3e5cf0c325326b42aa1d2631802611d90c0, 1726 lines, 2012 sentences.
compile 15.0 s (native on), coqchk -norec ok in 67.8 s (VM steps included), Print Assumptions: 0 assumptions (closed).
Not done here (other agents' files): proof.md still states the write-up's own invariant (excess profile, N* = 14,796); the formal proof uses the weighted-mass invariant above with threshold 17,705 (orbit epoch 694). status.json/STATUS.md not touched.

Kill packaging (2026-10-10)

Fresh human-readable check_kill on the audited file (sha256 93a493f5…90c0): PASS, 17/17, compile 15.5 s (native), coqchk -norec 67.7 s, 0 assumptions; 18:30:15-18:31:40 PDT. Copied verbatim to submission/check_kill.txt.
Public write-up: submission_src/build.py (head.md + working proof.md §0-§7 with 17 asserted one-match scrubs + tail.md = new §8 "The formal proof" and §9). §8.3 documents the formal Lemma D route of round 2 (Q potential, Pot, Inv, N1/N2, the κ table from bounds.py 12, the 691-epoch finite part). writeup_lint 0/0. Rebuild: python3 -B rocq/submission_src/build.py proof.md rocq/submission_src submission/proof.md (from the machine dir).
status.json -> KILLED_NONHALT; notes.md ## Kill; STATUS.md line. Not posted anywhere.