Skeptic review of proof.md §3.3–3.5 (class invariant INV), 2026-10-10

Reviewer stance: a skeptical busycoq maintainer. All checks use new code written for this review: a direct TM simulator, a K parser, the abstract map transcribed from the §2 table, an accelerated countdown, block-identity tracking and an INV checker. It does not use check_proof.py or scripts/. The code is in /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/m3-skeptic/, which is a session scratchpad and may not persist. Every counterexample below can be replayed by hand from the §2 rule table.

Verdict: the Theorem of §3.3 is false as stated (fatal, repairable). INV is not inductive. Configurations exist that satisfy every clause of INV, yet within one cycle pair they leave D ((o7) L = 0 or (o4) X1 with L ≤ 2), or they break INV(d). The step where this happens is the proof of INV(d), and with it the "k ≥ 3" premise of the fusion bound. Both use lower bounds on the two newest Ep blocks (p_1 and p_2 at the E-start), and those bounds come from earlier cycles; INV does not record them. Everything else I attacked in §3.3–3.5 held: L3, L5, the fusion bound, the head-block bound, the X1/X2 costs, INV(a)/(b)/(c) mechanics, the far-end table and the base case. Adding one clause, (e) below, made INV inductive in every test I ran (1,027,584 exhaustive cases and 70,000 random cycle pairs). Proving that (e) carries over needs one new counter lemma.

Consequence for the Rocq plan (§4): Lemma period: INV K -> exists K', INV K' /\ K -->+ K' cannot be proved with INV as written, because it is false for the K below. The formalizer should switch to INV + (e) now.

Validation of my own tooling (so the findings can be trusted)

• Abstract map vs direct simulation: 0 mismatches. Small sizes: 2,274 in-D instances (all 9 rules; the 726 outside-D cases were skipped). Sizes up to 300: 462 instances.
• Accelerated countdown vs single-step map: 0 mismatches on 20,000 random K.
• Base, from the blank tape:
• Step 956 is K0 = K(2; (11,11,0); −).
• Step 78,710 is K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); −).
• All 101 canonical transitions from step 956 to step 198,415 are predicted. The re-pairings are followed by starts at steps 1845, 4610, 8319, 19436, 34137, 78710 and 137547.
• Real orbit: INV and all lemma checks hold at every E-start up to L* = 300 (560 cycle pairs). Rule counts match proof.md §E: DecMerge 240, DecMergeTail 5, X1 3, X2 3.

Gap list

G1 (FATAL as written; repairable): INV is not inductive. INV(d) and "q_1, q_2 never run out" use history that INV does not carry

Claim attacked: §3.3 Theorem ("If INV holds at an E-start, then every K up to the next E-start is in D, and INV holds again there") and the §3.5 INV(d) paragraph.

Why the argument fails. INV(a) bounds p_1 only by p_1 ≥ 7, and INV puts no lower bound at all on the other Ep blocks (p_j, j ≥ 2). The INV(d) paragraph uses three facts that are not consequences of INV: - q_1 ≥ 11·2^(L*−1) − 4 at the L-start. This needs p_1 ≥ 2^(L*+2) − 1 at the E-start, the value left by the previous slot. - q_2 ≥ 3·2^(L*) − 3. This needs p_2 ≥ 9·2^(L*−2) − 2, which "uses L* ≤ L*_prev + 1", again the previous cycles. - "It is 15·2^(L*−1) − 4 after a regular start". This is exact only when the previous L-slot had no merges.

With small p_1 and p_2, the L-slot's q_1 and/or q_2 run out. That gives merges at k = 1 or 2, which the fusion bound excludes ("k ≥ 3"). The pair list then collapses into the far end.

Concrete counterexamples. Each start satisfies INV(a)–(d), p_1 ≥ 7 and non-empty blocks; my checker reports no violation. 1. (o7). Start: K(2; (7,19,0),(2,10,1),(1,6,1); −). Here L* = 3, r_1 = 20/4 = 5, r_2 = 10/2 = 5, p_1 = 7 is odd with d = 0, and p_2 = 2 with d = 1. - E-cycle: 6 Dec, End, 3 Dec, Ov. The L-start is K(2; (47,16,0),(9,7,1),(5,3,1),(4,2,1); −), with x = 3. - L-slot: after 10 Dec, the x = 3 pair runs out (DecMerge at k = 3, as the table predicts). After 1 more Dec, pair 2's q runs out (DecMerge at k = 2); it was 7 at the L-start, but the INV(d) paragraph claims q_2 ≥ 3·2^3 − 3 = 21. After 1 more Dec, EndLast fires with L = 1, leaving K(62; (62,1,1); T1(37)). - Pair 1's q runs out next (DecMergeTail), leaving K(66; −; T1(102)). This is L = 0, (o7), outside D. 2. (o4). Start: K(2; (7,39,0),(2,20,1),(2,10,1),(2,6,1); −). Here L* = 4 and r = 5, 5, 5. - The L-start is (95,28,0),(17,13,1),(9,7,1),(5,4,1),(4,2,1), with x = 4. - After 24 Dec: DecMerge at k = 2 (pair 2's q, 13 at the L-start), then 1 Dec, then DecMerge at k = 2 again, then DecMerge at k = 1 (pair 1's q). This leaves K(114; (183,1,0),(5,1,0); −): the X1 shape with L = 2, (o4), outside D. 3. INV(d) breaks at a T2 start. Start: K(2; (7,15,0),(8,8,0); T2(4)). - E-cycle: X2, End, Ov. L-slot: EndLast, DecMerge, DecMergeTail, Ov. - The next start is K(2; (83,80,0),(2,18,1); −), which has L* = 2. 4. Not a small-L artifact. Take the all-at-threshold INV configuration with L* = 20: p = (7,2,…,2,1), q = (5·2^19 − 1, 5·2^18, …, 10, 6). One cycle pair later it is at L = 0, (o7). Across 3,000 random INV starts with L* in 20–60, all 984 at-threshold starts went outside D. The random ones survived, but only because a random p_1 is huge.

Scale of the failure under literal INV.

Not a halting witness. None of these starts is reachable: on the orbit, p_1 ≥ 5.94·2^(L*) at regular starts and p_1 ≥ 3.999·2^(L*) at T2 starts. The machine also runs on through both outside configurations above: - the (o4) one reaches K(2; (119,182,0),(3,8,1); −) after 6,445 steps; - the (o7) one reaches K(2; (71,102,0); −) after 3,641 steps.

This is a gap in the proof, not in the machine.

Repair (tested, not proved). Add a clause (e) to INV that records the newest Ep blocks. - (e1) p_1 ≥ 2^(L*+2) − 1. This is the T2-start value; it is tight after a merge-free X1 slot. - (e2) p_2 ≥ 2^(L*).

Why this is enough: - (e1) gives q_1 ≥ 11·2^(L*−1) − 4 > 3·2^(L*) − 2, so pair 1 survives. - (e2) gives q_2 ≥ 7·2^(L*−2) − 1 > 3·2^(L*−1) − 1, so pair 2 survives. - From these, INV(d) and the "k ≥ 3" premise follow exactly as §3.5 argues.

Preservation: - (e2) follows from (e1), from "pair-1 touches in an L-slot ≤ 3·2^(L*) − 2" (merges only lower the counter), and from L*' ≤ L* + 1. The algebra is p_2' = p_1 + τ_1 − 1 − T1 ≥ 5·2^(L*−1) − 2 ≥ 2^(L*+1). - (e1) needs a new lemma: an L-slot that ends with L*' must touch pair 1 at least 2^(L*') − 2 times, because p_1' = 4·T1 + 7. A potential-function argument should work: each merge at k costs H·2^(k−1) < 2^(c−1) decrements and removes one pair. It is not in proof.md and must be written. - Alternative: the text's own numbers also work: p_1 ≥ 3·2^(L*+1) − 1 at regular starts (2^(L*+2) − 1 at T2 starts), and p_2 ≥ 9·2^(L*−2) − 2. Both are exactly tight at the base: 95 = 3·2^5 − 1 and 34 = 9·4 − 2. This version also passed 10,000 random starts.

Evidence that INV + (e1) + (e2) is inductive: - Exhaustive: the same four boxes as above, with p_1 and p_2 raised to their (e) minima. All 1,027,584 cases are in D and satisfy INV + (e) at the next start. - Random single cycle pairs: 20,000 (L* = 3–14). The "text numbers" variant passed a separate 10,000. - Random chains: 3,000 × 6 cycle pairs (L* ≤ 14) and 4,000 × 8 cycle pairs (L* ≤ 40). All chains completed, with no outside case and no INV or (e) failure. - Margins: at later starts, min p_1/(2^(L*+2) − 1) = 1.000 (tight) and min p_2/2^(L*) = 1.125. - Both clauses are needed. With only one of (e1)/(e2), or with the bare "survival" bounds p_1 ≥ 3·2^(L*−1) + 2 and p_2 ≥ 3·2^(L*−2) + 1, the invariant fails within one cycle pair. Example: from K(2; (15,41,0),(8,17,1),(1,9,1); −), the next start has p_2 = 6 < 3·2^1 + 1.

G2 (minor): "After X1 the bound is L* = M ≥ 4" is false when the X1 slot has interior merges

• Counterexample: in INV+(e) chains, 111 of 127 X1 slots had L*' < M. One example has M = 14 and L*' = 8, after 6 interior DecMerges. It starts from K(2; (32767,20479,0),(19630,10240,1),(2,6340,1),…,(2,44,1); −).
• What is true: L*' ≥ 4. Pairs 1 and 2 survive under (e), and the x-pair and the last pair are both present at X1. Reword the sentence.

G3 (minor): L5's corollary "with ≥ 1 merge, r' ≥ 2r − 3" does not follow from L5 in an X1 slot

• Derivation gap: in an X1 slot, L5 gives base r − 1 plus A/2^e ≥ r − 3, which is only 2r − 4.
• It still holds empirically: min margin over 2r − 3 is 0.51, over 22,379 + 104,312 merge cases including X1 slots. The reason is that an Ep block can run out only after at least 3·2^(e_k) touches, which is late in the countdown, so A has already grown.
• Not load-bearing: the T2-start threshold needs only r − 1 ≥ 4. Either state 2r − 4 for X1 slots or add the "Ep run-outs are late" remark.

G4 (minor, for the formalizer): L5's "remaining touches in a merge-free continuation" needs a definition

• The problem: in x = 3 and x = 5 slots, every real continuation contains a far-end merge.
• The definition that works: R := ⌊V/2^(i−1)⌋ + 2^(N−i) for EndLast-type slots and R := ⌊V/2^(i−1)⌋ for X1-type slots, where N is the current pair count. Depth is N − i before EndLast and N + 1 − i after it.
• Checks: with this R, I re-derived R' − R/2 = (a − 1)/2 ≥ 0 for a first-countdown DecMerge (a = 2^(k−i)). The EndLast-plus-second-countdown part halves exactly. A DecMergeTail has H = 0, so R' = R.

Claims attacked that held (with the reason)

• L1, merge effect on the counter. Algebra: pairs to the right keep ⌊(x−1)/2^(j−1)⌋ = ⌊H/2^m⌋ remaining touches, the fused pair inherits pair k+1's H, and pairs to the left lose H·2^(k−j). Exact in 20,000 accelerated-vs-stepwise comparisons.
• L3, exact τ_j in E-cycles (both regular and T2 starts). Every interior Eq block in every tracked cycle pair (orbit and random) lost exactly 3·2^e − 1 (pair 1: 3·2^e − 2). No E-cycle ever merged.
• L5 and persisting Eq blocks. Merge-free EndLast slot: r' = r exactly (min = max = 0 over 244,115 cases). X1 slot: r' = r − 1. With merges to the right: r' ≥ r always.
• Fusion lower bound r_F ≥ 2(r_a − 3) + r_b (−1 after X1). Min margin +3.00 over 14,053 fusions; nested fusions had margin ≥ 26.5. Under literal INV, fusions with the current head block (k = 1) also stayed far above threshold. The fusion bound is not where G1 bites.
• New head block. r_1 = 9 − 3/2^(M−1) (EndLast slot) or 8 − 3/2^(M−1) (X1 slot) exactly when merge-free, and never lower.
• X1/X2 cycle pair. The T2 countdown never touches the top pair. X2 and End always apply. x = 5 after every T2 start, and the following slot always has a DecMergeTail. k = p_M + 3 ≥ 8 (the text's "p_M ≥ 2" is weaker but true). The X1 slot costs exactly 2^e in scaled value, i.e. r' = r − 1.
• Far-end table (x = 3, 4, 5, ≥ 6). Exercised 1,866 / 1,013 / 3,636 / 25,485 times in the (e) chains, with no outside case. x = p_L + 2 ≥ 3 follows from blocks never being empty.
• INV(c). Every interior p-block at the next start is the new head block or one of the L-slot's q_1..q_{M−2}. No x-block, tail block or Eq block ever became an interior p-block. Every L-slot run-out was an interior Ep block or the x-pair.
• INV(a). Shape, h = 2, digits, q_L ≥ 6 and k ≥ 4 held in every case that stayed in D.
• Base case. Step 78,710 is as stated, and INV(a)–(d) hold there: r = 8.625, 8.25, 7.5 and L* = 4. The proposed (e) also holds there, tightly: p_1 = 95 and p_2 = 34. Every transition from K0 is rule-predicted.