mirrormere: the full prime-free window (2L <= log 2) proved kernel-native, hypothesis-free, no Arb seam (draft; includes #606; grant after #607)

[DrMurphyIsIn]

Summary

conjecture1_proved = False. This is Weil positivity on one finite window, not RH.

RvMBridge31.PrimeFreeWindowPositivity (E6Bridge31 on main) is proved with no hypotheses. The statement: for every Weil test g with support in [-L, L] and 2L <= log 2, Re weilForm (autocorr g) >= 0. The test class is the goal node's own, with the pole terms kept. The proof also gives the quantitative floor WindowFloor(log 2/2, 9/10000). There is no Arb seam: nothing of ReducedHeadFloor type, and no enclosure hypothesis anywhere in the closure.

• Why it is not Connes-Consani. mm: prime-free window of the Weil goal node PROVED at L <= 1/10 (E6Bridge31-34); full window as named Prop #604 found that the 1.3e-3 margin is zero content, carried by the first 200 zero pairs. Connes-Consani covers the pole-free class, where the margin is 0.547.
• Previous ceiling. weil_positivity_window_tenth covered L <= 1/10. This PR reaches log 2/2, about 0.347, which is the whole prime-free window.

Route

The KWin_* files are all new, on the rvm_bridge island. They sit on top of #606's Zhu reduction.

1. Zhu split at T = 20.
2. An exact-rational minorant of the digamma symbol: 7 pieces, from the island's psiR_ge_series with N = 400 plus a tail. This replaces quadrature entirely, so there is no quadrature error term.
3. Exact power-series head blocks on the Legendre basis. Each block gets an exact LDL^T certificate checked by decide +kernel: even sector lam0 = 461/500000, odd sector 44191/10^6. A negative control at lam = 1e-3 is rejected by the kernel.
4. A projection tail with a 2x2 bound, which needs no Legendre completeness.
5. A new Euler-gamma bound, gamma <= H_16 - 4 log 2 - 1/32 + 1/3072. The island's old bound had an error larger than the entire margin.

Kernel time is about 48 s.

Verification

• Merged island (main + rh: Zhu window inputs -- eq. (2), Lemma 3.1, eqs. (6)/(12) PROVED; node re-specified opaque -> concrete (DRAFT, conjecture1_proved = False) #606 + KWin): 8931 jobs; all 950 guard lines (951 after the window_tenth corollary) are the standard three axioms.
• KWin_Bridge: proves RvMBridge31.PrimeFreeWindowPositivity and PrimeFreeWindowArchPositivity.
• Skeptic: not refuted. It checked the statement is identical to the E6Bridge31 body by rfl, found no forbidden tokens, and confirmed the axiom closure is the standard three only.

Independent review

An independent skeptic from session peterwmurphy-95 rebuilt cl/kwin and found the proof sound, with no gap. Its registry findings are fixed: [proof] link, the MM. name convention, and the window_tenth containment is now the kernel corollary weil_positivity_window_tenth_of_prime_free.

Registry

The new node MM_weil_positivity_prime_free_window is DRAFT. Its gate pre-flight is True. It contains MM_weil_positivity_window_tenth.

It will not be granted before #607. After #607 lands: an independent audit, then the Comparator judge on rvm_bridge.

Note

This branch includes #606 (rh/zhu-inputs), which it builds on. Merge #606 first, or merge them together.

🤖 Generated with Claude Code

https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6

Attribution (added 2026-09-25, from the "missing Frobenius" literature review)

• Prior result. Weil positivity on the window x = e^{2L} = 2 (support in [2^{-1/2}, 2^{1/2}] multiplicatively) is Yoshida's 1992 theorem, which Connes–Consani revisit in arXiv:2006.13771 (2020).
• What Yoshida's statement assumes. It holds on the pole-free subspace: ĝ vanishes at the pole points.
• What this PR proves. The same window on the full test class, with the pole terms kept, kernel-checked with no Arb seam. The margin is 1.33e-3, against Connes–Consani's 0.547 on the pole-free class.
• Why the two statements differ. They are not equivalent: the fibre directions e^{±u/2} are not window-supported, so they can't be projected out inside the test class.
• Does not separate ζ from Davenport–Heilbronn. Like every current window result, this one is blind to DH: D's form stays positive until x ≈ 31–35.