Second skeptic review: proof.md §3.8 (INV+(e)) and its use in §3.3–3.5, 2026-10-10

Scope. Revision 3 of proof.md: §3.8 (statement, F1–F3, L6 and its corollary, L5′ with C1–C3, §3.8.3 survival of pairs 1 and 2, §3.8.4 proof of the Theorem, §3.8.5 notes), and the places where §3.3–3.5 rely on it. I did not re-review §0–§2 (the rules) or §3.7 beyond what my own tooling needed.

Stance and tooling. I started from the assumption that the proof is wrong. All code is new and written for this review. It does not use check_proof.py, scripts/ or the first skeptic's code. It lives in /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/m3-skeptic2/, a session scratchpad that may not persist: - lib.py: the TM simulator, the K encoder and parser, the abstract rules transcribed from §2, the accelerated countdown and the INV+(e) checker. - cyc.py: the cycle-pair driver. It checks every §3.8 claim at every event. - gen.py: the adversarial INV+(e) start generator. - counter.py: the pure counter model (L6 and F2 under arbitrary merges). - exh.py and rand_run.py: the sweeps. - validate.py and base.py: tool validation.

Verdict: no fatal or major gap. INV+(e) is inductive, and the Theorem (period) of §3.8.1 holds as stated. - I re-derived every equality and inequality in §3.8 by hand (sketches below), and each one is justified by the text, not just checked. - L6, F2 and the L5′ identities survive exhaustive tests in a pure counter model where any end touch may be a run-out, which is far more adversarial than the machine. - INV+(e) preservation survives: - 1,022,976 exhaustive near-threshold starts (L* = 3–6, regular and T2), each run for 2 chained cycle pairs (2,045,952 cycle pairs in all); - 150,600 random adversarial cycle pairs, with L* up to 600 and Ep blocks drawn to hit every L-slot run-out timing.

Every check passed and no configuration left D. - I found 7 minor items: wording and terminology (m1, m4–m6) and formalization aids for §3.8.1 and §3.8.5 (m2, m3, m7). None affects correctness.

1. Validation of my own tooling

• Abstract rules vs. direct TM simulation: 7,040 random rule instances, 0 mismatches. All 9 rules are covered, with h = 0–7, sizes up to 25 and all three tails. The 4,960 outside-D draws were skipped. Each instance is simulated until the next configuration that parses as K, and that configuration must equal the prediction exactly.
• Accelerated countdown vs. the single-step map: 6,000 random K, 0 mismatches. The plain runs are also maximal: the next step is always a merge or an outside case.
• Base, from the blank tape:
• step 956 is exactly K0 = K(2; (11,11,0); −);
• step 78,710 is exactly K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); −);
• INV+(e) holds there;
• K0 reaches it in 57 macro steps (45 Dec, 3 End, 3 EndLast, 6 Ov), all in D.
• Orbit from the base to L* = 300:
• 541 cycle pairs, 3 X1 slots and 245 L-slot merges, with all §3.8 checks passing;
• min p₁′/(2^(L*′+2) − 1) = 1.000 and min p₂′/2^(L*′) = 2.234;
• min ΔΦ/2^(k−1) = 1.000.
• Sensitivity: the checker rejects all six revision-2 counterexamples of §6.2 in the same way the old review found:
• five have a merge at k = 1 or 2;
• the sixth, K(2; (15,41,0),(8,17,1),(1,9,1); −), stays in D, but INV+(e) fails at its next start. Its p₂ there is 6, which is below 2^(L*) = 8.

2. What was attacked, and the result

2.1 L6 (Φ = steps + V − 2^n never decreases; each merge adds ≥ 2^(k−1))

• Derivation. A merge at k from x = H·2^k + 2^(k−1) gives V′ = 2^(k−1) − 1 + H·2^(k−1) and n′ = n − 1, so ΔΦ = 2^(n−1) − H·2^(k−1). Since x ≤ 2^n − 1, H ≤ 2^(n−k) − 1, and therefore ΔΦ ≥ 2^(k−1). A plain Dec gives ΔΦ = 0. The proof is correct and complete.
• Exhaustive identity check: every n ≤ 18 and every x < 2^n, 524,268 cases. ΔΦ matches the formula, ΔΦ ≥ 2^(k−1) and V′ ≤ x − 1, with 0 failures. The bound is tight in 171 cases.
• L6 by dynamic programming over all merge strategies (any end touch may merge, every n₀ ≤ 10 and V₀ < 2^(n₀)): the minimum D over strategies satisfies D ≥ V₀ − 2^(n₀) + 2^N + m in all 18,444 (n₀, V₀, N) cases. It is tight in 2,101.
• The corollary under arbitrary merges at k ≥ 3 (M = 4–11): a first countdown from 2^M − 2, then either X1 or EndLast plus a countdown from 2^(N₁−1) − 1. Both T1 ≥ 2^(L*′) − 2 (X1) and T1 ≥ 3·2^(L*′−1) − 2 (EndLast) hold, with 0 violations.
• In the machine: every merge in every run had ΔΦ = 2^(n−1) − H·2^(k−1) ≥ 2^(k−1), and the min ratio was exactly 1. D₁ ≥ 2^(N₁) − 2 + m₁ and D₂ ≥ 2^(N_f) − 1 + m₂ held in every slot, and so did p₁′ = 4·T1 + 7.
• No counterexample exists. There is no cycle in which Φ decreases, and no merge that adds less than 2^(k−1).

2.2 The (e2) touch upper bound (F2 and §3.8.3)

• F2 under arbitrary merges. Dynamic programming over all strategies gave 0 violations, both for pairs 1 and 2 with merges at k ≥ 3 (n ≤ 11) and for every pair j with merges at any k (n ≤ 9). This covers both the index-based and the block-based reading.
• Slot maxima. The maximum number of touches over all strategies equals the bound exactly:
• pair 1: 3·2^(M−1) − 2;
• pair 2: 3·2^(M−2) − 1.

So §3.8.3's budget is tight but never exceeded. - The arithmetic of §3.8.3 and §3.8.4 (e2), re-derived: - q₁ᴸ ≥ 11·2^(L*−1) − 4 ≥ (3·2^(L*) − 2) + 1; - q₂ᴸ ≥ 7·2^(L*−2) − 1 ≥ 3·2^(L*−1); - p₂′ = q₁ᴸ − T1 ≥ 5·2^(L*−1) − 2 ≥ 2^(L*+1) ≥ 2^(L*′).

All three hold for L* ≥ 2. Empirically, min p₂′/2^(L*′) = 1.125, which is exactly (5·4 − 2)/16 at L* = 3.

2.3 L5′, C1 and C2 (the explicit potential s_i)

Re-derived: - Plain Dec and EndLast: s does not change. - Merge at k > i: R′ = 2^(k−i) − 1 + H·2^(k−i) + c·2^(n−1−i), which gives 2(p + 1 + R′) − (p + R) = p + 2^(k−i). - Fused block: R_F equals R_(k+1) before the step, and e_F = e_(k+1). - Blocks above k + 1: they shift down with s unchanged, since ⌊V′/2^(i−2)⌋ = ⌊x/2^(i−1)⌋. - End of slot: s = r′, with δ = 1 after Ov and δ = 0 after X1. - L-start values: 9 − 3/2^(M−1) or 8 − 3/2^(M−1) for the head, and r or r − 1 for the other blocks.

Checked with exact rationals at every event of every slot, for L* ≤ 160: the plain-run invariance, the exact merge and fusion increments, the L5′.4 start values, s_end = r′, the A-bound p_i ≥ 2^(e_i) + 1 for non-tail i ≥ 2 before every event, rises > 1 for i ≥ 2, and fusion gains ≥ 2. There were 0 failures.

The threshold argument of §3.8.4 (b) holds, including the after-T2 case. Its margin is larger than claimed: - At the DecMergeTail, k = n and δ = 1, so the boost is > p_i/2^(e_i) + 1/2 > 1.5. - Empirically, min r′ at a regular K′ after a T2 start is 8.0.

2.4 INV+(e) preservation from adversarial starts inside INV+(e)

The generator. Every clause sits at its minimum, or a few units above it. The Ep blocks p_j (j ≥ 3, and the T2 top pair) range over every L-slot run-out timing, p ∈ {2, 4, …, 3·2^e + 2}, plus one survivor. The Eq q_j sit at threshold or threshold + 1, so both parities occur. The far p_L is 1–8 (x = 3–10), or up to 40 in random runs. T2(k) has k = 4–40. T2 starts with L = 2 (L* = 3) are included: INV allows them although they are unreachable.

At each start the checker asserts: - every macro step is a rule (in D); - the E-cycle is [X2,] End, Ov, with exact τ_j, h + 5 = 3·2^(L*+1) − 1 and x as claimed; - the L-start shape, and that every q-block below the x-pair is good; - merges only at k ≥ 3, only good or x ∈ {3, 5} run-outs, and no DecMergeEmpty; - the slot type matches the S2 table (EndLast iff x ≠ 4, X1 iff x = 4); - the pair-1/pair-2 touch bounds; - the L6 inequalities; - the L5′ checks; - p₁′ = 4·T1 + 7, p₂′ = q₁(end), L*′ = M − m ≤ L* + 1, and L*′ ≥ 4 after X1; - all of INV+(e) at K′: h, digits, q_L ≥ 6, k ≥ 4, θ-thresholds, parity, L* ≥ 3, (e1) and (e2).

Every row-type of the far-end table was exercised many times: x = 3, 4, 5 and ≥ 6; X1 slots; cascading DecMergeTails; and up to 16,770 merges in 120 cycle pairs at L* = 200–400.

Minimum margins over all runs:

The tight cases are expected: - (e1) and L6 are tight after a merge-free X1 slot; - (b) is tight after an X1 slot from a threshold regular start, where r′ = r − 1 = 4 = θ′; - the last row confirms §3.8.1's remark that regular starts give p₁ ≥ 3·2^(L*+1) − 1.

2.5 Is each informal step actually justified?

I went through §3.8.3–3.8.4 line by line. Every step follows from the stated lemmas, and none rests on a check alone: - The goodness of the L-start q-blocks comes from INV(c), from the fact that touches preserve p + d, and from X2's non-flipping touch. Merges preserve goodness below the x-pair, because the fused pair takes pair k+1's q and d. - The far-end schedule is F3 plus the explicit touch sequence end, pass, end at the x-pair. DecMergeEmpty is impossible: before EndLast the top pair has q = 1 and d = 0, and is never touched again. - "V = 0 ⇒ every pair below the far pairs has q even ≥ 2" holds because these pairs are good with d = 0. - The pair-1/pair-2 survival argument is not circular. §3.8.3 uses only F2, and L6 is applied afterwards. - (a), (c) and (d) at K′ follow from Ov/X1 mechanics and from the survival argument.

3. Gap list

Not gaps, noted for calibration: - Several INV constants are stronger than needed: q_L ≥ 6, k ≥ 4, and (e1) itself, since p₁ only needs to support (e2) and pair-1 survival. - The after-T2 bound r′ ≥ 5 is loose: 8 is observed. - C3 is informational.

4. Claims attacked that held, with the reason

• L6 and its corollary. The telescoping potential argument is exact, and ΔΦ ≥ 2^(k−1) follows from H ≤ 2^(n−k) − 1. The machine's merges are exactly the counter-model merges, because the rule effects on V and n were validated against the TM.
• F1–F3. F1: every step touches pair 1. F2: V′ ≤ x − 1. F3: the high digits H are unchanged by a merge below them.
• §3.8.3 survival of pairs 1 and 2. The bound q ≥ total touches + 1 gives q ≥ 2 before every touch. That rules out a pass-through with q = 1 and a run-out, and it covers End/EndLast/X1's "q ≥ 2" side conditions. The arithmetic holds for L* ≥ 2.
• (e1) at K′. p₁′ = h + 5 = 4·T1 + 7, because h starts at 2, every Dec-family step and EndLast adds 4, and T1 = D₁ (X1) or D₁ + 1 + D₂ (EndLast). With L6 this gives T1 ≥ 2^(L*′) − 2. L*′ = N₁ after X1, which yields N₁ − 1 pairs plus T2, and L*′ = N_f + 1 ≤ N₁ after Ov.
• (e2) at K′. p₂′ = q₁ at the end (Ov, and X1 with N₁ ≥ 4). The touch budget and L*′ ≤ L* + 1 do the rest.
• (b) at K′. This is L5′ plus C1/C2:
• regular → EndLast slot: σ = 5;
• regular → X1 slot: σ = 4 = θ′;
• T2 → x = 5 slot: the DecMergeTail boost lifts every surviving non-tail block above 5, and the head is ≥ 8.6.

The fused blocks satisfy s_F > s_(k+1). - (c) at K′. Every q-block below the top pair is good with d = 0 at V = 0, so it is even, and Ov/X1 give d = 1. The T2 top pair is the stated exception: even p, d = 0. - (a) and (d) at K′. h = 2, p₁′ ≥ 7, t ≥ 5 ⇒ q_L′ ≥ 6, k = t₀ + 4 ≥ 8. Pairs 1 and 2, the x-pair and the last pair are distinct at X1, so L*′ ≥ 4 there; L*′ ≥ 3 after Ov. - The §3.3–3.5 narrative agrees with §3.8. This covers the τ_j table (L3, both start types), h + 5 = 3·2^(L*+1) − 1, x = p_L + 2 or 5, the S2 table (the m5 constant aside), the head-block values 9 − 3/2^(M−1) and 8 − 3/2^(M−1), the fusion bound r_F ≥ 2(r_a − 3) + r_b (−1 after X1), C3's 2r − 3 / 2r − 4, and the corrected "L*′ ≥ 4 after X1".

5. Reproduce

cd /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/m3-skeptic2
python3 validate.py 1; python3 validate.py 2      # rules vs TM, accel vs single-step
python3 base.py 300                               # base from blank tape + orbit to L*=300
python3 counter.py                                # L6 / F2 / corollary, all merge strategies
python3 exh.py reg 5 3; python3 exh.py T2 6 2; python3 exh.py reg 6 2   # exhaustive boxes
python3 rand_run.py 31 20000 3 20 5               # random chains (seed, N, Lmin, Lmax, chain [, modes, s-check limit])