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

telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean

@@ -226,12 +226,14 @@ import ZhuOrtho
 import ZhuTail
 import ZhuInstance
 import W2cAssembly
+import Probes.Dogfood_complex_re_im_split
+import Probes.Dogfood_zero_sum_majorant
+import KWin_Window
 import E6Bridge31
 import E6Bridge32
 import E6Bridge33
 import E6Bridge34
-import Probes.Dogfood_complex_re_im_split
-import Probes.Dogfood_zero_sum_majorant
+import KWin_Bridge
 
 #print axioms RvMBridge.rvm_unbounded_mean_density
 #print axioms RvMBridge.eventually_Ncount_ge
@@ -1137,6 +1139,41 @@ import Probes.Dogfood_zero_sum_majorant
 #print axioms RvMBridgeZhu.legendreLocalization_L08_T200
 #print axioms RvMBridgeZhu.legendreLocalizationOdd_L08_T200
 #print axioms RvMBridgeZhu.eps_sum_lt_betaStar_L08_T200
+
+-- KWin (2026-09-24): the prime-free window at 2L = log 2 on the goal node's FULL class (pole terms
+-- kept), certified with no Arb seam: exact-rational symbol minorant and head certificate evaluated
+-- by the kernel (decide +kernel), projection tail, Zhu split.  WindowFloor(log 2 / 2, 9/10000).
+-- A finite-window statement, NOT RH; PR #604: the 1.3e-3 margin is zero content; not
+-- Connes-Consani (pole-free class).  conjecture1_proved = False.
+#print axioms KWin.gamma_le
+#print axioms KWin.log_pi_le
+#print axioms KWin.beta0_le_betaStar
+#print axioms KWin.combMass_L0
+#print axioms KWin.weilSymbol_L0
+#print axioms KWin.abs_Psi_sub_beta0_le
+#print axioms KWin.psdCert_sound
+#print axioms KWin.cert_even
+#print axioms KWin.cert_odd
+#print axioms KWin.cert_even_negative_control
+#print axioms KWin.ginv_even
+#print axioms KWin.ginv_odd
+#print axioms KWin.piece_ok
+#print axioms KWin.tail_even
+#print axioms KWin.tail_odd
+#print axioms KWin.Tr_sub_le
+#print axioms KWin.Pl_sub_le
+#print axioms KWin.A1_sq_le
+#print axioms KWin.lor_taylor
+#print axioms KWin.wpoly_le_Psi
+#print axioms KWin.head_floor
+#print axioms KWin.Rb_floor
+#print axioms KWin.Q_ge_Rb
+#print axioms KWin.evenSectorFloor
+#print axioms KWin.oddSectorFloor
+#print axioms KWin.windowFloor_L0
+#print axioms KWin.kwin_primeFreeWindow
+#print axioms KWin.kwin_primeFreeWindowArch
+
 -- E6Bridge31: the prime-free window (2026-09-23). conjecture1_proved = False.
 #print axioms RvMBridge31.primeSide_autocorr_eq_zero
 #print axioms RvMBridge31.weilForm_autocorr_eq_archSide
@@ -1176,3 +1213,25 @@ import Probes.Dogfood_zero_sum_majorant
 #print axioms RvMBridge34.re_archSide_autocorr_ge_tenth
 #print axioms RvMBridge34.weil_positivity_window_tenth_of_nonneg
 #print axioms RvMBridge34.weil_positivity_window_tenth
+
+-- Mirrormere prime-free window (kernel-native, KWin)
+#print axioms kwin_primeFreeWindowPositivity
+#print axioms kwin_primeFreeWindowArchPositivity
+#print axioms weil_positivity_prime_free_window
+#print axioms weil_positivity_window_tenth_of_prime_free
+
+-- ZhuEnvelope (2026-09-23): Zhu Lemma 3.1, the digamma envelope, PROVED.  conjecture1_proved = False.
+
+-- ZhuSymbol (2026-09-23): Zhu eq. (2), the symbol representation, PROVED.  conjecture1_proved = False.
+
+-- ZhuLegendre (2026-09-23): Zhu eqs. (6) and (12), PROVED.  conjecture1_proved = False.
+
+-- ZhuParity (2026-09-23): Zhu Lemma 6.1, parity decoupling, PROVED.  conjecture1_proved = False.
+
+-- ZhuSplit (2026-09-23): the envelope step of eq. (4), PROVED.  conjecture1_proved = False.
+
+-- ZhuOrtho (2026-09-23): Legendre orthonormality, uniform bounds, pole vectors.  conjecture1_proved = False.
+
+-- ZhuTail (2026-09-23): the eq. (13) tail data PROVED with closed-form constants.  conjecture1_proved = False.
+
+-- ZhuInstance (2026-09-23): the instance L = 4/5, T# = 200, N = 200.  conjecture1_proved = False.

telperion/examples/rvm_bridge/lean/KWin_Bridge.lean

@@ -0,0 +1,31 @@
+/-
+  KWin_Bridge.lean -- the mirrormere prime-free window, as the named Props of E6Bridge31.
+  PrimeFreeWindowPositivity (2L <= log 2, goal-node test class with pole terms kept) is proved
+  hypothesis-free by the kernel-native certificate of KWin_*. Per PR #604 the 1.3e-3 margin is
+  zero content (first 200 zero pairs), so this is NOT Connes-Consani (pole-free class).
+  A finite-window Weil positivity statement; conjecture1_proved = False.
+-/
+import KWin_Window
+import E6Bridge31
+
+theorem kwin_primeFreeWindowPositivity : RvMBridge31.PrimeFreeWindowPositivity :=
+  KWin.kwin_primeFreeWindow
+
+theorem kwin_primeFreeWindowArchPositivity : RvMBridge31.PrimeFreeWindowArchPositivity :=
+  RvMBridge31.primeFreeWindow_iff_arch.mp KWin.kwin_primeFreeWindow
+
+/-- The full prime-free window in the explicit-binder shape of `MM_weil_positivity_window_tenth`
+    (which it contains: L <= 1/10 implies 2L <= log 2). -/
+theorem weil_positivity_prime_free_window (g : ℝ → ℂ) (hg : WeilExplicit.IsWeilTest g) (L : ℝ)
+    (hL : 2 * L ≤ Real.log 2) (hsupp : tsupport g ⊆ Set.Icc (-L) L) :
+    0 ≤ (WeilExplicit.weilForm (WeilExplicit.autocorr g)).re :=
+  kwin_primeFreeWindowPositivity g L hg hsupp hL
+
+/-- The L <= 1/10 window (`MM_weil_positivity_window_tenth`, statement verbatim) as a corollary of the full
+    prime-free window: L <= 1/10 gives 2L <= 1/5 <= log 2. -/
+theorem weil_positivity_window_tenth_of_prime_free (g : ℝ → ℂ) (hg : WeilExplicit.IsWeilTest g) (L : ℝ)
+    (hL : L ≤ 1 / 10) (hsupp : tsupport g ⊆ Set.Icc (-L) L) :
+    0 ≤ (WeilExplicit.weilForm (WeilExplicit.autocorr g)).re := by
+  have hlog : (1 : ℝ) / 5 ≤ Real.log 2 := by
+    have := Real.log_two_gt_d9; linarith
+  exact weil_positivity_prime_free_window g hg L (by linarith) hsupp

telperion/examples/rvm_bridge/lean/KWin_Cert.lean

@@ -0,0 +1,36 @@
+/-
+  KWin_Cert -- the kernel evaluations of the KWin_Data checkers (rvm_bridge island, 2026-09-24).
+
+  Every theorem below is `decide +kernel`: the Lean kernel itself reduces the Boolean checker
+  (exact rational arithmetic, GMP-accelerated `Nat`); no compiled-code evaluation is trusted.
+  The two head certificates are the expensive ones (tens of seconds each): they rebuild the
+  symbol minorant, its moments, the head matrix and its exact LDL^T factorisation, and verify
+  A = sum_s d_s v_s v_s^T entrywise.  The NEGATIVE CONTROL at the end shows the checker is not
+  vacuous: at lam = 1/1000 (above the even head eigenvalue 9.24e-4) the same pipeline returns
+  `false`, which the kernel also proves.  conjecture1_proved = False.  No `sorry`.
+-/
+import KWin_Data
+
+namespace KWin
+
+/-- The even-sector head certificate (N = 12, lam = 915e-6). -/
+theorem cert_even : psdCert (headMat 0 12 lamE) 12 = true := by decide +kernel
+
+/-- The odd-sector head certificate (N = 10, lam = 1/100). -/
+theorem cert_odd : psdCert (headMat 1 10 lamO) 10 = true := by decide +kernel
+
+theorem ginv_even : ginvCheck 0 12 = true := by decide +kernel
+
+theorem ginv_odd : ginvCheck 1 10 = true := by decide +kernel
+
+theorem piece_ok : pieceCheck = true := by decide +kernel
+
+theorem tail_even : tailCond 0 12 lamE = true := by decide +kernel
+
+theorem tail_odd : tailCond 1 10 lamO = true := by decide +kernel
+
+/-- NEGATIVE CONTROL: the even-sector head matrix at `lam = 1/1000` is NOT certified (a pivot of its
+exact LDL^T is negative), so `cert_even` is a statement about the actual margin 9.24e-4. -/
+theorem cert_even_negative_control : psdCert (headMat 0 12 (1 / 1000)) 12 = false := by decide +kernel
+
+end KWin