mirrormere: Weil window positivity past the prime-free boundary to L = 1/2, kernel-native, no Arb (draft; stacked on #615; grant after #607)

telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean

@@ -234,6 +234,9 @@ import E6Bridge32
 import E6Bridge33
 import E6Bridge34
 import KWin_Bridge
+import KWin2_Window25
+import KWin2_Window
+import KWin2_Bridge
 
 #print axioms RvMBridge.rvm_unbounded_mean_density
 #print axioms RvMBridge.eventually_Ncount_ge
@@ -1220,6 +1223,38 @@ import KWin_Bridge
 #print axioms weil_positivity_prime_free_window
 #print axioms weil_positivity_window_tenth_of_prime_free
 
+-- KWin2: the window certificate PAST the prime-free boundary (2026-09-24), parametric in the window;
+-- first instance L = 2/5 (2L = 0.8 > log 2: the prime comb term n = 2 is present).  Kernel-native,
+-- no Arb seam.  A finite-window statement, NOT RH; not Connes-Consani (pole terms kept); cf. PR #604.
+-- conjecture1_proved = False.
+#print axioms KWin2.sym_minorant
+#print axioms KWin2.comb_le_combPoly
+#print axioms KWin2.wpoly_le_Psi
+#print axioms KWin2.head_floor
+#print axioms KWin2.Rb_floor
+#print axioms KWin2.weilSymbol_eq_two
+#print axioms KWin2.Q_ge_Rb
+#print axioms KWin2.certE25
+#print axioms KWin2.certO25
+#print axioms KWin2.certE25_negative_control
+#print axioms KWin2.log2_near25
+#print axioms KWin2.c2_near25
+#print axioms KWin2.beta0_le_betaStar25
+#print axioms KWin2.symHyp25
+#print axioms KWin2.evenSectorFloor25
+#print axioms KWin2.oddSectorFloor25
+#print axioms KWin2.windowFloor25
+#print axioms KWin2.weil_positivity_window_two_fifths
+#print axioms KWin2.weil_positivity_prime_free_window_of_two_fifths
+-- KWin2 generic assembly (any window with log 2 < 2L <= log 3) and the rounded PSD checker.
+#print axioms KWin2.windowFloor_of_cert
+#print axioms KWin2.weil_positivity_of_windowFloor
+#print axioms KWin2.headPSD_of_psdCertR
+#print axioms KWin2.gamma_le32
+-- KWin2 registry-shape bridge at L = 2/5 (explicit binders, 2L <= 4/5).
+#print axioms weil_positivity_window_two_fifths
+#print axioms weil_window_floor_two_fifths
+
 -- 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.

telperion/examples/rvm_bridge/lean/KWin2_Bridge.lean

@@ -0,0 +1,20 @@
+/-
+  KWin2_Bridge.lean -- the window PAST the prime-free boundary at L = 2/5, in the explicit-binder
+  registry shape of `weil_positivity_prime_free_window` (KWin_Bridge) and as a WeilWindow floor
+  (rvm_bridge island, 2026-09-24).
+  2L = 0.8 > log 2: the prime comb term n = 2 is present and kept exactly on [0, T] by the
+  kernel-native certificate of KWin2_*.  Goal-node test class, pole terms kept: NOT Connes-Consani
+  (pole-free class, 2L <= log 2).  Per PR #604 a finite-window margin samples the zeros and proves
+  nothing about them.  A finite-window Weil positivity statement; conjecture1_proved = False.
+-/
+import KWin2_Window25
+
+/-- Weil positivity on every window with `2L <= 4/5` (contains the prime-free window). -/
+theorem weil_positivity_window_two_fifths (g : ℝ → ℂ) (hg : WeilExplicit.IsWeilTest g) (L : ℝ)
+    (hL : 2 * L ≤ 4 / 5) (hsupp : tsupport g ⊆ Set.Icc (-L) L) :
+    0 ≤ (WeilExplicit.weilForm (WeilExplicit.autocorr g)).re :=
+  KWin2.weil_positivity_window_two_fifths g hg L (by linarith) hsupp
+
+/-- Zhu's window floor at `L = 2/5`: `Re weilForm (autocorr f) >= (1/25000) ||f||_2^2`. -/
+theorem weil_window_floor_two_fifths : WeilWindow.WindowFloor (2 / 5) (1 / 25000) :=
+  KWin2.windowFloor25

telperion/examples/rvm_bridge/lean/KWin2_BridgeHeavy.lean

@@ -0,0 +1,31 @@
+/-
+  KWin2_BridgeHeavy.lean -- the windows L = 9/20 and L = 1/2 (past the prime-free boundary, prime
+  comb term n = 2 present), in the explicit-binder registry shape of
+  `weil_positivity_prime_free_window` and as WeilWindow floors (rvm_bridge island, 2026-09-24).
+  HEAVY: imports the L = 9/20 and L = 1/2 head certificates (kernel ~6 min / ~50 min CPU, peak
+  ~17 GB / ~19 GB), so it is not in defaultTargets; KWin2_GuardHeavy prints its axioms.
+  Goal-node test class, pole terms kept: NOT Connes-Consani.  Per PR #604 a finite-window margin
+  samples the zeros and proves nothing about them.  conjecture1_proved = False.
+-/
+import KWin2_Window920
+import KWin2_Window12
+
+/-- Weil positivity on every window with `2L <= 9/10`. -/
+theorem weil_positivity_window_nine_twentieths (g : ℝ → ℂ) (hg : WeilExplicit.IsWeilTest g) (L : ℝ)
+    (hL : 2 * L ≤ 9 / 10) (hsupp : tsupport g ⊆ Set.Icc (-L) L) :
+    0 ≤ (WeilExplicit.weilForm (WeilExplicit.autocorr g)).re :=
+  KWin2.weil_positivity_window_nine_twentieths g hg L (by linarith) hsupp
+
+/-- Zhu's window floor at `L = 9/20`: `Re weilForm (autocorr f) >= 4.5e-6 ||f||_2^2`. -/
+theorem weil_window_floor_nine_twentieths : WeilWindow.WindowFloor (9 / 20) (9 / 2000000) :=
+  KWin2.windowFloor920
+
+/-- Weil positivity on every window with `2L <= 1`. -/
+theorem weil_positivity_window_half (g : ℝ → ℂ) (hg : WeilExplicit.IsWeilTest g) (L : ℝ)
+    (hL : 2 * L ≤ 1) (hsupp : tsupport g ⊆ Set.Icc (-L) L) :
+    0 ≤ (WeilExplicit.weilForm (WeilExplicit.autocorr g)).re :=
+  KWin2.weil_positivity_window_half g hg L (by linarith) hsupp
+
+/-- Zhu's window floor at `L = 1/2`: `Re weilForm (autocorr f) >= 3.5e-7 ||f||_2^2`. -/
+theorem weil_window_floor_half : WeilWindow.WindowFloor (1 / 2) (7 / 20000000) :=
+  KWin2.windowFloor12

telperion/examples/rvm_bridge/lean/KWin2_Cert12E.lean

@@ -0,0 +1,17 @@
+/-
+  KWin2_Cert12E -- the even-sector head certificate at L = 1/2 (kernel evaluation; rvm_bridge
+  island, 2026-09-24).  `decide +kernel`: the kernel rebuilds the comb-bearing symbol minorant on
+  [0, 40], its moments and the exact 31 x 31 head matrix, floors it at 10^-70, shifts the diagonal
+  by 31e-70 and runs the exact LDL^T checker (KWin2_Round.psdCertR).  conjecture1_proved = False.
+  No `sorry`.
+-/
+import KWin2_Par12
+import KWin2_Round
+
+namespace KWin2
+open KWin
+
+/-- The even-sector head certificate at L = 1/2 (N = 31, lam = 4.2e-7, rounding 10^-70). -/
+theorem certE12 : psdCertR (headMat P12 0 31 lamE12) 31 70 = true := by decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert12N.lean

@@ -0,0 +1,16 @@
+/-
+  KWin2_Cert12N -- NEGATIVE CONTROL at L = 1/2 (kernel evaluation; rvm_bridge island, 2026-09-24):
+  at lam = 4.6e-7, above the even head eigenvalue 4.50e-7, the same pipeline (rounded checker at
+  10^-70) returns `false` (a pivot of the LDL^T is negative).  conjecture1_proved = False.
+  No `sorry`.
+-/
+import KWin2_Par12
+import KWin2_Round
+
+namespace KWin2
+open KWin
+
+theorem certE12_negative_control : psdCertR (headMat P12 0 31 (46 / 10 ^ 8)) 31 70 = false := by
+  decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert12O.lean

@@ -0,0 +1,14 @@
+/-
+  KWin2_Cert12O -- the odd-sector head certificate at L = 1/2 (kernel evaluation, rounded checker
+  psdCertR at 10^-70; rvm_bridge island, 2026-09-24).  conjecture1_proved = False.  No `sorry`.
+-/
+import KWin2_Par12
+import KWin2_Round
+
+namespace KWin2
+open KWin
+
+/-- The odd-sector head certificate at L = 1/2 (N = 29, lam = 1e-4, rounding 10^-70). -/
+theorem certO12 : psdCertR (headMat P12 1 29 lamO12) 29 70 = true := by decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert25.lean

@@ -0,0 +1,47 @@
+/-
+  KWin2_Cert25 -- the kernel evaluations of the KWin2 checkers at L = 2/5 (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 (about 40 s each): the kernel rebuilds the symbol
+  minorant WITH the prime comb (the n = 2 term, degree-62 upper polynomial), its moments, the head
+  matrix and its exact LDL^T factorisation, and verifies A = sum_s d_s v_s v_s^T entrywise.
+  NEGATIVE CONTROL: at lam = 5e-5, above the even head eigenvalue 4.70e-5, the same pipeline
+  returns `false` (a pivot of the exact LDL^T is negative), which the kernel also proves.  The
+  rational halves of the real side conditions (log 2 series, sqrt 2 squares, exp Taylor bounds)
+  are in KWin2_Window25.  conjecture1_proved = False.  No `sorry`.
+-/
+import KWin2_Par25
+
+open Finset
+
+namespace KWin2
+open KWin
+
+/-! ## A. Structural checks. -/
+
+theorem par25 : parCheck P25 = true := by decide +kernel
+theorem brk25 : brkCheck P25 = true := by decide +kernel
+theorem piece25 : pieceCheck P25 = true := by decide +kernel
+theorem min25 : minCheck P25 = true := by decide +kernel
+theorem comb25 : combCheck P25 = true := by decide +kernel
+theorem tailE25 : tailCond P25 0 16 lamE25 = true := by decide +kernel
+theorem tailO25 : tailCond P25 1 14 lamO25 = true := by decide +kernel
+theorem ginvE25 : ginvCheck P25 0 16 = true := by decide +kernel
+theorem ginvO25 : ginvCheck P25 1 14 = true := by decide +kernel
+
+/-! ## B. The head certificates. -/
+
+/-- The even-sector head certificate (N = 16, lam = 45e-6). -/
+theorem certE25 : psdCert (headMat P25 0 16 lamE25) 16 = true := by decide +kernel
+
+/-- The odd-sector head certificate (N = 14, lam = 1e-3). -/
+theorem certO25 : psdCert (headMat P25 1 14 lamO25) 14 = true := by decide +kernel
+
+/-- NEGATIVE CONTROL: the even head matrix at `lam = 5e-5` is NOT certified, so `certE25` is a
+statement about the actual margin 4.70e-5 of the comb-bearing form. -/
+theorem certE25_negative_control : psdCert (headMat P25 0 16 (5 / 10 ^ 5)) 16 = false := by
+  decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert920E.lean

@@ -0,0 +1,15 @@
+/-
+  KWin2_Cert920E -- the even-sector head certificate at L = 9/20 (kernel evaluation; rvm_bridge
+  island, 2026-09-24).  `decide +kernel`: the kernel rebuilds the comb-bearing symbol minorant, its
+  moments, the 22 x 22 head matrix and its exact LDL^T factorisation.  conjecture1_proved = False.
+  No `sorry`.
+-/
+import KWin2_Par920
+
+namespace KWin2
+open KWin
+
+/-- The even-sector head certificate at L = 9/20 (N = 22, lam = 5e-6). -/
+theorem certE920 : psdCert (headMat P920 0 22 lamE920) 22 = true := by decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert920N.lean

@@ -0,0 +1,15 @@
+/-
+  KWin2_Cert920N -- NEGATIVE CONTROL at L = 9/20 (kernel evaluation; rvm_bridge island,
+  2026-09-24): at lam = 5.2e-6, above the even head eigenvalue 5.18e-6, the same pipeline returns
+  `false` (a pivot of the exact LDL^T is negative), so certE920 is a statement about the actual
+  margin of the comb-bearing form, not a vacuous checker.  conjecture1_proved = False.  No `sorry`.
+-/
+import KWin2_Par920
+
+namespace KWin2
+open KWin
+
+theorem certE920_negative_control : psdCert (headMat P920 0 22 (52 / 10 ^ 7)) 22 = false := by
+  decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Cert920O.lean

@@ -0,0 +1,13 @@
+/-
+  KWin2_Cert920O -- the odd-sector head certificate at L = 9/20 (kernel evaluation; rvm_bridge
+  island, 2026-09-24).  conjecture1_proved = False.  No `sorry`.
+-/
+import KWin2_Par920
+
+namespace KWin2
+open KWin
+
+/-- The odd-sector head certificate at L = 9/20 (N = 19, lam = 1e-3). -/
+theorem certO920 : psdCert (headMat P920 1 19 lamO920) 19 = true := by decide +kernel
+
+end KWin2

telperion/examples/rvm_bridge/lean/KWin2_Consts.lean

@@ -0,0 +1,112 @@
+/-
+  KWin2_Consts -- shared real constants of the KWin2 window certificates (rvm_bridge island,
+  2026-09-24).
+
+  conjecture1_proved = False.  (Finite-window Weil positivity is not RH; not Connes-Consani; cf.
+  PR #604.)
+
+  PROVED HERE:
+    * log2_near_S: |log 2 - S| <= 2^-60, S = sum_{i < 60} 2^-(i+1)/(i+1) (the kernel-evaluated
+      partial sum), from Mathlib's `Real.abs_log_sub_add_sum_range_le` at x = 1/2;
+    * sqrt2_bounds: two 20-digit rationals squeeze sqrt 2 (their squares are kernel-checked);
+    * gamma_le32: Euler's constant gamma <= a_32 = H_32 - log 32 - 1/64 + 1/12288 (rounded up at
+      10^-20), i.e. gamma + 8e-9.  KWin's gamma_le stops at a_16 (gamma + 1.3e-7), which is larger
+      than the margin of the certificates past L = 2/5, so the sharper bound is needed there.  Same
+      route as KWin (a_n antitone for n >= 16, a_n -> gamma), log 2 from log2_near_S.
+  No `sorry`.
+-/
+import KWin_Constants
+
+open Real Finset Filter Topology
+
+noncomputable section
+
+namespace KWin2
+open KWin (emA emA_succ_le tendsto_emA ceilR le_ceilR)
+
+/-! ## A. log 2. -/
+
+/-- The partial sum of `log 2 = sum_{i >= 1} 2^-i / i` (60 terms). -/
+def log2S : ℚ := ∑ i ∈ range 60, (1 / 2 : ℚ) ^ (i + 1) / ((i : ℚ) + 1)
+
+theorem log2S_ge : (1 / 2) ^ 60 ≤ log2S := by decide +kernel
+
+lemma log2_near_S : |Real.log 2 - ((log2S : ℚ) : ℝ)| ≤ (1 / 2) ^ 60 := by
+  have h := Real.abs_log_sub_add_sum_range_le (x := (1 / 2 : ℝ)) (by norm_num) 60
+  have e : Real.log (1 - 1 / 2) = -Real.log 2 := by
+    rw [show (1 : ℝ) - 1 / 2 = 2⁻¹ by norm_num, Real.log_inv]
+  rw [e] at h
+  have hS : ((log2S : ℚ) : ℝ) = ∑ i ∈ range 60, (1 / 2 : ℝ) ^ (i + 1) / ((i : ℝ) + 1) := by
+    unfold log2S; push_cast; rfl
+  rw [← hS] at h
+  have hr : |(1 / 2 : ℝ)| ^ (60 + 1) / (1 - |(1 / 2 : ℝ)|) = (1 / 2) ^ 60 := by norm_num
+  rw [hr] at h
+  rw [abs_sub_comm]
+  have e2 : ((log2S : ℚ) : ℝ) + -Real.log 2 = ((log2S : ℚ) : ℝ) - Real.log 2 := by ring
+  rwa [e2] at h
+
+/-! ## B. sqrt 2. -/
+
+/-- `sqrt 2` squeezed by two 20-digit rationals. -/
+def sq2lo : ℚ := 14142135623730950488 / 10 ^ 19
+def sq2hi : ℚ := 14142135623730950489 / 10 ^ 19
+
+theorem sq2lo_sq : sq2lo ^ 2 ≤ 2 := by decide +kernel
+theorem sq2hi_sq : 2 ≤ sq2hi ^ 2 := by decide +kernel
+theorem sq2lo_pos : 0 < sq2lo := by decide +kernel
+theorem sq2hi_nonneg : 0 ≤ sq2hi := by decide +kernel
+
+lemma sqrt2_bounds : ((sq2lo : ℚ) : ℝ) ≤ Real.sqrt 2 ∧ Real.sqrt 2 ≤ ((sq2hi : ℚ) : ℝ) := by
+  have hhi0 : (0 : ℝ) ≤ ((sq2hi : ℚ) : ℝ) := by exact_mod_cast sq2hi_nonneg
+  constructor
+  · apply Real.le_sqrt_of_sq_le
+    have := (Rat.cast_le (K := ℝ)).mpr sq2lo_sq
+    push_cast at this
+    exact this
+  · rw [Real.sqrt_le_left hhi0]
+    have := (Rat.cast_le (K := ℝ)).mpr sq2hi_sq
+    push_cast at this
+    exact this
+
+/-! ## C. Euler's constant at n = 32. -/
+
+/-- `H_32`. -/
+def H32 : ℚ := ∑ k ∈ range 32, (1 : ℚ) / (k + 1)
+
+/-- `a_32 = H_32 - log 32 - 1/64 + 1/12288`, with `log 32 >= 5 (S - 2^-60)`, rounded up. -/
+def gamUp32 : ℚ := ceilR (H32 - 5 * (log2S - (1 / 2) ^ 60) - 1 / 64 + 1 / 12288) 20
+
+/-- **`gamma <= gamUp32`** (= gamma + 8e-9). -/
+theorem gamma_le32 : Real.eulerMascheroniConstant ≤ ((gamUp32 : ℚ) : ℝ) := by
+  have hanti : Antitone (fun m : ℕ => emA (m + 16)) :=
+    antitone_nat_of_succ_le fun m => by
+      have := emA_succ_le (n := m + 16) (by omega)
+      simpa [add_assoc, add_comm 1 16, add_left_comm] using this
+  have hlim : Tendsto (fun m : ℕ => emA (m + 16)) atTop (𝓝 Real.eulerMascheroniConstant) :=
+    tendsto_emA.comp (tendsto_add_atTop_nat 16)
+  have h32 : Real.eulerMascheroniConstant ≤ emA 32 := by
+    have := hanti.le_of_tendsto hlim 16
+    simpa using this
+  refine h32.trans ?_
+  have hc := le_ceilR (H32 - 5 * (log2S - (1 / 2) ^ 60) - 1 / 64 + 1 / 12288) 20
+  have hc' : (((H32 - 5 * (log2S - (1 / 2) ^ 60) - 1 / 64 + 1 / 12288 : ℚ)) : ℝ)
+      ≤ ((gamUp32 : ℚ) : ℝ) := by exact_mod_cast hc
+  refine le_trans ?_ hc'
+  unfold emA
+  have hlog32 : Real.log ((32 : ℕ) : ℝ) = 5 * Real.log 2 := by
+    rw [show ((32 : ℕ) : ℝ) = 2 ^ 5 by norm_num, Real.log_pow]
+    norm_num
+  have hl2 := (abs_le.mp log2_near_S).1
+  have hH : (harmonic 32 : ℝ) = ((H32 : ℚ) : ℝ) := by
+    unfold harmonic H32
+    push_cast
+    refine Finset.sum_congr rfl fun k _ => ?_
+    ring
+  rw [hlog32, hH]
+  push_cast
+  norm_num
+  linarith
+
+end KWin2
+
+end