D-006 — §7 sharpness/ceiling + conditional extensions + Lean (App. A)

Date: 2026-08-17 | Session: 001 | Task: 0.2e | Status: complete Source: fulltext pp. 12–17. This completes the 0.2 sub-stage series.

1. §7.1 — Position vs. prior work (map)

• [Ary22]/[BGSTB24]: unconditional Fejér-kernel sum over zero differences = (4/3+o(1))(T/2π)log T — the zero-side reading of our ‖G̃‖²_HS.
• [GS25 Thm 2]: unconditional bound on the diagonal (γ=γ′) sum with constant C < 2 would give ≥ 2−C simple/on-line; C = 4/3 needs discarding γ≠γ′ terms = termwise positivity that FAILS off the line. [BGSTB25, GS26] achieve it under "all zeros within o(1/log T) of the line".
• Theorem A = unconditional substitute reaching their 2−C = 2/3: instead of isolating the horizontal diagonal termwise, Lemma 3.2 bounds the rank from tr, ‖·‖_HS, and positive index. 5/6 = (3−C)/2 = average of simple and critical proportions [GS25 Thm 3(ii)] = RH-conditional [CGG98,(1.2)].
• Bombieri [Bom00]: negative index of truncated Weil form = #off-line pairs seen. Yoshida [Yos92]: positivity of W on small support. No prior use of positive index/rank + second moment together.

2. §7.2 — Sharpness and limits (THE ceiling analysis)

(a) Dimension. rank P, n₊(G̃) ≤ d = N(1+o(1)): trivial ceiling 100%. X ≤ T restriction is from Prop 5.4 (off-diagonal primes). X ≫ T needs Hardy–Littlewood prime-pair info ⟺ Montgomery pair correlation for support > 1 [Mon73, GM87]. Extreme configuration test: all zeros off-line pairs ⟹ rank P = 0, n₊(Q) ≤ N/2, Lemma 3.2 forces ‖G̃‖² ≥ 2N > (4/3)N — contradiction with (P) only shows ≥ 2/3 are not of this kind. Nothing in the method distinguishes "two thirds" from "all". [This is the precise statement of the wall.]

(b) Sharpness of the three counts. Given only tr, ‖·‖²_HS, block structure, tr P₁ ≤ s₁: §6 inequalities are SHARP. Extremal: (2/3)N mutually orthogonal simple on-line + (1/6)N on-line doubles realizes tr = N, ‖·‖² = (4/3)N, s₁ = (2/3)N, N_d = (5/6)N — Montgomery's RH extremal. Off-line pairs of depth → 0 are spectrally identical; there Thm A(i) is exact (2/3) and A(ii) is not sharp (N_d = N). ⟹ Improving the constants with this exact data set is impossible (formal sense).

(c) Two levels of integrality. (P,Q) decomposition recovers (m−1)² ≥ 0; (P₁,Q′) regrouping recovers (m−1)(m−2) ≥ 0. Interacting simple zeros (eigenvalues in (0,2)) are harmless on the rank side; multiple on-line points and off-line pairs sit on the index side at flat charge 4. = [CGG98,(1.2)] made unconditional.

(d) CMS connection. Lemma 3.2 is the m=1 case of the one-sided Chebyshev–Markov–Stieltjes bound: knowing moments d⁻¹tr G̃ᵏ for k ≤ 2m, the sharp lower bound for n₊(G̃)/d is 1 − Λ_m(0), Λ_m = Christoffel function of the moment sequence at 0. ⟹ The natural upgrade path is MOMENTS, and the upgrade is quantified by Christoffel functions.

(e) Rudnick–Sarnak wall. Prime-side evaluation of tr G̃ᵏ by the diagonal method works exactly when Xᵏ ≤ T^{2−ε} [RS96]. At X ≍ T: only k = 1,2 (tr G̃ and ‖G̃‖² = tr G̃²). Unconditionally, higher moments add nothing. [Confirmed: this is why the certificate is a 2-moment object.]

(f) Conditional ladder HL*(k₀). Hypothesis: tr G̃ᵏ = d·m_k(1)(1+o(1)) for k ≤ k₀, where m_k(1) = k-th moment of the limiting spectral distribution of the sine-kernel Gram matrix over the sine process. (k=4 encodes Hardy–Littlewood-type additive correlations Σ_m(Λ∗Λ)(m)(Λ∗Λ)(m+h), |h| ≤ X²/T.) Computed: m_k(1) = 1, 4/3, 2, 13/4 (k ≤ 4); Λ₂(0;1) = 5/36. HL(4) ⟹ N^s_0/N ≥ 13/18 = 0.7222. HL(∞) ⟹ 100% simple on line — the ceiling of (a). RH itself is out of reach of the mechanism. Complementary to [GLSS25]: full-support pair correlation conjecture ⟹ 100% simple zeros on the line. [Verify later (Phase 1): m_k sequence and 13/18 computation — reproduction target 1.3; the moment sequence 1, 4/3, 2, 13/4 looks like it comes from a specific density — identify it: candidate ρ(x) = (2/π)√... or Marčenko– Pastur-like. NUMERICALLY CHECKABLE. → logged as open thread.]

The bandwidth-one ceiling (≈ 0.682, partially Lean-verified). Definition: a bandwidth-one certificate p depends on the zero configuration only through its first two trace moments against test functions of Fourier support in [−1,1] + the on-line/off-line partition, and satisfies p ≤ N^s_0/N configuration-wise. Thm A(i)'s certificate is of this kind. Lean theorem Zeta23.PairCeiling.ceiling_law256: for any such p and any window r of Fourier support in [−1,1], c₀ + ∫₀¹ r(x)x dx ≤ p + 0.824|r(1)| + 2.55×10⁻⁶(|r′(1)| + ∫₀¹|r″|) under hypotheses h_valid (sampled form factor S_j of the explicit 256-periodic law, Zeta23/PairCeiling/LawN256.lean — optimum of the finite program) and EnclOK (form-factor enclosures). p₀ := 1 − a_N ≤ 0.6818287 (exact rational, rounded up). Band-limited windows have r(±1) = 0 ⟹ 0.824-term vanishes ⟹ bound p₀ + 2.55×10⁻⁶(|r′(1)| + ∫|r″|) < 0.6819 for |r′(1)| + ∫|r″| < 8.2 (both windows (2.6) qualify). Audit caveat: at tag v1.0 the enclosures EnclOK are certified by INTERVAL ARITHMETIC, not the Lean kernel. Kernel-checked (given EnclOK): 255 near-CUE row inequalities |256S(j) − j| ≤ 3×10⁻⁴⁰, edge bound |D(1)| ≤ 0.82395317 and its sign, analytic stability inequality. This is the ONLY numerical certification in the paper; Theorems A/B are independent of it (3 standard axioms only). ⟹ Theorem A is within 0.016 of the ceiling of its own method class. Beating 0.682 provably requires leaving bandwidth one (support > 1 form-factor input) or using ≥ 3 moments.

3. §7.3 — Conditional extensions (roadmap material)

Under RH, tr G̃³ available [Hej94, RS96]. Cubic weight ω(m) = ½m + (1/18)(2m² − m³) + (4/9)·1_{m=1} (tight at m = 1,2,3; Schur–Horn + convex minorant of −x²/9 + x³/18); window cos(8s/5)1_{|s|≤1/2}

• [BHB13] N^s/N ≥ 19/27 (RH) ⟹ N_d/N ≥ 0.85082 (cf. 0.8477 [CGdL20] RH). If Montgomery's form factor were known on support (−λ₀,λ₀) for ALL λ₀: method certifies 100% simple zeros on the line.

4. Remark 7.1 — Zeros of ξ′ (unconditional, new)

Same argument applied to ξ′: N^s_{0,ξ′}/N_{ξ′} ≥ 0.85838 (flat window); 0.86864 with quartic window v(s) = 1 − (7/100)(2s)² − (51/200)(2s)⁴; distinct: 0.92919 / 0.93432. Comparators: Conrey 79.874% (uncond.); FGL14 85.84% (RH); CGdL20 0.8825/0.9412 (RH). Wu [Wu15] 0.86957 on-line (not simple, uncond.) — NOT exceeded; the new content is SIMPLICITY. Flat-window 85.838% = FGL's RH-constant with RH removed. Lean: Zeta23.XiPrime.*.

5. Appendix A — Lean formalisation (facts for task 0.5)

Toolchain v4.33.0-rc2; Mathlib 51e6992efd06; repo tag v1.0; github.com/anthropics/zeta-23-lean. Counting functions defined directly against Mathlib's riemannZeta (Zeta23/Statement.lean). Main theorems carry NO hypotheses: two_thirds_on_critical_line, thmB_0_mult (2/3 simple on-line), thmC_0_mult (5/6 distinct), Montgomery–Taylor variants with cMT := √2 tan(1/√2)/(1 + (1/√2)tan(1/√2)), Theorem B analogues, comparator/ directory restating against Mathlib alone. Audit: no axiom declarations beyond Mathlib's; #print axioms on all main declarations ⟹ only propext, Classical.choice, Quot.sound; no sorry. Contributed to Mathlib: von Neumann trace inequality (Hermitian), both directions of Sylvester's law of inertia (Hermitian forms). Analytic inputs (§2) appear as theorems in their own right; several ported with attribution from PrimeNumberTheoremAnd [PNT+].

6. SYNTHESIS — the obstruction map, now mechanistic (Phase 1 input)

Open threads logged to STATE.md:

• T1: reproduce m_k(1) = 1,4/3,2,13/4 + Λ₂(0;1) = 5/36 numerically (identify the limiting density) — feeds Phase 1 task 1.3.
• T2: Christoffel/CMS formulation (§7.2d) — is there a weighted/variant CMS bound using tr G̃² differently? (task 1.1 material)
• T3: the 0.824 edge constant / finite program LawN256 — understand the 256-periodic law construction before attempting to beat 0.682.
• T4: ξ′-analogue (Remark 7.1) — the method is stronger on ξ′; do our Track A ideas also transfer there? (cheap secondary target)