From c4d17bce93ae3ee27edc62ad4e1427838f84c2b8 Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Thu, 24 Sep 2026 01:12:50 -0400 Subject: [PATCH 1/6] rvm_bridge: KWin -- kernel-native (Arb-free) prime-free window: WindowFloor(log2/2, 9/10000) and the PrimeFreeWindowPositivity body at 2L = log 2, hypothesis-free Exact-rational digamma minorant (7 pieces, psiR_ge_series N=400 + tail) replaces quadrature; Zhu split at T=20; exact LDL^T head certificates (even lam0=461/500000, odd 44191/10^6) by decide +kernel with a lam=1e-3 negative control rejected; projection tail + 2x2 bound; new gamma <= H_16 - 4 log 2 - 1/32 + 1/3072. Pole terms KEPT (goal-node class). Per PR #604 the 1.3e-3 margin is zero content (first 200 zero pairs); not Connes-Consani (pole-free class). Skeptic not refuted. conjecture1_proved = False. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6 --- .../rvm_bridge/lean/AxiomGuardRvMBridge.lean | 35 + .../examples/rvm_bridge/lean/KWin_Cert.lean | 36 ++ .../rvm_bridge/lean/KWin_Constants.lean | 322 ++++++++++ .../examples/rvm_bridge/lean/KWin_Data.lean | 446 +++++++++++++ .../examples/rvm_bridge/lean/KWin_Head.lean | 554 ++++++++++++++++ .../rvm_bridge/lean/KWin_Minorant.lean | 597 ++++++++++++++++++ .../examples/rvm_bridge/lean/KWin_Split.lean | 357 +++++++++++ .../examples/rvm_bridge/lean/KWin_Tail.lean | 393 ++++++++++++ .../examples/rvm_bridge/lean/KWin_Taylor.lean | 427 +++++++++++++ .../examples/rvm_bridge/lean/KWin_Window.lean | 178 ++++++ .../examples/rvm_bridge/lean/lakefile.toml | 33 +- 11 files changed, 3377 insertions(+), 1 deletion(-) create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Cert.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Constants.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Data.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Head.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Minorant.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Split.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Tail.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Taylor.lean create mode 100644 telperion/examples/rvm_bridge/lean/KWin_Window.lean diff --git a/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean b/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean index 28252e23a..b80544270 100644 --- a/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean +++ b/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean @@ -228,6 +228,7 @@ import ZhuInstance import W2cAssembly import Probes.Dogfood_complex_re_im_split import Probes.Dogfood_zero_sum_majorant +import KWin_Window #print axioms RvMBridge.rvm_unbounded_mean_density #print axioms RvMBridge.eventually_Ncount_ge @@ -1133,3 +1134,37 @@ 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 diff --git a/telperion/examples/rvm_bridge/lean/KWin_Cert.lean b/telperion/examples/rvm_bridge/lean/KWin_Cert.lean new file mode 100644 index 000000000..81b0bc60c --- /dev/null +++ b/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 diff --git a/telperion/examples/rvm_bridge/lean/KWin_Constants.lean b/telperion/examples/rvm_bridge/lean/KWin_Constants.lean new file mode 100644 index 000000000..85cc77ab1 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Constants.lean @@ -0,0 +1,322 @@ +/- + KWin_Constants -- the real constants of the prime-free window certificate at 2L = log 2 + (rvm_bridge island, 2026-09-24). + + conjecture1_proved = False. A finite-window Weil positivity statement is NOT RH (PR #604: the + 1.3e-3 full-class margin at this window is zero content; not Connes-Consani, whose theorem is + for the pole-free class). + + PROVED HERE: + * gamma_le: Euler's constant gamma <= H_16 - 4 * 0.6931471803 - 1/32 + 1/3072 (= gamma + + 1.3e-7). The island's 0.58112 is off by 3.9e-3, larger than the whole margin, so this + sharper bound is mandatory. Route: a_n = H_n - log n - 1/(2n) + 1/(12 n^2) is antitone for + n >= 16 (log(1 + 1/n) against its degree-6 Taylor floor; the difference is + (2n^4 - 3n^3 - 67n^2 - 122n - 50) / (60 n^6 (n-1) (n+1)^2) >= 0) and tends to gamma + (Real.tendsto_harmonic_sub_log), so gamma <= a_16. + * log_pi_le: log pi <= 1.1447298859 (pi_lt_d20 and the exp Taylor floor, kernel-checked). + * combMass_L0 / weilSymbol_L0: on the window 2L = log 2 the prime comb is EMPTY + (Lambda(0) = Lambda(1) = 0), so Psi_L0(t) = Re psi(1/4 + it/2) - log pi. + * beta0_le_betaStar: 1107/1000 <= beta*(log 2 / 2, 20) = log(10/pi) - 1/20. + * abs_Psi_sub_beta0_le: |Psi(t) - beta0| <= 6.485 on [0, 20]. + * cosh_half_ell_le: cosh(l/2) <= 1.02, l = 26/75; L0_lt_ell: log 2 / 2 < 26/75. + No `sorry`. +-/ +import ZhuTail +import KWin_Data + +open Real Finset Filter Topology + +noncomputable section + +namespace KWin +open RvMBridge11 RvMBridge30 RvMBridgeZhu WeilWindow + +/-- The window half-width `L0 = log 2 / 2` (the edge `2 L0 = log 2` of the prime-free window). -/ +def L0 : ℝ := Real.log 2 / 2 + +/-- The Weil symbol on the prime-free window: `Psi(t) = Re psi(1/4 + it/2) - log pi`. -/ +def Psi (t : ℝ) : ℝ := psiR t - Real.log Real.pi + +/-! ## A. pi. -/ + +theorem pi_gt_Q : ((piLoQ : ℚ) : ℝ) < Real.pi := by + have h := Real.pi_gt_d20 + have e : ((piLoQ : ℚ) : ℝ) = 3.14159265358979323846 := by unfold piLoQ; norm_num + rw [e]; exact h + +theorem pi_lt_Q : Real.pi < ((piHiQ : ℚ) : ℝ) := by + have h := Real.pi_lt_d20 + have e : ((piHiQ : ℚ) : ℝ) = 3.14159265358979323847 := by unfold piHiQ; norm_num + rw [e]; exact h + +/-! ## B. Euler's constant. -/ + +/-- `a n = H_n - log n - 1/(2n) + 1/(12 n^2)`. -/ +def emA (n : ℕ) : ℝ := (harmonic n : ℝ) - Real.log n - 1 / (2 * n) + 1 / (12 * (n : ℝ) ^ 2) + +lemma em_poly {n : ℝ} (hn : 16 ≤ n) : + 1 / (2 * (n + 1)) + 1 / (2 * n) - 1 / (12 * n ^ 2) + 1 / (12 * (n + 1) ^ 2) + ≤ 1 / n - 1 / (2 * n ^ 2) + 1 / (3 * n ^ 3) - 1 / (4 * n ^ 4) + 1 / (5 * n ^ 5) + - 1 / (6 * n ^ 6) - (1 / n) ^ 7 / (1 - 1 / n) := by + have hn0 : n ≠ 0 := by positivity + have hn1 : n - 1 ≠ 0 := by + have : 0 < n - 1 := by linarith + exact this.ne' + have hn2 : n + 1 ≠ 0 := by positivity + rw [← sub_nonneg] + have h1 : 1 - 1 / n = (n - 1) / n := by field_simp + have key : (1 / n - 1 / (2 * n ^ 2) + 1 / (3 * n ^ 3) - 1 / (4 * n ^ 4) + 1 / (5 * n ^ 5) + - 1 / (6 * n ^ 6) - (1 / n) ^ 7 / (1 - 1 / n)) + - (1 / (2 * (n + 1)) + 1 / (2 * n) - 1 / (12 * n ^ 2) + 1 / (12 * (n + 1) ^ 2)) + = (2 * n ^ 4 - 3 * n ^ 3 - 67 * n ^ 2 - 122 * n - 50) + / (60 * n ^ 6 * (n - 1) * (n + 1) ^ 2) := by + rw [h1] + field_simp + ring + rw [key] + apply div_nonneg + · have hm : 0 ≤ n - 16 := by linarith + have e : 2 * n ^ 4 - 3 * n ^ 3 - 67 * n ^ 2 - 122 * n - 50 + = 2 * (n - 16) ^ 4 + 125 * (n - 16) ^ 3 + 2861 * (n - 16) ^ 2 + 28198 * (n - 16) + 99630 := by + ring + rw [e] + positivity + · have : 0 < n - 1 := by linarith + positivity + +/-- `log (1 + x) >= x - x^2/2 + ... - x^6/6 - x^7/(1-x)` for `0 < x < 1`. -/ +lemma log_one_add_ge {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : + x - x ^ 2 / 2 + x ^ 3 / 3 - x ^ 4 / 4 + x ^ 5 / 5 - x ^ 6 / 6 - x ^ 7 / (1 - x) + ≤ Real.log (1 + x) := by + have habs : |(-x)| < 1 := by rw [abs_neg, abs_of_pos hx0]; exact hx1 + have h := Real.abs_log_sub_add_sum_range_le habs 6 + have e1 : (∑ i ∈ range 6, (-x) ^ (i + 1) / ((i : ℝ) + 1)) + = -x + x ^ 2 / 2 - x ^ 3 / 3 + x ^ 4 / 4 - x ^ 5 / 5 + x ^ 6 / 6 := by + simp only [Finset.sum_range_succ, Finset.sum_range_zero] + norm_num + ring + rw [e1, abs_neg, abs_of_pos hx0, sub_neg_eq_add] at h + have h2 := (abs_le.mp h).1 + linarith + +lemma emA_succ_le {n : ℕ} (hn : 16 ≤ n) : emA (n + 1) ≤ emA n := by + have hnR : (16 : ℝ) ≤ n := by exact_mod_cast hn + have hn0 : (0 : ℝ) < n := by linarith + have hx0 : (0 : ℝ) < 1 / n := by positivity + have hx1 : (1 : ℝ) / n < 1 := by rw [div_lt_one hn0]; linarith + have hlog := log_one_add_ge hx0 hx1 + have hpoly := em_poly hnR + have hl : Real.log ((n : ℝ) + 1) - Real.log n = Real.log (1 + 1 / n) := by + rw [← Real.log_div (by positivity) hn0.ne'] + congr 1 + field_simp + have hH : (harmonic (n + 1) : ℝ) = (harmonic n : ℝ) + 1 / ((n : ℝ) + 1) := by + rw [harmonic_succ] + push_cast + ring + unfold emA + push_cast + rw [hH] + have e2 : (1 / (n : ℝ)) ^ 2 / 2 = 1 / (2 * (n : ℝ) ^ 2) := by field_simp + have e3 : (1 / (n : ℝ)) ^ 3 / 3 = 1 / (3 * (n : ℝ) ^ 3) := by field_simp + have e4 : (1 / (n : ℝ)) ^ 4 / 4 = 1 / (4 * (n : ℝ) ^ 4) := by field_simp + have e5 : (1 / (n : ℝ)) ^ 5 / 5 = 1 / (5 * (n : ℝ) ^ 5) := by field_simp + have e6 : (1 / (n : ℝ)) ^ 6 / 6 = 1 / (6 * (n : ℝ) ^ 6) := by field_simp + rw [e2, e3, e4, e5, e6] at hlog + have e7 : 1 / ((n : ℝ) + 1) - 1 / (2 * ((n : ℝ) + 1)) = 1 / (2 * ((n : ℝ) + 1)) := by + field_simp + ring + nlinarith [hl, hlog, hpoly, e7] + +lemma tendsto_emA : Tendsto emA atTop (𝓝 Real.eulerMascheroniConstant) := by + have h1 := Real.tendsto_harmonic_sub_log + have h2 : Tendsto (fun n : ℕ => 1 / (2 * (n : ℝ))) atTop (𝓝 0) := by + have := tendsto_const_div_atTop_nhds_zero_nat (1 / 2 : ℝ) + refine this.congr fun n => ?_ + rw [div_div] + have h3 : Tendsto (fun n : ℕ => 1 / (12 * (n : ℝ) ^ 2)) atTop (𝓝 0) := by + refine squeeze_zero' (Eventually.of_forall fun n => by positivity) ?_ + tendsto_one_div_atTop_nhds_zero_nat + filter_upwards [eventually_ge_atTop 1] with n hn + have hnR : (1 : ℝ) ≤ n := by exact_mod_cast hn + rw [div_le_div_iff₀ (by positivity) (by positivity)] + nlinarith + have h4 := (h1.sub h2).add h3 + simp only [sub_zero, add_zero] at h4 + refine h4.congr fun n => ?_ + unfold emA + ring + +/-- **A1.** `gamma <= H_16 - 4 * 0.6931471803 - 1/32 + 1/3072`. -/ +theorem gamma_le : Real.eulerMascheroniConstant ≤ ((gammaUpQ : ℚ) : ℝ) := 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 h16 : Real.eulerMascheroniConstant ≤ emA 16 := by + have := hanti.le_of_tendsto hlim 0 + simpa using this + refine h16.trans ?_ + unfold emA gammaUpQ + have hlog16 : Real.log ((16 : ℕ) : ℝ) = 4 * Real.log 2 := by + rw [show ((16 : ℕ) : ℝ) = 2 ^ 4 by norm_num, Real.log_pow] + norm_num + have hl2 := Real.log_two_gt_d9 + have hH : (harmonic 16 : ℝ) = ((∑ k ∈ range 16, (1 : ℚ) / (k + 1) : ℚ) : ℝ) := by + unfold harmonic + congr 1 + refine Finset.sum_congr rfl fun k _ => ?_ + push_cast + ring + rw [hlog16, hH] + push_cast + norm_num at hl2 ⊢ + linarith + +/-! ## C. log pi. -/ + +/-- **A2.** `log pi <= 1.1447298859`. -/ +theorem log_pi_le : Real.log Real.pi ≤ ((logPiUpQ : ℚ) : ℝ) := by + rw [Real.log_le_iff_le_exp Real.pi_pos] + have h2 : (piHiQ : ℚ) ≤ ∑ i ∈ range 30, logPiUpQ ^ i / (i.factorial : ℚ) := by decide +kernel + have h2' : ((piHiQ : ℚ) : ℝ) ≤ ∑ i ∈ range 30, ((logPiUpQ : ℚ) : ℝ) ^ i / (i.factorial : ℝ) := by + have := (Rat.cast_le (K := ℝ)).mpr h2 + push_cast at this + exact this + have h3 := Real.sum_le_exp_of_nonneg (x := ((logPiUpQ : ℚ) : ℝ)) (by unfold logPiUpQ; norm_num) 30 + linarith [pi_lt_Q] + +theorem one_le_log_pi : 1 ≤ Real.log Real.pi := by + rw [Real.le_log_iff_exp_le Real.pi_pos] + have := Real.exp_one_lt_d9 + have := Real.pi_gt_three + linarith + +/-! ## D. The prime comb is empty on the window. -/ + +lemma comb_term_eq_zero (n : ℕ) (hn : Real.log n < 2 * L0) : + ArithmeticFunction.vonMangoldt n = 0 := by + have h2 : 2 * L0 = Real.log 2 := by unfold L0; ring + rw [h2] at hn + have hn2 : n < 2 := by + by_contra hc + have hc' : 2 ≤ n := not_lt.mp hc + have : Real.log 2 ≤ Real.log n := Real.log_le_log (by norm_num) (by exact_mod_cast hc') + linarith + interval_cases n <;> simp + +/-- **A4.** `combMass (log 2 / 2) = 0`. -/ +theorem combMass_L0 : combMass L0 = 0 := by + unfold combMass + convert tsum_zero with n + split_ifs with h + · rw [comb_term_eq_zero n h]; simp + · rfl + +/-- **A5.** On the window the Weil symbol is `Psi`. -/ +theorem weilSymbol_L0 (t : ℝ) : weilSymbol L0 t = Psi t := by + unfold weilSymbol Psi + have h0 : (∑' n : ℕ, if Real.log n < 2 * L0 then + 2 * ArithmeticFunction.vonMangoldt n / Real.sqrt n * Real.cos (t * Real.log n) else 0) = 0 := by + convert tsum_zero with n + split_ifs with h + · rw [comb_term_eq_zero n h]; simp + · rfl + rw [h0, sub_zero] + rfl + +/-! ## E. beta*. -/ + +/-- **A3.** `beta0 = 1107/1000 <= beta*(log 2 / 2, 20) = log(10/pi) - 1/20`. -/ +theorem beta0_le_betaStar : ((beta0Q : ℚ) : ℝ) ≤ betaStar L0 20 := by + unfold betaStar + rw [combMass_L0] + have hlog : (1157 / 1000 : ℝ) ≤ Real.log (20 / (2 * Real.pi)) := by + rw [Real.le_log_iff_exp_le (by positivity)] + have e1 : Real.exp (1157 / 1000) = Real.exp (1157 / 2000) ^ 2 := by + rw [← Real.exp_nat_mul]; norm_num + have e2 := Real.exp_bound' (x := 1157 / 2000) (by norm_num) (by norm_num) (n := 10) (by norm_num) + have hq : ((∑ m ∈ range 10, (1157 / 2000 : ℚ) ^ m / (m.factorial : ℚ)) + + (1157 / 2000 : ℚ) ^ 10 * (10 + 1) / ((Nat.factorial 10 : ℚ) * 10)) ^ 2 * piHiQ ≤ 10 := by + decide +kernel + have hq' : ((∑ m ∈ range 10, (1157 / 2000 : ℝ) ^ m / (m.factorial : ℝ)) + + (1157 / 2000 : ℝ) ^ 10 * (10 + 1) / ((Nat.factorial 10 : ℝ) * 10)) ^ 2 + * ((piHiQ : ℚ) : ℝ) ≤ 10 := by + have := (Rat.cast_le (K := ℝ)).mpr hq + push_cast at this + exact this + have hpos : 0 ≤ Real.exp (1157 / 2000) := (Real.exp_pos _).le + have hsq : Real.exp (1157 / 2000) ^ 2 ≤ ((∑ m ∈ range 10, (1157 / 2000 : ℝ) ^ m / (m.factorial : ℝ)) + + (1157 / 2000 : ℝ) ^ 10 * (10 + 1) / ((Nat.factorial 10 : ℝ) * 10)) ^ 2 := + pow_le_pow_left₀ hpos e2 2 + have hpi := pi_lt_Q + have hpi0 := Real.pi_pos + rw [e1, show (20 : ℝ) / (2 * Real.pi) = 10 / Real.pi by field_simp; ring, + le_div_iff₀ hpi0] + nlinarith + unfold beta0Q + push_cast + linarith + +/-! ## F. The symbol is bounded on [0, 20]. -/ + +lemma log_ten_le : Real.log 10 ≤ 231 / 100 := by + rw [Real.log_le_iff_le_exp (by norm_num)] + have h := Real.sum_le_exp_of_nonneg (x := 231 / 100) (by norm_num) 20 + have hq : (10 : ℚ) ≤ ∑ i ∈ range 20, (231 / 100 : ℚ) ^ i / (i.factorial : ℚ) := by decide +kernel + have hq' : (10 : ℝ) ≤ ∑ i ∈ range 20, (231 / 100 : ℝ) ^ i / (i.factorial : ℝ) := by + have := (Rat.cast_le (K := ℝ)).mpr hq + push_cast at this + exact this + linarith + +/-- **A7.** `|Psi(t) - beta0| <= 6.485` for `0 <= t <= 20`. -/ +theorem abs_Psi_sub_beta0_le {t : ℝ} (h0 : 0 ≤ t) (h1 : t ≤ 20) : + |Psi t - ((beta0Q : ℚ) : ℝ)| ≤ ((S0Q : ℚ) : ℝ) := by + have hlow : psiR 0 ≤ psiR t := psiR_mono le_rfl (by rw [abs_of_nonneg h0]; exact h0) + have hup : psiR t ≤ psiR 20 := psiR_mono h0 (by rw [abs_of_pos (by norm_num : (0 : ℝ) < 20)]; exact h1) + have hfl := psiR_floor_0 + have hst := psiR_le_stirling (t := 20) (by norm_num) + have h10 : Real.log ((20 : ℝ) / 2) = Real.log 10 := by norm_num + rw [h10] at hst + have hl10 := log_ten_le + have hlp := log_pi_le + have hlp1 := one_le_log_pi + unfold Psi + unfold beta0Q S0Q logPiUpQ at * + push_cast at * + rw [abs_le] + constructor <;> nlinarith + +/-! ## G. Miscellaneous. -/ + +/-- **A6.** `log 2 / 2 < 26/75`. -/ +theorem L0_lt_ell : L0 < ((ellQ : ℚ) : ℝ) := by + unfold L0 ellQ + have := Real.log_two_lt_d9 + push_cast + norm_num at this ⊢ + linarith + +theorem L0_pos : 0 < L0 := by + unfold L0 + have := Real.log_two_gt_d9 + norm_num at this ⊢ + linarith + +theorem cosh_half_ell_le : Real.cosh (((ellQ : ℚ) : ℝ) / 2) ≤ ((CpQ : ℚ) : ℝ) := by + have h := Real.cosh_le_exp_half_sq (((ellQ : ℚ) : ℝ) / 2) + have hx : (((ellQ : ℚ) : ℝ) / 2) ^ 2 / 2 = 169 / 11250 := by unfold ellQ; push_cast; norm_num + rw [hx] at h + have e2 := Real.exp_bound' (x := 169 / 11250) (by norm_num) (by norm_num) (n := 3) (by norm_num) + simp only [Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial] at e2 + unfold CpQ + push_cast + norm_num at e2 ⊢ + linarith + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Data.lean b/telperion/examples/rvm_bridge/lean/KWin_Data.lean new file mode 100644 index 000000000..4f73857e4 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Data.lean @@ -0,0 +1,446 @@ +/- + KWin_Data -- the exact-rational data of the prime-free window certificate at 2L = log 2 + (rvm_bridge island, 2026-09-24). + + conjecture1_proved = False. A finite-window Weil positivity statement is NOT RH. PR #604 + found that the 1.3e-3 full-class margin at this window is zero content (the zero sum over the + first 200 zero pairs is 0.001301 against a least eigenvalue of 0.001329), and Connes-Consani's + theorem is for the pole-free class (margin 0.547 here), so nothing below is their result. + + WHAT THIS FILE IS. Computable definitions over `ℚ` / `ℕ`, evaluated by the Lean kernel itself + (`decide +kernel`: the kernel reduces the Boolean checker; no compiled-code evaluation and no + trusted-reduction shortcut). Nothing here is analysis; the modules KWin_Minorant / KWin_Head consume the + data through the soundness lemmas of sections H-J. + * B. the symbol minorant w_i on the 7 pieces [brk i, brk (i+1)] of [0, 20]: the island's + series floor (psiR_ge_series with N = 400 explicit terms and the integral tail), the + Lorentzians x/(x^2 + (r/2)^2), x = j + 1/4, j < 18, bounded on each piece by their + geometric Taylor polynomial about the centre (coefficients `kap`, floor-rounded at + 10^-30, remainder `remB`), the Lorentzians 18 <= j <= 400 by the global alternating + bound 1/(1+y) <= sum_{k<=10} (-y)^k, all constants rounded in the safe direction; + * C. the moments of (w - beta0) t^q over [0, 20] and the pi-scaled head matrix of the + scaled monomials (x/l)^(2k+par), l = 26/75, k < N (N = 12 even, N = 10 odd); + * D. an LDL^T certificate: the kernel factors the head matrix exactly and re-verifies + A = sum_s d_s v_s v_s^T entrywise with every d_s >= 0 (soundness is pure algebra); + * E. the exact inverse of the Gram matrix of the head monomials (data; G * G^-1 = I checked). + No `sorry`. +-/ +import Mathlib + +open Finset + +namespace KWin + +/-! ## A. Parameters. -/ + +/-- The head half-width `l = 26/75`; `log 2 / 2 < l`. -/ +def ellQ : ℚ := 26 / 75 +/-- The frequency cut `T = 20`. -/ +def TQ : ℚ := 20 +/-- The rational envelope floor `beta0 <= beta*(log 2 / 2, 20) = log (10/pi) - 1/20`. -/ +def beta0Q : ℚ := 1107 / 1000 +/-- `Real.pi_gt_d20`. -/ +def piLoQ : ℚ := 314159265358979323846 / 10 ^ 20 +/-- `Real.pi_lt_d20`. -/ +def piHiQ : ℚ := 314159265358979323847 / 10 ^ 20 +/-- `|Psi - beta0| <= S0` on `[0, 20]`. -/ +def S0Q : ℚ := 6485 / 1000 +/-- `cosh (l / 2) <= Cp`. -/ +def CpQ : ℚ := 102 / 100 +/-- `gamma <= H_16 - 4 * 0.6931471803 - 1/32 + 1/3072` (Euler-Maclaurin, KWin_Constants). -/ +def gammaUpQ : ℚ := (∑ k ∈ range 16, (1 : ℚ) / (k + 1)) - 4 * (6931471803 / 10 ^ 10) - 1 / 32 + 1 / 3072 +/-- `log pi <= 1.1447298859`. -/ +def logPiUpQ : ℚ := 11447298859 / 10 ^ 10 + +/-! ## B. The symbol minorant. -/ + +/-- The breakpoints `0 = brk 0 < ... < brk 7 = 20` of the seven pieces. -/ +def brk : ℕ → ℚ + | 0 => 0 + | 1 => 3 / 10 + | 2 => 4 / 5 + | 3 => 8 / 5 + | 4 => 16 / 5 + | 5 => 32 / 5 + | 6 => 64 / 5 + | _ => 20 + +def nPc : ℕ := 7 +def pcen (i : ℕ) : ℚ := (brk i + brk (i + 1)) / 2 +def phw (i : ℕ) : ℚ := (brk (i + 1) - brk i) / 2 + +/-- Number of Lorentzians kept exact (per piece): `x_j = j + 1/4`, `j < 18`. -/ +def nS : ℕ := 18 +/-- `b_j = 2 x_j = 2 j + 1/2`. -/ +def bS (j : ℕ) : ℚ := 2 * j + 1 / 2 + +/-- Taylor degrees per (piece, Lorentzian): chosen offline so each remainder is <= 1e-8. -/ +def degTab : List (List ℕ) := + [[16, 6, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, 2, 2], + [18, 7, 6, 5, 4, 4, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3], + [17, 9, 7, 6, 5, 5, 4, 4, 4, 4, 4, 3, 3, 3, 3, 3, 3, 3], + [16, 12, 9, 8, 7, 6, 6, 5, 5, 5, 4, 4, 4, 4, 4, 4, 4, 4], + [16, 15, 12, 10, 9, 8, 8, 7, 7, 6, 6, 6, 5, 5, 5, 5, 5, 5], + [15, 15, 15, 13, 12, 11, 10, 9, 9, 8, 8, 8, 7, 7, 7, 7, 6, 6], + [10, 10, 10, 10, 10, 9, 9, 9, 8, 8, 8, 7, 7, 7, 7, 7, 6, 6]] + +def deg (i j : ℕ) : ℕ := (degTab.getD i []).getD j 0 +def Dmax : ℕ := 20 +def Rk : ℕ := 30 + +/-- A rational lower bound `s <= sqrt (b^2 + c^2)` (for `0 <= b, c`). -/ +def smax (b c : ℚ) : ℚ := max (max b c) (7 / 10 * (b + c)) + +/-- Powers of the Gaussian rational `x + i y`: `(gpow x y n).1 + i (gpow x y n).2 = (x + i y)^n`. -/ +def gpow (x y : ℚ) : ℕ → ℚ × ℚ + | 0 => (1, 0) + | n + 1 => match gpow x y n with + | (p, q) => (p * x - q * y, p * y + q * x) + +/-- `kap b c k = 2 Re (i^k / (b - i c)^(k+1))`, the Taylor coefficients of `2 Re (1/(b - i t))` +about `t = c`. -/ +def kap (b c : ℚ) (k : ℕ) : ℚ := + 2 * (if k % 4 = 0 then (gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).1 + else if k % 4 = 1 then -(gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).2 + else if k % 4 = 2 then -(gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).1 + else (gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).2) + +def floorR (q : ℚ) (R : ℕ) : ℚ := (⌊q * 10 ^ R⌋ : ℚ) / 10 ^ R +def ceilR (q : ℚ) (R : ℕ) : ℚ := (⌈q * 10 ^ R⌉ : ℚ) / 10 ^ R + +def kapR (b c : ℚ) (k : ℕ) : ℚ := floorR (kap b c k) Rk + +/-- The geometric remainder `2 rho^(d+1) / ((1 - rho) s)`, `rho = h / s`. -/ +def remB (b c h : ℚ) (d : ℕ) : ℚ := + 2 * (h / smax b c) ^ (d + 1) / ((1 - h / smax b c) * smax b c) + +/-- Shifted coefficients of the exact-Lorentzian upper polynomial on piece `i`. -/ +def uCoef (i k : ℕ) : ℚ := ∑ j ∈ range nS, if k ≤ deg i j then kapR (bS j) (pcen i) k else 0 + +def rhoRaw (i : ℕ) : ℚ := ∑ j ∈ range nS, + (remB (bS j) (pcen i) (phw i) (deg i j) + (∑ k ∈ range (deg i j + 1), phw i ^ k) / 10 ^ Rk) +def rhoR (i : ℕ) : ℚ := ceilR (rhoRaw i) Rk + +def Nser : ℕ := 400 +def Mser : ℕ := 10 ^ 9 +def Kalt : ℕ := 5 + +/-- `HNr <= H_400` (termwise floor at 10^-30). -/ +def HNr : ℚ := (∑ n ∈ range Nser, ((10 ^ 30 / (n + 1) : ℕ) : ℚ)) / 10 ^ 30 +def NQ : ℚ := Nser +def MQ : ℚ := Mser +def C0 : ℚ := -gammaUpQ - logPiUpQ + HNr + (1 / 4) / (NQ + 5 / 4) + - (1 / 2) * ((NQ + MQ + 5 / 4) ^ 2 - (NQ + MQ + 1) ^ 2) / (NQ + MQ + 1) ^ 2 +def C1 : ℚ := 1 / (8 * (NQ + 5 / 4) ^ 2) - 1 / (8 * (NQ + MQ + 1) ^ 2) +def C2 : ℚ := -1 / (32 * (NQ + 5 / 4) ^ 4) + +/-- An upper bound on `(-1)^k sum_{18 <= j <= 400} 4^(k+1) / (4 j + 1)^(2k+1)` (termwise +ceiling / floor at `10^-(30+3k)`). -/ +def gAlt (k : ℕ) : ℚ := + if k % 2 = 0 then + (∑ j ∈ Ico nS (Nser + 1), (((4 ^ (k + 1) * 10 ^ (30 + 3 * k) + (4 * j + 1) ^ (2 * k + 1) - 1) + / (4 * j + 1) ^ (2 * k + 1) : ℕ) : ℚ)) / 10 ^ (30 + 3 * k) + else + -(∑ j ∈ Ico nS (Nser + 1), ((4 ^ (k + 1) * 10 ^ (30 + 3 * k) / (4 * j + 1) ^ (2 * k + 1) : ℕ) : ℚ)) + / 10 ^ (30 + 3 * k) + +def globRaw (p : ℕ) : ℚ := + (if p = 0 then C0 else if p = 2 then C1 else if p = 4 then C2 else 0) + - (if p % 2 = 0 ∧ p / 2 ≤ 2 * Kalt then gAlt (p / 2) else 0) +def globC (p : ℕ) : ℚ := floorR (globRaw p) (30 + 3 * (p / 2)) +def globList : List ℚ := (List.range (Dmax + 1)).map globC + +def uList (i : ℕ) : List ℚ := (List.range (Dmax + 1)).map (uCoef i) +/-- Power-basis coefficients of the minorant on piece `i`: +`w_i(t) = sum_p globC p t^p - sum_k uCoef i k (t - c_i)^k - rhoR i`. -/ +def wpCoef (i p : ℕ) : ℚ := globList.getD p 0 + - (∑ k ∈ range (Dmax + 1), if p ≤ k then (uList i).getD k 0 * (k.choose p) * (-pcen i) ^ (k - p) else 0) + - (if p = 0 then rhoR i else 0) +def wpList (i : ℕ) : List ℚ := (List.range (Dmax + 1)).map (wpCoef i) + +/-! ## C. Moments and the head matrix. -/ + +/-- `int_{brk i}^{brk (i+1)} (w_i t - beta0) t^q dt`. -/ +def momPiece (i q : ℕ) : ℚ := + (∑ p ∈ range (Dmax + 1), (wpList i).getD p 0 * (brk (i + 1) ^ (p + q + 1) - brk i ^ (p + q + 1)) / (p + q + 1)) + - beta0Q * (brk (i + 1) ^ (q + 1) - brk i ^ (q + 1)) / (q + 1) +def mom (q : ℕ) : ℚ := ∑ i ∈ range nPc, momPiece i q + +def Mt : ℕ := 16 +def Mp : ℕ := 8 +def momList (par : ℕ) : List ℚ := (List.range (2 * Mt)).map (fun s => mom (2 * s + 2 * par)) + +/-- Gram matrix of the scaled monomials: `int_{-l}^{l} (x/l)^(2j+par) (x/l)^(2k+par) dx`. -/ +def Gm (par j k : ℕ) : ℚ := 2 * ellQ / (2 * j + 2 * k + 2 * par + 1) +/-- Taylor coefficient matrix of the transforms: `c_m = sum_k Bm par m k a_k`. -/ +def Bm (par m k : ℕ) : ℚ := (-1) ^ m * ellQ ^ (2 * m + par) / ((2 * m + par).factorial : ℚ) * Gm par m k +/-- The truncated pole functional of `(x/l)^(2k+par)`. -/ +def pv (par k : ℕ) : ℚ := ∑ m ∈ range Mp, (ellQ / 2) ^ (2 * m + par) / ((2 * m + par).factorial : ℚ) * Gm par m k + +def WBrow (par N m : ℕ) : List ℚ := + (List.range N).map (fun k => ∑ m' ∈ range Mt, (momList par).getD (m + m') 0 * Bm par m' k) +def WBmat (par N : ℕ) : List (List ℚ) := (List.range Mt).map (WBrow par N) + +def epsQ (par : ℕ) : ℚ := if par = 0 then 1 else -1 +def piEQ (par : ℕ) : ℚ := if par = 0 then piLoQ else piHiQ +/-- Upper bound for the head truncation error constant (checked in section G). -/ +def Econst : ℚ := 1 / 10 ^ 6 +def diagc (lam : ℚ) : ℚ := piLoQ * (beta0Q - lam) - 2 * ellQ * Econst + +def headEntry (par N : ℕ) (lam : ℚ) (j k : ℕ) : ℚ := + 2 * piEQ par * epsQ par * pv par j * pv par k + diagc lam * Gm par j k + + ∑ m ∈ range Mt, Bm par m j * ((WBmat par N).getD m []).getD k 0 +def headMat (par N : ℕ) (lam : ℚ) : List (List ℚ) := + (List.range N).map (fun j => (List.range N).map (headEntry par N lam j)) + +/-! ## D. The LDL^T certificate. -/ + +/-- Symmetric Gaussian elimination (untrusted: its output is re-verified by `psdCert`). -/ +def ldlAux : ℕ → List (List ℚ) → ℕ → List (ℚ × List ℚ) + | 0, _, _ => [] + | _ + 1, [], _ => [] + | f + 1, (r :: rs), s => match r with + | [] => [] + | d :: a => + (d, List.replicate s 0 ++ (1 :: a.map (· / d))) :: + ldlAux f (rs.map (fun row => match row with + | [] => [] + | x :: xs => List.zipWith (fun y aj => y - x * aj / d) xs a)) (s + 1) + +def mget (A : List (List ℚ)) (j k : ℕ) : ℚ := (A.getD j []).getD k 0 + +/-- `A = sum_s d_s v_s v_s^T` entrywise on `n x n`, every `d_s >= 0`. -/ +def psdCert (A : List (List ℚ)) (n : ℕ) : Bool := + (ldlAux n A 0).all (fun p => decide (0 ≤ p.1)) && + (List.range n).all (fun j => (List.range n).all (fun k => + decide (mget A j k = ((ldlAux n A 0).map (fun p => p.1 * p.2.getD j 0 * p.2.getD k 0)).sum))) + +/-! ## E. The inverse Gram matrices (data). -/ + +def ginvData0 : List (List ℚ) := + [[23730337878975/1099511627776, -2175280972239375/1099511627776, 58732586250463125/1099511627776, -729962143398613125/1099511627776, 2514314049484111875/549755813888, -10560119007833269875/549755813888, 28431089636474188125/549755813888, -50092872216644998125/549755813888, 114918942144067936875/1099511627776, -82660993472048866875/1099511627776, 33851644945696202625/1099511627776, -6021043567416320625/1099511627776], + [-2175280972239375/1099511627776, 358921360419496875/1099511627776, -11536758013483828125/1099511627776, 156130791782481140625/1099511627776, -565720661133925171875/549755813888, 2457258461438126259375/549755813888, -6776076363359681503125/549755813888, 12154888111391801015625/549755813888, -28276108132816716046875/1099511627776, 20566842423402634734375/1099511627776, -8499706502669372615625/1099511627776, 1523324022556329118125/1099511627776], + [58732586250463125/1099511627776, -11536758013483828125/1099511627776, 403786530471933984375/1099511627776, -5748451879264078359375/1099511627776, 21540902097022535390625/549755813888, -95833079996086924115625/549755813888, 269050090898105000859375/549755813888, -489394179221827777734375/549755813888, 1151241545407537724765625/1099511627776, -845028960439803905390625/1099511627776, 351887849210512026286875/1099511627776, -63471834273180379921875/1099511627776], + [-729962143398613125/1099511627776, 156130791782481140625/1099511627776, -5748451879264078359375/1099511627776, 84634899207011122921875/1099511627776, -324836803623099833690625/549755813888, 1471319639939922776128125/549755813888, -4188685099350497855484375/549755813888, 7704462650035060158046875/549755813888, -18289724377909316723015625/1099511627776, 13527223598720380917493125/1099511627776, -5669304237280471534621875/1099511627776, 1028243715225522154734375/1099511627776], + [2514314049484111875/549755813888, -565720661133925171875/549755813888, 21540902097022535390625/549755813888, -324836803623099833690625/549755813888, 1269320283065053971984375/274877906944, -5829965791340897015184375/274877906944, 16783234853860158074015625/274877906944, -31152827237098286726015625/274877906944, 74517562751139101848629375/549755813888, -55468774015916905878609375/549755813888, 23375407126126870317628125/549755813888, -4259866820220020355328125/549755813888], + [-10560119007833269875/549755813888, 2457258461438126259375/549755813888, -95833079996086924115625/549755813888, 1471319639939922776128125/549755813888, -5829965791340897015184375/274877906944, 27076952230894388359411875/274877906944, -78662292054179349581690625/274877906944, 147124418765069508778063125/274877906944, -354188415545537706317559375/549755813888, 265102485469175281199146875/549755813888, -112252223898153336385513125/549755813888, 20542024444172098157915625/549755813888], + [28431089636474188125/549755813888, -6776076363359681503125/549755813888, 269050090898105000859375/549755813888, -4188685099350497855484375/549755813888, 16783234853860158074015625/274877906944, -78662292054179349581690625/274877906944, 230265982194961368775494375/274877906944, -433447361681602088150859375/274877906944, 1049241544484429882351390625/549755813888, -789088043258688886853765625/549755813888, 335519732588144269912621875/549755813888, -61626073332516294473746875/549755813888], + [-50092872216644998125/549755813888, 12154888111391801015625/549755813888, -489394179221827777734375/549755813888, 7704462650035060158046875/549755813888, -31152827237098286726015625/274877906944, 147124418765069508778063125/274877906944, -433447361681602088150859375/274877906944, 10665367347781292760165234375/3573412790272, -1995455826359080580934140625/549755813888, 1506966343019840414953828125/549755813888, -643123380675234150020896875/549755813888, 118511679485608258603359375/549755813888], + [114918942144067936875/1099511627776, -28276108132816716046875/1099511627776, 1151241545407537724765625/1099511627776, -18289724377909316723015625/1099511627776, 74517562751139101848629375/549755813888, -354188415545537706317559375/549755813888, 1049241544484429882351390625/549755813888, -1995455826359080580934140625/549755813888, 4873749684986118024948234375/1099511627776, -3694220349460065931515384375/1099511627776, 1581735882201251558159503125/1099511627776, -292328809397833704554953125/1099511627776], + [-82660993472048866875/1099511627776, 20566842423402634734375/1099511627776, -845028960439803905390625/1099511627776, 13527223598720380917493125/1099511627776, -55468774015916905878609375/549755813888, 265102485469175281199146875/549755813888, -789088043258688886853765625/549755813888, 1506966343019840414953828125/549755813888, -3694220349460065931515384375/1099511627776, 2809330260453203291851921875/1099511627776, -1206381766364654908862728125/1099511627776, 223545560127755185836140625/1099511627776], + [33851644945696202625/1099511627776, -8499706502669372615625/1099511627776, 351887849210512026286875/1099511627776, -5669304237280471534621875/1099511627776, 23375407126126870317628125/549755813888, -112252223898153336385513125/549755813888, 335519732588144269912621875/549755813888, -643123380675234150020896875/549755813888, 1581735882201251558159503125/1099511627776, -1206381766364654908862728125/1099511627776, 519410069882805207230499375/1099511627776, -96477557528820659150334375/1099511627776], + [-6021043567416320625/1099511627776, 1523324022556329118125/1099511627776, -63471834273180379921875/1099511627776, 1028243715225522154734375/1099511627776, -4259866820220020355328125/549755813888, 20542024444172098157915625/549755813888, -61626073332516294473746875/549755813888, 118511679485608258603359375/549755813888, -292328809397833704554953125/1099511627776, 223545560127755185836140625/1099511627776, -96477557528820659150334375/1099511627776, 17959025860343239582096875/1099511627776]] + +def ginvData1 : List (List ℚ) := + [[45232685623125/17179869184, -1872633184797375/17179869184, 6687975659990625/4294967296, -46815829619934375/4294967296, 370270652448571875/8589934592, -882953094300440625/8589934592, 647498935820323125/4294967296, -571322590429696875/4294967296, 1112575570836778125/17179869184, -229579086045684375/17179869184], + [-1872633184797375/17179869184, 92294064107870625/17179869184, -358921360419496875/4294967296, 2642966381270840625/4294967296, -21618109631420465625/8589934592, 52800595039166349375/8589934592, -39421258739649084375/4294967296, 35271652556528128125/4294967296, -69456503493667434375/17179869184, 14463482420878115625/17179869184], + [6687975659990625/4294967296, -358921360419496875/4294967296, 1468314656261578125/1073741824, -11181780843838171875/1073741824, 93678475069488684375/2147483648, -232943801643380953125/2147483648, 176358262782640640625/1073741824, -159562237755722484375/1073741824, 317084037688481765625/4294967296, -66532019136039331875/4294967296], + [-46815829619934375/4294967296, 2642966381270840625/4294967296, -11181780843838171875/1073741824, 87217890581937740625/1073741824, -743917302022410140625/2147483648, 1875810613233541359375/2147483648, -1436060139801502359375/1073741824, 1311185345036154328125/1073741824, -2625455832060629019375/4294967296, 554433492800327765625/4294967296], + [370270652448571875/8589934592, -21618109631420465625/8589934592, 93678475069488684375/2147483648, -743917302022410140625/2147483648, 6434232103456985953125/4294967296, -16405899172883829984375/4294967296, 12674791668682825171875/2147483648, -11660808335188199158125/2147483648, 23499450348690815296875/8589934592, -4989901435202949890625/8589934592], + [-882953094300440625/8589934592, 52800595039166349375/8589934592, -232943801643380953125/2147483648, 1875810613233541359375/2147483648, -16405899172883829984375/4294967296, 42214388780819657390625/4294967296, -32862278035530379445625/2147483648, 30428035218083684671875/2147483648, -61658432419605681515625/8589934592, 13155194692807776984375/8589934592], + [647498935820323125/4294967296, -39421258739649084375/4294967296, 176358262782640640625/1073741824, -1436060139801502359375/1073741824, 12674791668682825171875/2147483648, -32862278035530379445625/2147483648, 334708387398920531390625/13958643712, -311625050336926011984375/13958643712, 634485159414652013015625/55834574848, -10456693217360027859375/4294967296], + [-571322590429696875/4294967296, 35271652556528128125/4294967296, -159562237755722484375/1073741824, 1311185345036154328125/1073741824, -11660808335188199158125/2147483648, 30428035218083684671875/2147483648, -311625050336926011984375/13958643712, 291520208379704978953125/13958643712, -596031513389521587984375/55834574848, 9859167890653740553125/4294967296], + [1112575570836778125/17179869184, -69456503493667434375/17179869184, 317084037688481765625/4294967296, -2625455832060629019375/4294967296, 23499450348690815296875/8589934592, -61658432419605681515625/8589934592, 634485159414652013015625/55834574848, -596031513389521587984375/55834574848, 1223116769493455225090625/223338299392, -20298286833698877609375/17179869184], + [-229579086045684375/17179869184, 14463482420878115625/17179869184, -66532019136039331875/4294967296, 554433492800327765625/4294967296, -4989901435202949890625/8589934592, 13155194692807776984375/8589934592, -10456693217360027859375/4294967296, 9859167890653740553125/4294967296, -20298286833698877609375/17179869184, 4392026975712622640625/17179869184]] + +def ginv (par : ℕ) : List (List ℚ) := if par = 0 then ginvData0 else ginvData1 + +def ginvCheck (par N : ℕ) : Bool := + (List.range N).all (fun j => (List.range N).all (fun k => + decide ((∑ l ∈ range N, Gm par j l * mget (ginv par) l k) = if j = k then 1 else 0))) + +/-! ## F. Side conditions. -/ + +def pieceCheck : Bool := + (List.range nPc).all (fun i => (List.range nS).all (fun j => + decide (phw i < smax (bS j) (pcen i)) && decide (deg i j ≤ Dmax))) + +/-- The head truncation error: pole (Mp terms) and transform (Mt terms) remainders. -/ +def Ehead (par : ℕ) : ℚ := + 2 * piHiQ * (2 * (ellQ / 2) ^ (2 * Mp + par) / ((2 * Mp + par).factorial : ℚ)) + * (2 * CpQ + 2 * (ellQ / 2) ^ (2 * Mp + par) / ((2 * Mp + par).factorial : ℚ)) + + S0Q * (2 * (2 * ellQ ^ (2 * Mt + par) * TQ ^ (2 * Mt + par + 1) + / ((2 * Mt + par + 1) * ((2 * Mt + par).factorial : ℚ))) + + 4 * ellQ ^ (2 * (2 * Mt + par)) * TQ ^ (2 * (2 * Mt + par) + 1) + / ((2 * (2 * Mt + par) + 1) * ((2 * Mt + par).factorial : ℚ) ^ 2)) + +/-- Tail constants after `N` head modes: pole remainder, `int_0^T eps_N`, `int_0^T eps_N^2`. -/ +def dPT (par N : ℕ) : ℚ := 2 * (ellQ / 2) ^ (2 * N + par) / ((2 * N + par).factorial : ℚ) +def I1T (par N : ℕ) : ℚ := + 2 * ellQ ^ (2 * N + par) * TQ ^ (2 * N + par + 1) / ((2 * N + par + 1) * ((2 * N + par).factorial : ℚ)) +def I2T (par N : ℕ) : ℚ := + 4 * ellQ ^ (2 * (2 * N + par)) * TQ ^ (2 * (2 * N + par) + 1) + / ((2 * (2 * N + par) + 1) * ((2 * N + par).factorial : ℚ) ^ 2) +/-- Coupling constant `|R(h, r)| <= kapT A1(h) A1(r)` (uses `1/pi <= 1/3`). -/ +def kapT (par N : ℕ) : ℚ := 2 * CpQ * dPT par N + S0Q / 3 * I1T par N +/-- Tail floor `R(r, r) >= dT * int r^2`. -/ +def dT (par N : ℕ) : ℚ := beta0Q - 2 * ellQ * (2 * dPT par N ^ 2 + S0Q / 3 * I2T par N) + +def lamE : ℚ := 915 / 10 ^ 6 +def lamO : ℚ := 1 / 100 +/-- The window floor certified in both sectors. -/ +def lamFloor : ℚ := 9 / 10000 + +def tailCond (par N : ℕ) (lam : ℚ) : Bool := + decide (lamFloor ≤ lam) && decide (lamFloor ≤ dT par N) && + decide (4 * kapT par N ^ 2 * ellQ ^ 2 ≤ (lam - lamFloor) * (dT par N - lamFloor)) && + decide (Ehead par ≤ Econst) && decide (lam < beta0Q) && + decide (TQ * ellQ ≤ ((2 * N + par + 1 : ℕ) : ℚ) / 2) && decide (TQ * ellQ ≤ ((2 * Mt + par + 1 : ℕ) : ℚ) / 2) + +/-! ## H. Soundness of the elementary computable pieces. -/ + +theorem getD_map_range {α : Type*} (f : ℕ → α) {n i : ℕ} (d : α) (h : i < n) : + ((List.range n).map f).getD i d = f i := by + rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range h] + rfl + +theorem mget_map_range (f : ℕ → ℕ → ℚ) {n m j k : ℕ} (hj : j < n) (hk : k < m) : + mget ((List.range n).map (fun j => (List.range m).map (f j))) j k = f j k := by + unfold mget + rw [getD_map_range _ _ hj, getD_map_range _ _ hk] + +theorem floorR_le (q : ℚ) (R : ℕ) : floorR q R ≤ q := by + unfold floorR + have h := Int.floor_le (q * 10 ^ R) + have hp : (0 : ℚ) < 10 ^ R := by positivity + rw [div_le_iff₀ hp] + exact h + +theorem sub_floorR_le (q : ℚ) (R : ℕ) : q - floorR q R ≤ 1 / 10 ^ R := by + unfold floorR + have h := Int.lt_floor_add_one (q * 10 ^ R) + have hp : (0 : ℚ) < 10 ^ R := by positivity + have e : q - (⌊q * 10 ^ R⌋ : ℚ) / 10 ^ R = (q * 10 ^ R - (⌊q * 10 ^ R⌋ : ℚ)) / 10 ^ R := by + field_simp + rw [e, div_le_div_iff_of_pos_right hp] + linarith + +theorem le_ceilR (q : ℚ) (R : ℕ) : q ≤ ceilR q R := by + unfold ceilR + have h := Int.le_ceil (q * 10 ^ R) + have hp : (0 : ℚ) < 10 ^ R := by positivity + rw [le_div_iff₀ hp] + exact h + +theorem gpow_cast (x y : ℚ) (n : ℕ) : + ((gpow x y n).1 : ℂ) + ((gpow x y n).2 : ℂ) * Complex.I = ((x : ℂ) + (y : ℂ) * Complex.I) ^ n := by + induction n with + | zero => simp [gpow] + | succ n ih => + rcases hgp : gpow x y n with ⟨p, q⟩ + rw [hgp] at ih + simp only [gpow, hgp] + rw [pow_succ, ← ih] + push_cast + linear_combination (-(q : ℂ) * (y : ℂ)) * Complex.I_sq + +theorem re_I_pow_mul (k : ℕ) (P Q : ℝ) : + (Complex.I ^ k * ((P : ℂ) + (Q : ℂ) * Complex.I)).re + = if k % 4 = 0 then P else if k % 4 = 1 then -Q else if k % 4 = 2 then -P else Q := by + have hk : Complex.I ^ k = Complex.I ^ (k % 4) := by + conv_lhs => rw [← Nat.div_add_mod k 4, pow_add, pow_mul, Complex.I_pow_four, one_pow, one_mul] + rw [hk] + have h4 : k % 4 < 4 := Nat.mod_lt _ (by norm_num) + interval_cases (k % 4) <;> simp [pow_succ, Complex.mul_re, Complex.mul_im] + +/-- `kap` is the Taylor coefficient: `kap b c k = 2 Re (I^k / (b - c I)^(k+1))` (`b > 0`). -/ +theorem kap_eq {b c : ℚ} (hb : 0 < b) (k : ℕ) : + ((kap b c k : ℚ) : ℝ) = 2 * (Complex.I ^ k / ((b : ℂ) - (c : ℂ) * Complex.I) ^ (k + 1)).re := by + have hn : (0 : ℚ) < b * b + c * c := by nlinarith [mul_pos hb hb, mul_self_nonneg c] + have hz : ((b : ℂ) - (c : ℂ) * Complex.I) ≠ 0 := by + intro h + have := congrArg Complex.re h + simp at this + exact absurd this (by exact_mod_cast hb.ne') + have hinv : ((b : ℂ) - (c : ℂ) * Complex.I)⁻¹ + = (((b / (b * b + c * c) : ℚ) : ℂ) + ((c / (b * b + c * c) : ℚ) : ℂ) * Complex.I) := by + apply inv_eq_of_mul_eq_one_right + have hnC : ((b * b + c * c : ℚ) : ℂ) ≠ 0 := by exact_mod_cast hn.ne' + have e1 : (((b / (b * b + c * c) : ℚ) : ℂ) + ((c / (b * b + c * c) : ℚ) : ℂ) * Complex.I) + = ((b : ℂ) + (c : ℂ) * Complex.I) / ((b * b + c * c : ℚ) : ℂ) := by push_cast; ring + have e2 : ((b : ℂ) - (c : ℂ) * Complex.I) * ((b : ℂ) + (c : ℂ) * Complex.I) + = ((b * b + c * c : ℚ) : ℂ) := by + push_cast; linear_combination (-(c : ℂ) ^ 2) * Complex.I_sq + rw [e1, mul_div_assoc', e2, div_self hnC] + have hdiv : Complex.I ^ k / ((b : ℂ) - (c : ℂ) * Complex.I) ^ (k + 1) + = Complex.I ^ k * ((((gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).1 : ℚ) : ℝ) : ℂ) + + Complex.I ^ k * (((((gpow (b / (b * b + c * c)) (c / (b * b + c * c)) (k + 1)).2 : ℚ) : ℝ) : ℂ) + * Complex.I) := by + rw [div_eq_mul_inv, ← inv_pow, hinv, ← mul_add] + congr 1 + rw [← gpow_cast] + push_cast + ring + rw [hdiv, ← mul_add, re_I_pow_mul] + unfold kap + split_ifs <;> push_cast <;> ring + +/-! ## I. Soundness of the LDL^T certificate. -/ + +theorem sum_quad_cert (n : ℕ) (x : ℕ → ℝ) (C : List (ℚ × List ℚ)) : + ∑ j ∈ range n, ∑ k ∈ range n, x j * x k + * (((C.map (fun p => p.1 * p.2.getD j 0 * p.2.getD k 0)).sum : ℚ) : ℝ) + = (C.map (fun p => (p.1 : ℝ) * (∑ j ∈ range n, x j * (p.2.getD j 0 : ℝ)) ^ 2)).sum := by + induction C with + | nil => simp + | cons p C ih => + simp only [List.map_cons, List.sum_cons, Rat.cast_add, Rat.cast_mul, mul_add, + Finset.sum_add_distrib, ih] + congr 1 + rw [sq, Finset.sum_mul_sum, Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + ring + +theorem psdCert_sound {A : List (List ℚ)} {n : ℕ} (h : psdCert A n = true) (x : ℕ → ℝ) : + 0 ≤ ∑ j ∈ range n, ∑ k ∈ range n, x j * x k * ((mget A j k : ℚ) : ℝ) := by + unfold psdCert at h + rw [Bool.and_eq_true, List.all_eq_true, List.all_eq_true] at h + obtain ⟨hpos, heq⟩ := h + have hA : ∀ j ∈ range n, ∀ k ∈ range n, mget A j k + = ((ldlAux n A 0).map (fun p => p.1 * p.2.getD j 0 * p.2.getD k 0)).sum := by + intro j hj k hk + have := heq j (List.mem_range.mpr (Finset.mem_range.mp hj)) + rw [List.all_eq_true] at this + exact of_decide_eq_true (this k (List.mem_range.mpr (Finset.mem_range.mp hk))) + rw [Finset.sum_congr rfl fun j hj => Finset.sum_congr rfl fun k hk => by rw [hA j hj k hk], + sum_quad_cert] + apply List.sum_nonneg + intro y hy + rw [List.mem_map] at hy + obtain ⟨p, hp, rfl⟩ := hy + have := of_decide_eq_true (hpos p hp) + have h0 : (0 : ℝ) ≤ (p.1 : ℝ) := by exact_mod_cast this + positivity + +/-! ## J. Extraction of the side conditions. -/ + +theorem ginvCheck_sound {par N : ℕ} (h : ginvCheck par N = true) {j k : ℕ} (hj : j < N) (hk : k < N) : + (∑ l ∈ range N, Gm par j l * mget (ginv par) l k) = if j = k then 1 else 0 := by + unfold ginvCheck at h + rw [List.all_eq_true] at h + have := h j (List.mem_range.mpr hj) + rw [List.all_eq_true] at this + exact of_decide_eq_true (this k (List.mem_range.mpr hk)) + +theorem pieceCheck_sound (h : pieceCheck = true) {i j : ℕ} (hi : i < nPc) (hj : j < nS) : + phw i < smax (bS j) (pcen i) ∧ deg i j ≤ Dmax := by + unfold pieceCheck at h + rw [List.all_eq_true] at h + have := h i (List.mem_range.mpr hi) + rw [List.all_eq_true] at this + have h2 := this j (List.mem_range.mpr hj) + rw [Bool.and_eq_true] at h2 + exact ⟨of_decide_eq_true h2.1, of_decide_eq_true h2.2⟩ + +theorem tailCond_sound {par N : ℕ} {lam : ℚ} (h : tailCond par N lam = true) : + lamFloor ≤ lam ∧ lamFloor ≤ dT par N + ∧ 4 * kapT par N ^ 2 * ellQ ^ 2 ≤ (lam - lamFloor) * (dT par N - lamFloor) + ∧ Ehead par ≤ Econst ∧ lam < beta0Q + ∧ TQ * ellQ ≤ ((2 * N + par + 1 : ℕ) : ℚ) / 2 ∧ TQ * ellQ ≤ ((2 * Mt + par + 1 : ℕ) : ℚ) / 2 := by + unfold tailCond at h + simp only [Bool.and_eq_true, decide_eq_true_eq] at h + obtain ⟨⟨⟨⟨⟨⟨h1, h2⟩, h3⟩, h4⟩, h5⟩, h6⟩, h7⟩ := h + exact ⟨h1, h2, h3, h4, h5, h6, h7⟩ + +end KWin diff --git a/telperion/examples/rvm_bridge/lean/KWin_Head.lean b/telperion/examples/rvm_bridge/lean/KWin_Head.lean new file mode 100644 index 000000000..303c8e287 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Head.lean @@ -0,0 +1,554 @@ +/- + KWin_Head -- the head inequality of the prime-free window certificate (rvm_bridge island, + 2026-09-24). + + conjecture1_proved = False. (Finite-window Weil positivity is not RH; PR #604: the 1.3e-3 + full-class margin at this window is zero content; not Connes-Consani, whose theorem is for the + pole-free class.) + + THE FORM. For a sector par (0 even / 1 odd, eps = +1 / -1) and continuous f, g, + Rb par f g = 2 eps Pl f Pl g + beta0 int_{-l}^{l} f g + + (1/pi) int_0^20 (Psi(t) - beta0) Tr f t Tr g t dt, + with l = 26/75, Tr f t = int_{-l}^{l} f(x) phiF(t x) (cosine / sine transform), Pl f = + int f cosh(x/2) (resp. sinh(x/2)). KWin_Split shows Q(v) >= Rb par v v (Zhu split at T = 20). + + PROVED HERE (`head_floor`): for the head polynomials h = sum_{k= sum_{j,k} a_j a_k headEntry_{jk}, + where headEntry is the exact-rational matrix of KWin_Data whose kernel LDL^T certificate + (KWin_Cert) makes the right side >= 0; hence Rb h h >= lam int h^2. The inequality chain: + pole and transform Taylor truncations (KWin_Taylor; errors Ehead <= 1e-6 absorbed through + (int |h|)^2 <= 2 l int h^2), Psi >= w_i on every piece (KWin_Minorant), and exact polynomial + moments of (w_i - beta0) t^q (integral_pow). No `sorry`. +-/ +import KWin_Minorant +import KWin_Taylor + +open Real Finset MeasureTheory intervalIntegral + +noncomputable section + +namespace KWin +open RvMBridge11 + +/-! ## A. The form. -/ + +def ellR : ℝ := ((ellQ : ℚ) : ℝ) +lemma ellR_eq : ellR = 26 / 75 := by unfold ellR ellQ; push_cast; norm_num +lemma ellR_pos : 0 < ellR := by rw [ellR_eq]; norm_num + +def epsR (par : ℕ) : ℝ := if par = 0 then 1 else -1 +def beta0R : ℝ := ((beta0Q : ℚ) : ℝ) + +/-- The split form `R(f, g)` of the Weil form on the window (KWin_Split: `Q(v) >= Rb v v`). -/ +def Rb (par : ℕ) (f g : ℝ → ℝ) : ℝ := + 2 * epsR par * Pl ellR par f * Pl ellR par g + beta0R * ip ellR f g + + (1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par f t * Tr ellR par g t) + +/-- The head polynomials. -/ +def hfun (par N : ℕ) (a : ℕ → ℝ) (x : ℝ) : ℝ := ∑ k ∈ range N, a k * (x / ellR) ^ (2 * k + par) + +lemma continuous_hfun (par N : ℕ) (a : ℕ → ℝ) : Continuous (hfun par N a) := by + unfold hfun; fun_prop + +lemma continuous_Psi : Continuous Psi := by + unfold Psi; exact continuous_psiR.sub continuous_const + +/-! ## B. Moments of the head polynomials. -/ + +lemma int_pow_div_even (n : ℕ) : + ∫ x in (-ellR)..ellR, (x / ellR) ^ (2 * n) = 2 * ellR / (2 * n + 1) := by + have hl := ellR_pos + have h := intervalIntegral.integral_comp_div (a := -ellR) (b := ellR) + (fun x : ℝ => x ^ (2 * n)) hl.ne' + rw [h, integral_pow, smul_eq_mul, neg_div, div_self hl.ne'] + have e : (-1 : ℝ) ^ (2 * n + 1) = -1 := by rw [pow_succ, pow_mul]; norm_num + rw [e] + push_cast + field_simp + ring + +lemma mo_hfun (par N : ℕ) (a : ℕ → ℝ) (m : ℕ) : + mo ellR (hfun par N a) (2 * m + par) = ∑ k ∈ range N, a k * ((Gm par k m : ℚ) : ℝ) := by + unfold mo hfun + simp_rw [Finset.sum_mul] + rw [intervalIntegral.integral_finsetSum fun k _ => Continuous.intervalIntegrable (by fun_prop) _ _] + refine Finset.sum_congr rfl fun k _ => ?_ + have e : ∀ x : ℝ, a k * (x / ellR) ^ (2 * k + par) * (x / ellR) ^ (2 * m + par) + = a k * (x / ellR) ^ (2 * (k + m + par)) := by + intro x + rw [mul_assoc, ← pow_add] + congr 2 + ring + simp_rw [e] + rw [intervalIntegral.integral_const_mul, int_pow_div_even] + unfold Gm ellR + push_cast + ring + +lemma ip_hfun_left (par N : ℕ) (a : ℕ → ℝ) {g : ℝ → ℝ} (hg : Continuous g) : + ip ellR (hfun par N a) g = ∑ k ∈ range N, a k * mo ellR g (2 * k + par) := by + unfold ip hfun mo + simp_rw [Finset.sum_mul] + rw [intervalIntegral.integral_finsetSum fun k _ => Continuous.intervalIntegrable (by fun_prop) _ _] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [← intervalIntegral.integral_const_mul] + congr 1 + funext x + ring + +lemma Gm_symm (par j k : ℕ) : Gm par j k = Gm par k j := by + unfold Gm; ring + +lemma ip_hfun_self (par N : ℕ) (a : ℕ → ℝ) : + ip ellR (hfun par N a) (hfun par N a) + = ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((Gm par j k : ℚ) : ℝ) := by + rw [ip_hfun_left par N a (continuous_hfun par N a)] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [mo_hfun, Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [Gm_symm par k j] + ring + +/-! ## C. The quadratic form of the certified matrix. -/ + +lemma quad_outer (N : ℕ) (a u : ℕ → ℝ) (C : ℝ) : + ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * (C * u j * u k) + = C * (∑ j ∈ range N, a j * u j) ^ 2 := by + rw [sq, Finset.sum_mul_sum, Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + ring + +lemma quad_hankel (N M : ℕ) (a : ℕ → ℝ) (B : ℕ → ℕ → ℝ) (W : ℕ → ℝ) : + ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ∑ m ∈ range M, B m j * ∑ m' ∈ range M, W (m + m') * B m' k + = ∑ m ∈ range M, ∑ m' ∈ range M, + W (m + m') * (∑ j ∈ range N, B m j * a j) * (∑ k ∈ range N, B m' k * a k) := by + have hF : ∀ j k, a j * a k * ∑ m ∈ range M, B m j * ∑ m' ∈ range M, W (m + m') * B m' k + = ∑ m ∈ range M, ∑ m' ∈ range M, a j * a k * B m j * W (m + m') * B m' k := by + intro j k + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun m _ => ?_ + rw [Finset.mul_sum, Finset.mul_sum] + refine Finset.sum_congr rfl fun m' _ => ?_ + ring + simp_rw [hF] + conv_lhs => enter [2, j]; rw [Finset.sum_comm] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun m _ => ?_ + conv_lhs => enter [2, j]; rw [Finset.sum_comm] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun m' _ => ?_ + rw [mul_assoc, Finset.sum_mul_sum, Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + ring + +/-- The certified quadratic form, expanded. -/ +lemma quad_headEntry {par N : ℕ} (lam : ℚ) (a : ℕ → ℝ) : + ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((headEntry par N lam j k : ℚ) : ℝ) + = 2 * ((piEQ par : ℚ) : ℝ) * ((epsQ par : ℚ) : ℝ) + * (∑ j ∈ range N, a j * ((pv par j : ℚ) : ℝ)) ^ 2 + + ((diagc lam : ℚ) : ℝ) * ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((Gm par j k : ℚ) : ℝ) + + ∑ m ∈ range Mt, ∑ m' ∈ range Mt, (((momList par).getD (m + m') 0 : ℚ) : ℝ) + * (∑ j ∈ range N, ((Bm par m j : ℚ) : ℝ) * a j) + * (∑ k ∈ range N, ((Bm par m' k : ℚ) : ℝ) * a k) := by + have hentry : ∀ j ∈ range N, ∀ k ∈ range N, ((headEntry par N lam j k : ℚ) : ℝ) + = 2 * ((piEQ par : ℚ) : ℝ) * ((epsQ par : ℚ) : ℝ) * ((pv par j : ℚ) : ℝ) * ((pv par k : ℚ) : ℝ) + + ((diagc lam : ℚ) : ℝ) * ((Gm par j k : ℚ) : ℝ) + + ∑ m ∈ range Mt, ((Bm par m j : ℚ) : ℝ) * ∑ m' ∈ range Mt, + (((momList par).getD (m + m') 0 : ℚ) : ℝ) * ((Bm par m' k : ℚ) : ℝ) := by + intro j _ k hk + unfold headEntry + push_cast + congr 1 + refine Finset.sum_congr rfl fun m hm => ?_ + congr 1 + unfold WBmat + rw [getD_map_range _ _ (Finset.mem_range.mp hm)] + unfold WBrow + rw [getD_map_range _ _ (Finset.mem_range.mp hk)] + push_cast + rfl + rw [Finset.sum_congr rfl fun j hj => Finset.sum_congr rfl fun k hk => by rw [hentry j hj k hk]] + simp only [mul_add, Finset.sum_add_distrib] + rw [quad_outer N a (fun j => ((pv par j : ℚ) : ℝ)) (2 * ((piEQ par : ℚ) : ℝ) * ((epsQ par : ℚ) : ℝ)), + quad_hankel N Mt a (fun m j => ((Bm par m j : ℚ) : ℝ)) (fun s => (((momList par).getD s 0 : ℚ) : ℝ))] + congr 1 + congr 1 + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + ring + +/-! ## D. The pole term. -/ + +lemma pole_sq_bound {par : ℕ} (hpar : par = 0 ∨ par = 1) {P Pt A dP : ℝ} (hA : 0 ≤ A) + (hdP : 0 ≤ dP) (h1 : |P - Pt| ≤ dP * A) (h2 : |P| ≤ ((CpQ : ℚ) : ℝ) * A) : + 2 * ((piEQ par : ℚ) : ℝ) * ((epsQ par : ℚ) : ℝ) * Pt ^ 2 + - 2 * ((piHiQ : ℚ) : ℝ) * (dP * (2 * ((CpQ : ℚ) : ℝ) + dP)) * A ^ 2 + ≤ 2 * Real.pi * epsR par * P ^ 2 := by + have hlo := pi_gt_Q + have hhi := pi_lt_Q + have hCp : (0 : ℝ) ≤ ((CpQ : ℚ) : ℝ) := by unfold CpQ; push_cast; norm_num + have hd : |P ^ 2 - Pt ^ 2| ≤ dP * (2 * ((CpQ : ℚ) : ℝ) + dP) * A ^ 2 := by + have hPt : |Pt| ≤ (((CpQ : ℚ) : ℝ) + dP) * A := by + have := abs_sub_abs_le_abs_sub Pt P + rw [abs_sub_comm] at this + nlinarith [abs_nonneg P] + rw [sq_sub_sq, abs_mul] + have h3 : |P + Pt| ≤ (2 * ((CpQ : ℚ) : ℝ) + dP) * A := by + refine (abs_add_le _ _).trans ?_ + nlinarith + calc |P + Pt| * |P - Pt| ≤ ((2 * ((CpQ : ℚ) : ℝ) + dP) * A) * (dP * A) := + mul_le_mul h3 h1 (abs_nonneg _) (by positivity) + _ = dP * (2 * ((CpQ : ℚ) : ℝ) + dP) * A ^ 2 := by ring + have hE : 0 ≤ dP * (2 * ((CpQ : ℚ) : ℝ) + dP) * A ^ 2 := by positivity + rw [abs_le] at hd + have hpi0 : 0 < Real.pi := Real.pi_pos + rcases hpar with h | h <;> subst h + · simp only [piEQ, epsQ, epsR, if_true] + push_cast + have hPt2 : 0 ≤ Pt ^ 2 := sq_nonneg _ + nlinarith + · simp only [piEQ, epsQ, epsR, one_ne_zero, if_false] + push_cast + have hPt2 : 0 ≤ Pt ^ 2 := sq_nonneg _ + nlinarith + +/-! ## E. The transform term. -/ + +/-- The transform-truncation error weight `eps_M(t) = 2 (t l)^n / n!`. -/ +def epsW (n : ℕ) (t : ℝ) : ℝ := 2 * (t * ellR) ^ n / (n.factorial : ℝ) + +lemma continuous_epsW (n : ℕ) : Continuous (epsW n) := by unfold epsW; fun_prop + +lemma epsW_nonneg (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ epsW n t := by + unfold epsW; have := ellR_pos; positivity + +lemma int_epsW (n : ℕ) : + ∫ t in (0 : ℝ)..20, epsW n t + = 2 * ellR ^ n * 20 ^ (n + 1) / ((n + 1 : ℝ) * (n.factorial : ℝ)) := by + unfold epsW + have e : (fun t : ℝ => 2 * (t * ellR) ^ n / (n.factorial : ℝ)) + = fun t => (2 * ellR ^ n / (n.factorial : ℝ)) * t ^ n := by + funext t; rw [mul_pow]; ring + rw [e, intervalIntegral.integral_const_mul, integral_pow] + have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast Nat.factorial_pos n + field_simp + ring + +lemma int_epsW_sq (n : ℕ) : + ∫ t in (0 : ℝ)..20, epsW n t ^ 2 + = 4 * ellR ^ (2 * n) * 20 ^ (2 * n + 1) / ((2 * n + 1 : ℝ) * (n.factorial : ℝ) ^ 2) := by + unfold epsW + have e : (fun t : ℝ => (2 * (t * ellR) ^ n / (n.factorial : ℝ)) ^ 2) + = fun t => (4 * ellR ^ (2 * n) / (n.factorial : ℝ) ^ 2) * t ^ (2 * n) := by + funext t; ring + rw [e, intervalIntegral.integral_const_mul, integral_pow] + have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast Nat.factorial_pos n + push_cast + field_simp + ring + +/-- `int_0^20 (Psi - beta0) F^2 >= int_0^20 (Psi - beta0) G^2 - S0 (2 I1 + I2) A^2` when +`|F - G| <= eps_n A` and `|F| <= A` on `[0, 20]`. -/ +lemma int_sq_perturb {F G : ℝ → ℝ} (hF : Continuous F) (hG : Continuous G) {A : ℝ} (hA : 0 ≤ A) + (n : ℕ) (h1 : ∀ t ∈ Set.Icc (0 : ℝ) 20, |F t - G t| ≤ epsW n t * A) + (h2 : ∀ t ∈ Set.Icc (0 : ℝ) 20, |F t| ≤ A) : + (∫ t in (0 : ℝ)..20, (Psi t - beta0R) * G t ^ 2) + - ((S0Q : ℚ) : ℝ) * (2 * (∫ t in (0 : ℝ)..20, epsW n t) + ∫ t in (0 : ℝ)..20, epsW n t ^ 2) * A ^ 2 + ≤ ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * F t ^ 2 := by + have hcP : Continuous fun t => Psi t - beta0R := continuous_Psi.sub continuous_const + have hpt : ∀ t ∈ Set.Icc (0 : ℝ) 20, (Psi t - beta0R) * G t ^ 2 + - ((S0Q : ℚ) : ℝ) * (2 * epsW n t + epsW n t ^ 2) * A ^ 2 ≤ (Psi t - beta0R) * F t ^ 2 := by + intro t ht + have hS := abs_Psi_sub_beta0_le ht.1 ht.2 + have he := epsW_nonneg n ht.1 + have hd : |F t ^ 2 - G t ^ 2| ≤ epsW n t * (2 + epsW n t) * A ^ 2 := by + rw [sq_sub_sq, abs_mul] + have hFG := h1 t ht + have hFt := h2 t ht + have hsum : |F t + G t| ≤ (2 + epsW n t) * A := by + have : |G t| ≤ |F t| + |F t - G t| := by + have := abs_sub_abs_le_abs_sub (F t) (G t) + have := abs_sub_abs_le_abs_sub (G t) (F t) + rw [abs_sub_comm (G t)] at this + linarith + refine (abs_add_le _ _).trans ?_ + nlinarith + calc |F t + G t| * |F t - G t| ≤ ((2 + epsW n t) * A) * (epsW n t * A) := + mul_le_mul hsum hFG (abs_nonneg _) (by positivity) + _ = epsW n t * (2 + epsW n t) * A ^ 2 := by ring + have hprod : |(Psi t - beta0R) * (F t ^ 2 - G t ^ 2)| + ≤ ((S0Q : ℚ) : ℝ) * (epsW n t * (2 + epsW n t) * A ^ 2) := by + rw [abs_mul] + exact mul_le_mul hS hd (abs_nonneg _) (by unfold S0Q; push_cast; norm_num) + have := neg_abs_le ((Psi t - beta0R) * (F t ^ 2 - G t ^ 2)) + nlinarith + have hint1 : IntervalIntegrable (fun t => (Psi t - beta0R) * G t ^ 2 + - ((S0Q : ℚ) : ℝ) * (2 * epsW n t + epsW n t ^ 2) * A ^ 2) volume 0 20 := + Continuous.intervalIntegrable (by have := continuous_epsW n; fun_prop) _ _ + have hint2 : IntervalIntegrable (fun t => (Psi t - beta0R) * F t ^ 2) volume 0 20 := + Continuous.intervalIntegrable (by fun_prop) _ _ + have hmono := intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 20) hint1 hint2 hpt + have hce := continuous_epsW n + rw [intervalIntegral.integral_sub (Continuous.intervalIntegrable (by fun_prop) _ _) + (Continuous.intervalIntegrable (by fun_prop) _ _)] at hmono + have e1 : ∫ t in (0 : ℝ)..20, ((S0Q : ℚ) : ℝ) * (2 * epsW n t + epsW n t ^ 2) * A ^ 2 + = ((S0Q : ℚ) : ℝ) * (2 * (∫ t in (0 : ℝ)..20, epsW n t) + ∫ t in (0 : ℝ)..20, epsW n t ^ 2) + * A ^ 2 := by + rw [intervalIntegral.integral_mul_const, intervalIntegral.integral_const_mul, + intervalIntegral.integral_add (Continuous.intervalIntegrable (by fun_prop) _ _) + (Continuous.intervalIntegrable (by fun_prop) _ _), + intervalIntegral.integral_const_mul] + rw [e1] at hmono + exact hmono + +/-! ## F. The moments of the minorant. -/ + +lemma int_wpoly_mom {i : ℕ} (q : ℕ) : + ∫ t in ((brk i : ℚ) : ℝ)..((brk (i + 1) : ℚ) : ℝ), (wpoly i t - beta0R) * t ^ q + = ((momPiece i q : ℚ) : ℝ) := by + unfold wpoly momPiece beta0R + have e : (fun t : ℝ => (∑ p ∈ range (Dmax + 1), (((wpList i).getD p 0 : ℚ) : ℝ) * t ^ p + - ((beta0Q : ℚ) : ℝ)) * t ^ q) + = fun t => ∑ p ∈ range (Dmax + 1), (((wpList i).getD p 0 : ℚ) : ℝ) * t ^ (p + q) + - ((beta0Q : ℚ) : ℝ) * t ^ q := by + funext t + rw [sub_mul, Finset.sum_mul] + congr 1 + refine Finset.sum_congr rfl fun p _ => ?_ + rw [pow_add]; ring + rw [e, intervalIntegral.integral_sub (Continuous.intervalIntegrable (by fun_prop) _ _) + (Continuous.intervalIntegrable (by fun_prop) _ _), + intervalIntegral.integral_finsetSum fun p _ => Continuous.intervalIntegrable (by fun_prop) _ _, + intervalIntegral.integral_const_mul, integral_pow] + push_cast + congr 1 + · refine Finset.sum_congr rfl fun p _ => ?_ + rw [intervalIntegral.integral_const_mul, integral_pow] + push_cast + ring + · ring + +/-- `int_0^20 (Psi - beta0) (sum_m c_m t^(2m+par))^2 >= sum_{m,m'} W_{m+m'} c_m c_m'`. -/ +theorem moment_floor (par : ℕ) (c : ℕ → ℝ) : + ∑ m ∈ range Mt, ∑ m' ∈ range Mt, (((momList par).getD (m + m') 0 : ℚ) : ℝ) * c m * c m' + ≤ ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (∑ m ∈ range Mt, c m * t ^ (2 * m + par)) ^ 2 := by + set pt : ℝ → ℝ := fun t => ∑ m ∈ range Mt, c m * t ^ (2 * m + par) with hpt + have hptc : Continuous pt := by rw [hpt]; fun_prop + show _ ≤ ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * pt t ^ 2 + -- split [0, 20] into the pieces + have hbrk0 : ((brk 0 : ℚ) : ℝ) = 0 := by simp [brk] + have hbrk7 : ((brk nPc : ℚ) : ℝ) = 20 := by simp [brk, nPc] + have hsplit : ∀ F : ℝ → ℝ, Continuous F → + ∑ i ∈ range nPc, ∫ t in ((brk i : ℚ) : ℝ)..((brk (i + 1) : ℚ) : ℝ), F t + = ∫ t in (0 : ℝ)..20, F t := by + intro F hF + rw [intervalIntegral.sum_integral_adjacent_intervals (a := fun i => ((brk i : ℚ) : ℝ)) + fun k _ => hF.intervalIntegrable _ _] + rw [hbrk0, hbrk7] + rw [← hsplit (fun t => (Psi t - beta0R) * pt t ^ 2) + ((continuous_Psi.sub continuous_const).mul (hptc.pow 2))] + -- on each piece Psi >= w_i + have hpiece : ∀ i ∈ range nPc, + ∫ t in ((brk i : ℚ) : ℝ)..((brk (i + 1) : ℚ) : ℝ), (wpoly i t - beta0R) * pt t ^ 2 + ≤ ∫ t in ((brk i : ℚ) : ℝ)..((brk (i + 1) : ℚ) : ℝ), (Psi t - beta0R) * pt t ^ 2 := by + intro i hi + have hi' := Finset.mem_range.mp hi + have hle : ((brk i : ℚ) : ℝ) ≤ ((brk (i + 1) : ℚ) : ℝ) := by exact_mod_cast brk_le_succ hi' + apply intervalIntegral.integral_mono_on hle + · exact Continuous.intervalIntegrable (by unfold wpoly; fun_prop) _ _ + · exact Continuous.intervalIntegrable ((continuous_Psi.sub continuous_const).mul (hptc.pow 2)) _ _ + · intro t ht + exact mul_le_mul_of_nonneg_right (by linarith [wpoly_le_Psi hi' ht.1 ht.2]) (sq_nonneg _) + refine le_trans (le_of_eq ?_) (Finset.sum_le_sum hpiece) + -- expand the square and integrate the monomials + have hexp : ∀ i ∈ range nPc, + ∫ t in ((brk i : ℚ) : ℝ)..((brk (i + 1) : ℚ) : ℝ), (wpoly i t - beta0R) * pt t ^ 2 + = ∑ m ∈ range Mt, ∑ m' ∈ range Mt, c m * c m' * ((momPiece i (2 * (m + m') + 2 * par) : ℚ) : ℝ) := by + intro i _ + have e : (fun t : ℝ => (wpoly i t - beta0R) * pt t ^ 2) + = fun t => ∑ m ∈ range Mt, ∑ m' ∈ range Mt, + c m * c m' * ((wpoly i t - beta0R) * t ^ (2 * (m + m') + 2 * par)) := by + funext t + rw [hpt, sq, Finset.sum_mul_sum, Finset.mul_sum] + refine Finset.sum_congr rfl fun m _ => ?_ + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun m' _ => ?_ + have : t ^ (2 * (m + m') + 2 * par) = t ^ (2 * m + par) * t ^ (2 * m' + par) := by + rw [← pow_add]; congr 1; ring + rw [this]; ring + have hcw : Continuous fun t => wpoly i t - beta0R := by unfold wpoly; fun_prop + rw [e, intervalIntegral.integral_finsetSum fun m _ => Continuous.intervalIntegrable + (continuous_finsetSum _ fun m' _ => by fun_prop) _ _] + refine Finset.sum_congr rfl fun m _ => ?_ + rw [intervalIntegral.integral_finsetSum fun m' _ => Continuous.intervalIntegrable (by fun_prop) _ _] + refine Finset.sum_congr rfl fun m' _ => ?_ + rw [intervalIntegral.integral_const_mul, int_wpoly_mom] + rw [Finset.sum_congr rfl hexp] + conv_rhs => rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun m hm => ?_ + conv_rhs => rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun m' hm' => ?_ + have hs : m + m' < 2 * Mt := by + have := Finset.mem_range.mp hm; have := Finset.mem_range.mp hm'; omega + unfold momList + rw [getD_map_range _ _ hs] + unfold mom + push_cast + rw [Finset.sum_mul, Finset.sum_mul] + refine Finset.sum_congr rfl fun i _ => ?_ + ring + +/-! ## G. The head floor. -/ + +theorem head_floor {par N : ℕ} (hpar : par = 0 ∨ par = 1) {lam : ℚ} + (htail : tailCond par N lam = true) (hcert : psdCert (headMat par N lam) N = true) + (a : ℕ → ℝ) : + (lam : ℝ) * ip ellR (hfun par N a) (hfun par N a) ≤ Rb par (hfun par N a) (hfun par N a) := by + obtain ⟨_, _, _, hE, hlam, _, hM⟩ := tailCond_sound htail + set h := hfun par N a with hh + have hc : Continuous h := continuous_hfun par N a + have hl := ellR_pos + set X := ip ellR h h with hX + set A := A1 ellR h with hA + have hA0 : 0 ≤ A := A1_nonneg hl.le h + have hA2 : A ^ 2 ≤ 2 * ellR * X := by + have := A1_sq_le hl hc + rw [hX] + unfold ip + have e : (fun x => h x ^ 2) = fun x => h x * h x := by funext x; ring + rw [e] at this + exact this + have hX0 : 0 ≤ X := by + rw [hX]; unfold ip + exact intervalIntegral.integral_nonneg (by linarith) fun x _ => mul_self_nonneg _ + -- the pole term + set Pt := ∑ k ∈ range N, a k * ((pv par k : ℚ) : ℝ) with hPt + set dP : ℝ := 2 * (ellR / 2) ^ (2 * Mp + par) / ((2 * Mp + par).factorial : ℝ) with hdP + have hdP0 : 0 ≤ dP := by rw [hdP]; positivity + have hPt_eq : ∑ m ∈ range Mp, (ellR / 2) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo ellR h (2 * m + par) = Pt := by + rw [hPt, hh] + simp_rw [mo_hfun, Finset.mul_sum] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun k _ => ?_ + unfold pv + push_cast + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun m _ => ?_ + rw [Gm_symm par k m] + unfold ellR + ring + have hP1 : |Pl ellR par h - Pt| ≤ dP * A := by + have := Pl_sub_le hl (by rw [ellR_eq]; norm_num) hpar (M := Mp) (by unfold Mp; omega) hc + rw [hPt_eq] at this + rw [hdP]; exact this + have hP2 : |Pl ellR par h| ≤ ((CpQ : ℚ) : ℝ) * A := by + have h1 := abs_Pl_le hl par hc + have h2 := cosh_half_ell_le + rw [← ellR] at h2 + exact h1.trans (mul_le_mul_of_nonneg_right h2 hA0) + have hpole := pole_sq_bound hpar hA0 hdP0 hP1 hP2 + -- the transform term + set c : ℕ → ℝ := fun m => ∑ k ∈ range N, ((Bm par m k : ℚ) : ℝ) * a k with hcdef + set pt : ℝ → ℝ := fun t => ∑ m ∈ range Mt, c m * t ^ (2 * m + par) with hpt + have hptc : Continuous pt := by rw [hpt]; fun_prop + have hpt_eq : ∀ t, ∑ m ∈ range Mt, (-1) ^ m * (t * ellR) ^ (2 * m + par) + / ((2 * m + par).factorial : ℝ) * mo ellR h (2 * m + par) = pt t := by + intro t + rw [hpt] + refine Finset.sum_congr rfl fun m _ => ?_ + rw [hcdef, hh, mo_hfun] + simp only + rw [Finset.mul_sum, Finset.sum_mul] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [Gm_symm par k m] + unfold Bm + push_cast + rw [mul_pow] + unfold ellR + ring + have hT1 : ∀ t ∈ Set.Icc (0 : ℝ) 20, |Tr ellR par h t - pt t| ≤ epsW (2 * Mt + par) t * A := by + intro t ht + have htl : t * ellR ≤ (2 * Mt + par + 1) / 2 := by + have h1 : t * ellR ≤ 20 * ellR := mul_le_mul_of_nonneg_right ht.2 hl.le + have h2 := (Rat.cast_le (K := ℝ)).mpr hM + unfold TQ at h2 + push_cast at h2 + have e : (20 : ℝ) * ellR = (20 : ℝ) * ((ellQ : ℚ) : ℝ) := rfl + linarith + have := Tr_sub_le hl hpar hc ht.1 htl + rw [hpt_eq] at this + unfold epsW + exact this + have hT2 : ∀ t ∈ Set.Icc (0 : ℝ) 20, |Tr ellR par h t| ≤ A := fun t _ => abs_Tr_le hl par hc t + have hint := int_sq_perturb (continuous_Tr ellR par hc) hptc hA0 (2 * Mt + par) hT1 hT2 + have hmom := moment_floor par c + -- the error constant + have hEle : 2 * ((piHiQ : ℚ) : ℝ) * (dP * (2 * ((CpQ : ℚ) : ℝ) + dP)) + + ((S0Q : ℚ) : ℝ) * (2 * (∫ t in (0 : ℝ)..20, epsW (2 * Mt + par) t) + + ∫ t in (0 : ℝ)..20, epsW (2 * Mt + par) t ^ 2) ≤ ((Econst : ℚ) : ℝ) := by + rw [int_epsW, int_epsW_sq] + have h1 : ((Ehead par : ℚ) : ℝ) ≤ ((Econst : ℚ) : ℝ) := by exact_mod_cast hE + refine le_trans (le_of_eq ?_) h1 + unfold Ehead + rw [hdP] + unfold ellR TQ + push_cast + ring + -- the quadratic form + have hquad := quad_headEntry (par := par) (N := N) lam a + have hGX : ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((Gm par j k : ℚ) : ℝ) = X := by + rw [hX, hh, ip_hfun_self] + rw [hGX] at hquad + have hWc : ∑ m ∈ range Mt, ∑ m' ∈ range Mt, (((momList par).getD (m + m') 0 : ℚ) : ℝ) + * (∑ j ∈ range N, ((Bm par m j : ℚ) : ℝ) * a j) * (∑ k ∈ range N, ((Bm par m' k : ℚ) : ℝ) * a k) + = ∑ m ∈ range Mt, ∑ m' ∈ range Mt, (((momList par).getD (m + m') 0 : ℚ) : ℝ) * c m * c m' := rfl + rw [hWc] at hquad + have hpsd := psdCert_sound hcert a + have hmat : ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((mget (headMat par N lam) j k : ℚ) : ℝ) + = ∑ j ∈ range N, ∑ k ∈ range N, a j * a k * ((headEntry par N lam j k : ℚ) : ℝ) := by + refine Finset.sum_congr rfl fun j hj => Finset.sum_congr rfl fun k hk => ?_ + unfold headMat + rw [mget_map_range _ (Finset.mem_range.mp hj) (Finset.mem_range.mp hk)] + rw [hmat, hquad] at hpsd + -- assemble + have hpi := Real.pi_pos + have hlo := pi_gt_Q + have hbl : (lam : ℝ) < beta0R := by unfold beta0R; exact_mod_cast hlam + have hdiag : ((diagc lam : ℚ) : ℝ) = ((piLoQ : ℚ) : ℝ) * (beta0R - lam) - 2 * ellR * ((Econst : ℚ) : ℝ) := by + unfold diagc beta0R ellR; push_cast; ring + rw [hdiag] at hpsd + have hRb : Real.pi * (Rb par h h - (lam : ℝ) * X) + = 2 * Real.pi * epsR par * (Pl ellR par h) ^ 2 + Real.pi * (beta0R - lam) * X + + ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par h t) ^ 2 := by + unfold Rb + rw [← hX] + have e : (fun t => (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par h t)) + = fun t => (Psi t - beta0R) * (Tr ellR par h t) ^ 2 := by funext t; ring + rw [e] + field_simp + ring + have hfin : 0 ≤ Real.pi * (Rb par h h - (lam : ℝ) * X) := by + rw [hRb] + have hEc : 0 ≤ ((Econst : ℚ) : ℝ) := by unfold Econst; positivity + have h1 : ((piLoQ : ℚ) : ℝ) * (beta0R - lam) * X ≤ Real.pi * (beta0R - lam) * X := + mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_right hlo.le (by linarith)) hX0 + have h2 : ((S0Q : ℚ) : ℝ) * (2 * (∫ t in (0 : ℝ)..20, epsW (2 * Mt + par) t) + + ∫ t in (0 : ℝ)..20, epsW (2 * Mt + par) t ^ 2) * A ^ 2 + + 2 * ((piHiQ : ℚ) : ℝ) * (dP * (2 * ((CpQ : ℚ) : ℝ) + dP)) * A ^ 2 + ≤ ((Econst : ℚ) : ℝ) * (2 * ellR * X) := by + have := mul_le_mul hEle hA2 (sq_nonneg A) hEc + nlinarith + nlinarith + have := (mul_nonneg_iff_of_pos_left hpi).mp hfin + linarith + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Minorant.lean b/telperion/examples/rvm_bridge/lean/KWin_Minorant.lean new file mode 100644 index 000000000..b79c9d0c1 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Minorant.lean @@ -0,0 +1,597 @@ +/- + KWin_Minorant -- the proved piecewise-polynomial minorant w <= Psi of the Weil symbol on + [0, 20] (rvm_bridge island, 2026-09-24). + + conjecture1_proved = False. (Finite-window Weil positivity is not RH; PR #604: the 1.3e-3 + full-class margin is zero content; not Connes-Consani, whose theorem is pole-free.) + + STATEMENT (`wpoly_le_Psi`): for each of the 7 pieces [brk i, brk (i+1)] of [0, 20] and every t + in it, wpoly i t = sum_p wpCoef i p t^p <= Psi t = Re psi(1/4 + it/2) - log pi, where the + coefficients wpCoef are the exact rationals computed by KWin_Data (and evaluated by the kernel + inside the head certificate). No pointwise digamma value is ever enclosed numerically. + + ROUTE. + 1. The island's series floor `psiR_ge_series` with N = 400 terms (the Lorentzian form: + psiR r >= -gamma + H_N - sum_{j<=N} Lz(j + 1/4, r) + serG(N) - serG(N + M)). + 2. Lorentzians j < 18: the GEOMETRIC Taylor bound `lor_taylor` about the piece centre c + (1/(b - i r) = (1/z) sum_{k<=d} q^k + q^(d+1)/(z (1 - q)), z = b - i c, q = i (r-c)/z), with + the coefficients `kap` floor-rounded at 10^-30 and the rounding paid by 10^-30 sum h^k. + 3. Lorentzians 18 <= j <= 400: the global alternating bound 1/(1+y) <= sum_{k<=10} (-y)^k, + summed with termwise ceilings / floors (`gAlt`). + 4. serG(N) >= (1/4)/(N+5/4) + (1/2)(y - y^2) (two log floors), serG(N+M) <= the island's + serG_bounds upper, gamma <= gammaUp (KWin_Constants), log pi <= 1.1447298859. + 5. The kernel-side coefficients are the shift-to-power expansion of steps 2-4 + (`wpoly_eq`: binomial theorem). + No `sorry`. +-/ +import KWin_Constants +import KWin_Cert + +open Real Finset + +noncomputable section + +namespace KWin +open RvMBridge11 RvMBridge30 + +/-- The Lorentzian `x / (x^2 + (r/2)^2)` of the vertical-line digamma series. -/ +def Lz (x r : ℝ) : ℝ := x / (x ^ 2 + (r / 2) ^ 2) + +/-- The minorant polynomial on piece `i`. -/ +def wpoly (i : ℕ) (t : ℝ) : ℝ := ∑ p ∈ range (Dmax + 1), (((wpList i).getD p 0 : ℚ) : ℝ) * t ^ p + +/-! ## A. The series floor in Lorentzian form. -/ + +theorem psi_series_Lz (r : ℝ) (N M : ℕ) : + -Real.eulerMascheroniConstant + (∑ n ∈ range N, (1 : ℝ) / ((n : ℝ) + 1)) + - (∑ j ∈ range (N + 1), Lz ((j : ℝ) + 1 / 4) r) + + (serG (r / 2) N - serG (r / 2) ((N : ℝ) + M)) ≤ psiR r := by + have h := psiR_ge_series r N M + have e1 : (∑ j ∈ range (N + 1), Lz ((j : ℝ) + 1 / 4) r) + = (∑ n ∈ range N, Lz ((n : ℝ) + 1 + 1 / 4) r) + Lz (1 / 4) r := by + rw [Finset.sum_range_succ'] + push_cast + simp only [zero_add] + have e2 : ∑ n ∈ range N, serF (r / 2) n + = ∑ n ∈ range N, (1 : ℝ) / ((n : ℝ) + 1) - ∑ n ∈ range N, Lz ((n : ℝ) + 1 + 1 / 4) r := by + rw [← Finset.sum_sub_distrib] + rfl + have e3 : (1 / 4 : ℝ) / ((1 / 4) ^ 2 + (r / 2) ^ 2) = Lz (1 / 4) r := rfl + rw [e2, e3] at h + rw [e1] + linarith + +/-! ## B. The geometric Taylor bound for one Lorentzian. -/ + +/-- `2b/(b^2 + r^2) <= sum_{k<=d} 2 Re(I^k/(b - cI)^(k+1)) (r-c)^k + 2 rho^(d+1)/((1-rho) s)`, +`rho = h/s`, whenever `s <= |b - cI|`, `|r - c| <= h < s`. -/ +theorem lor_taylor {b c r h s : ℝ} (hb : 0 < b) (hs : 0 < s) (hsz : s ^ 2 ≤ b ^ 2 + c ^ 2) + (hh0 : 0 ≤ h) (hhs : h < s) (hu : |r - c| ≤ h) (d : ℕ) : + 2 * b / (b ^ 2 + r ^ 2) + ≤ ∑ k ∈ range (d + 1), 2 * (Complex.I ^ k / ((b : ℂ) - (c : ℂ) * Complex.I) ^ (k + 1)).re + * (r - c) ^ k + + 2 * (h / s) ^ (d + 1) / ((1 - h / s) * s) := by + set z : ℂ := (b : ℂ) - (c : ℂ) * Complex.I with hz + set u : ℝ := r - c with hu_def + have hz0 : z ≠ 0 := by + intro h0 + have := congrArg Complex.re h0 + simp [hz] at this + linarith + have hzsq : ‖z‖ ^ 2 = b ^ 2 + c ^ 2 := by + rw [Complex.sq_norm, Complex.normSq_apply]; simp [hz]; ring + have hzs : s ≤ ‖z‖ := by + rw [← pow_le_pow_iff_left₀ hs.le (norm_nonneg z) (by norm_num : (2 : ℕ) ≠ 0), hzsq] + exact hsz + have hzpos : 0 < ‖z‖ := lt_of_lt_of_le hs hzs + set q : ℂ := (u : ℂ) * Complex.I / z with hq + have hqn : ‖q‖ = |u| / ‖z‖ := by + rw [hq, norm_div, norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs] + have hρ0 : 0 ≤ h / s := div_nonneg hh0 hs.le + have hρ1 : h / s < 1 := (div_lt_one hs).mpr hhs + have hqle : ‖q‖ ≤ h / s := by + rw [hqn] + calc |u| / ‖z‖ ≤ h / ‖z‖ := div_le_div_of_nonneg_right hu hzpos.le + _ ≤ h / s := div_le_div_of_nonneg_left hh0 hs hzs + have hq1 : ‖q‖ < 1 := lt_of_le_of_lt hqle hρ1 + have h1q : (1 : ℂ) - q ≠ 0 := by + intro h0 + have : q = 1 := by linear_combination -h0 + rw [this, norm_one] at hq1 + exact lt_irrefl _ hq1 + -- b - rI = z (1 - q) + have hfac : (b : ℂ) - (r : ℂ) * Complex.I = z * (1 - q) := by + rw [hq, mul_sub, mul_one, mul_div_cancel₀ _ hz0, hz, hu_def] + push_cast + ring + -- the geometric identity + have hgeo : (1 : ℂ) / (1 - q) = (∑ k ∈ range (d + 1), q ^ k) + q ^ (d + 1) / (1 - q) := by + have := geom_sum_mul_neg q (d + 1) + field_simp + linear_combination -this + have hinv : (1 : ℂ) / ((b : ℂ) - (r : ℂ) * Complex.I) + = (∑ k ∈ range (d + 1), (Complex.I ^ k / z ^ (k + 1)) * (u : ℂ) ^ k) + + q ^ (d + 1) / (z * (1 - q)) := by + have e1 : (1 : ℂ) / (z * (1 - q)) = (1 / z) * (1 / (1 - q)) := by + rw [one_div_mul_one_div] + rw [hfac, e1, hgeo, mul_add, Finset.mul_sum] + congr 1 + · refine Finset.sum_congr rfl fun k _ => ?_ + rw [hq, div_pow, mul_pow] + field_simp + ring + · field_simp + -- real parts + have hre : ((1 : ℂ) / ((b : ℂ) - (r : ℂ) * Complex.I)).re = b / (b ^ 2 + r ^ 2) := by + rw [one_div, Complex.inv_re, Complex.normSq_apply] + simp + ring + have hsumre : (∑ k ∈ range (d + 1), (Complex.I ^ k / z ^ (k + 1)) * (u : ℂ) ^ k).re + = ∑ k ∈ range (d + 1), (Complex.I ^ k / z ^ (k + 1)).re * u ^ k := by + rw [Complex.re_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [← Complex.ofReal_pow, Complex.re_mul_ofReal] + -- the tail + have htail : (q ^ (d + 1) / (z * (1 - q))).re ≤ (h / s) ^ (d + 1) / ((1 - h / s) * s) := by + refine (Complex.re_le_norm _).trans ?_ + rw [norm_div, norm_mul, norm_pow] + have h1q' : 1 - h / s ≤ ‖1 - q‖ := by + have := norm_sub_norm_le (1 : ℂ) q + rw [norm_one] at this + linarith + have hden : (1 - h / s) * s ≤ ‖z‖ * ‖1 - q‖ := by + rw [mul_comm] + exact mul_le_mul hzs h1q' (by linarith) (norm_nonneg _) + have hdpos : 0 < (1 - h / s) * s := mul_pos (by linarith) hs + calc ‖q‖ ^ (d + 1) / (‖z‖ * ‖1 - q‖) ≤ (h / s) ^ (d + 1) / (‖z‖ * ‖1 - q‖) := + div_le_div_of_nonneg_right (pow_le_pow_left₀ (norm_nonneg _) hqle _) + (mul_nonneg (norm_nonneg _) (norm_nonneg _)) + _ ≤ (h / s) ^ (d + 1) / ((1 - h / s) * s) := + div_le_div_of_nonneg_left (pow_nonneg hρ0 _) hdpos hden + have hmain : b / (b ^ 2 + r ^ 2) + = ∑ k ∈ range (d + 1), (Complex.I ^ k / z ^ (k + 1)).re * u ^ k + + (q ^ (d + 1) / (z * (1 - q))).re := by + rw [← hre, hinv, Complex.add_re, hsumre] + have e2 : 2 * b / (b ^ 2 + r ^ 2) = 2 * (b / (b ^ 2 + r ^ 2)) := by ring + rw [e2, hmain, mul_add, Finset.mul_sum] + have e3 : ∀ k ∈ range (d + 1), 2 * ((Complex.I ^ k / z ^ (k + 1)).re * u ^ k) + = 2 * (Complex.I ^ k / z ^ (k + 1)).re * u ^ k := fun k _ => by ring + rw [Finset.sum_congr rfl e3] + have e4 : 2 * (h / s) ^ (d + 1) / ((1 - h / s) * s) = 2 * ((h / s) ^ (d + 1) / ((1 - h / s) * s)) := by + ring + rw [e4] + linarith + +/-! ## C. One exact Lorentzian with rounded rational coefficients. -/ + +lemma smax_pos {b c : ℚ} (hb : 0 < b) : 0 < smax b c := by + unfold smax + exact lt_of_lt_of_le hb (le_trans (le_max_left b c) (le_max_left _ _)) + +lemma smax_sq_le {b c : ℚ} (hb : 0 ≤ b) (hc : 0 ≤ c) : smax b c ^ 2 ≤ b ^ 2 + c ^ 2 := by + unfold smax + rcases le_total (max b c) (7 / 10 * (b + c)) with h | h + · rw [max_eq_right h]; nlinarith [sq_nonneg (b - c), mul_nonneg hb hc] + · rw [max_eq_left h] + rcases le_total b c with h2 | h2 + · rw [max_eq_right h2]; nlinarith + · rw [max_eq_left h2]; nlinarith + +theorem Lz_le_kapR {b c h : ℚ} (hb : 0 < b) (hc : 0 ≤ c) (hh0 : 0 ≤ h) (hhs : h < smax b c) + {r : ℝ} (hu : |r - (c : ℝ)| ≤ (h : ℝ)) (d : ℕ) : + Lz ((b : ℝ) / 2) r ≤ ∑ k ∈ range (d + 1), ((kapR b c k : ℚ) : ℝ) * (r - c) ^ k + + ((remB b c h d : ℚ) : ℝ) + (((∑ k ∈ range (d + 1), h ^ k) / 10 ^ Rk : ℚ) : ℝ) := by + have hbR : (0 : ℝ) < b := by exact_mod_cast hb + have hL : Lz ((b : ℝ) / 2) r = 2 * (b : ℝ) / ((b : ℝ) ^ 2 + r ^ 2) := by + unfold Lz + field_simp + have hs := smax_pos (c := c) hb + have hsq := smax_sq_le hb.le hc + have hT := lor_taylor (b := (b : ℝ)) (c := (c : ℝ)) (r := r) (h := (h : ℝ)) + (s := ((smax b c : ℚ) : ℝ)) hbR (by exact_mod_cast hs) (by exact_mod_cast hsq) + (by exact_mod_cast hh0) (by exact_mod_cast hhs) hu d + have hk : ∀ k, 2 * (Complex.I ^ k / (((b : ℝ) : ℂ) - (((c : ℝ)) : ℂ) * Complex.I) ^ (k + 1)).re + = ((kap b c k : ℚ) : ℝ) := by + intro k + rw [kap_eq hb k] + push_cast + rfl + simp only [hk] at hT + have hrem : 2 * ((h : ℝ) / ((smax b c : ℚ) : ℝ)) ^ (d + 1) + / ((1 - (h : ℝ) / ((smax b c : ℚ) : ℝ)) * ((smax b c : ℚ) : ℝ)) = ((remB b c h d : ℚ) : ℝ) := by + unfold remB + push_cast + ring + rw [hrem] at hT + have hround : ∀ k ∈ range (d + 1), ((kap b c k : ℚ) : ℝ) * (r - c) ^ k + ≤ ((kapR b c k : ℚ) : ℝ) * (r - c) ^ k + (h : ℝ) ^ k / 10 ^ Rk := by + intro k _ + have h1 : ((kapR b c k : ℚ) : ℝ) ≤ ((kap b c k : ℚ) : ℝ) := by exact_mod_cast floorR_le _ _ + have h2 : ((kap b c k : ℚ) : ℝ) - ((kapR b c k : ℚ) : ℝ) ≤ 1 / 10 ^ Rk := by + have := sub_floorR_le (kap b c k) Rk + have h' : (((kap b c k - kapR b c k : ℚ)) : ℝ) ≤ ((1 / 10 ^ Rk : ℚ) : ℝ) := by exact_mod_cast this + push_cast at h' + exact h' + have h3 : |(r - c) ^ k| ≤ (h : ℝ) ^ k := by + rw [abs_pow]; exact pow_le_pow_left₀ (abs_nonneg _) hu k + have h4 : (((kap b c k : ℚ) : ℝ) - ((kapR b c k : ℚ) : ℝ)) * (r - c) ^ k + ≤ (((kap b c k : ℚ) : ℝ) - ((kapR b c k : ℚ) : ℝ)) * |(r - c) ^ k| := + mul_le_mul_of_nonneg_left (le_abs_self _) (by linarith) + have h5 : (((kap b c k : ℚ) : ℝ) - ((kapR b c k : ℚ) : ℝ)) * |(r - c) ^ k| + ≤ (1 / 10 ^ Rk) * (h : ℝ) ^ k := + mul_le_mul h2 h3 (abs_nonneg _) (by positivity) + have e : (1 / 10 ^ Rk : ℝ) * (h : ℝ) ^ k = (h : ℝ) ^ k / 10 ^ Rk := by ring + linarith + have hsum := Finset.sum_le_sum hround + rw [Finset.sum_add_distrib] at hsum + have e5 : (((∑ k ∈ range (d + 1), h ^ k) / 10 ^ Rk : ℚ) : ℝ) + = ∑ k ∈ range (d + 1), (h : ℝ) ^ k / 10 ^ Rk := by + push_cast + rw [Finset.sum_div] + rw [hL, e5] + linarith + +/-! ## D. The alternating tail. -/ + +lemma inv_one_add_le_alt {y : ℝ} (hy : 0 ≤ y) (K : ℕ) : + 1 / (1 + y) ≤ ∑ k ∈ range (2 * K + 1), (-y) ^ k := by + have h := geom_sum_mul_neg (-y) (2 * K + 1) + have hodd : (-y) ^ (2 * K + 1) = -(y ^ (2 * K + 1)) := by + rw [pow_succ, pow_mul, neg_sq, ← pow_mul]; ring + rw [sub_neg_eq_add, hodd, sub_neg_eq_add] at h + rw [div_le_iff₀ (by linarith)] + nlinarith [pow_nonneg hy (2 * K + 1)] + +lemma Lz_le_alt (j : ℕ) (r : ℝ) (K : ℕ) : + Lz ((j : ℝ) + 1 / 4) r + ≤ ∑ k ∈ range (2 * K + 1), r ^ (2 * k) * ((-1) ^ k * (4 ^ (k + 1) / (4 * (j : ℝ) + 1) ^ (2 * k + 1))) := by + have e4 : (4 * (j : ℝ) + 1) = 4 * ((j : ℝ) + 1 / 4) := by ring + rw [e4] + have hx : (0 : ℝ) < (j : ℝ) + 1 / 4 := by positivity + generalize hX : (j : ℝ) + 1 / 4 = X at hx ⊢ + have hy : 0 ≤ (r ^ 2 / 4) / X ^ 2 := by positivity + have hLz : Lz X r = (1 / X) * (1 / (1 + (r ^ 2 / 4) / X ^ 2)) := by + unfold Lz + field_simp + ring + rw [hLz] + have h1 := inv_one_add_le_alt hy K + refine (mul_le_mul_of_nonneg_left h1 (by positivity)).trans (le_of_eq ?_) + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [neg_pow, div_pow, div_pow, ← pow_mul, ← pow_mul, mul_pow] + field_simp + ring + +lemma nat_div_ceil_ge (a b : ℕ) (hb : 0 < b) : (a : ℝ) / b ≤ (((a + b - 1) / b : ℕ) : ℝ) := by + have h1 := Nat.div_add_mod (a + b - 1) b + have h2 := Nat.mod_lt (a + b - 1) hb + have h3 : a ≤ b * ((a + b - 1) / b) := by omega + have hbR : (0 : ℝ) < b := by exact_mod_cast hb + rw [div_le_iff₀ hbR] + have : (a : ℝ) ≤ (b : ℝ) * (((a + b - 1) / b : ℕ) : ℝ) := by exact_mod_cast h3 + linarith + +lemma gAlt_ge (k : ℕ) : + (-1) ^ k * ∑ j ∈ Ico nS (Nser + 1), (4 : ℝ) ^ (k + 1) / (4 * (j : ℝ) + 1) ^ (2 * k + 1) + ≤ ((gAlt k : ℚ) : ℝ) := by + have hR : (0 : ℝ) < 10 ^ (30 + 3 * k) := by positivity + have hterm : ∀ j : ℕ, (4 : ℝ) ^ (k + 1) / (4 * (j : ℝ) + 1) ^ (2 * k + 1) + = ((4 ^ (k + 1) * 10 ^ (30 + 3 * k) : ℕ) : ℝ) / (((4 * j + 1) ^ (2 * k + 1) : ℕ) : ℝ) + / 10 ^ (30 + 3 * k) := by + intro j + push_cast + field_simp + unfold gAlt + split_ifs with hk + · have hev : (-1 : ℝ) ^ k = 1 := by + rw [← Nat.div_add_mod k 2, hk, add_zero, pow_mul]; norm_num + rw [hev, one_mul] + push_cast + rw [Finset.sum_div] + refine Finset.sum_le_sum fun j _ => ?_ + rw [hterm j] + apply div_le_div_of_nonneg_right _ hR.le + have hpos : 0 < (4 * j + 1) ^ (2 * k + 1) := by positivity + have := nat_div_ceil_ge (4 ^ (k + 1) * 10 ^ (30 + 3 * k)) ((4 * j + 1) ^ (2 * k + 1)) hpos + push_cast at this ⊢ + exact this + · have hodd : (-1 : ℝ) ^ k = -1 := by + have hk1 : k % 2 = 1 := by omega + rw [← Nat.div_add_mod k 2, hk1, pow_add, pow_mul]; norm_num + rw [hodd, neg_one_mul] + push_cast + rw [neg_div, neg_le_neg_iff, Finset.sum_div] + refine Finset.sum_le_sum fun j _ => ?_ + rw [hterm j] + apply div_le_div_of_nonneg_right _ hR.le + exact Nat.cast_div_le + +theorem sum_Lz_large_le (r : ℝ) : + ∑ j ∈ Ico nS (Nser + 1), Lz ((j : ℝ) + 1 / 4) r + ≤ ∑ k ∈ range (2 * Kalt + 1), r ^ (2 * k) * ((gAlt k : ℚ) : ℝ) := by + calc ∑ j ∈ Ico nS (Nser + 1), Lz ((j : ℝ) + 1 / 4) r + ≤ ∑ j ∈ Ico nS (Nser + 1), ∑ k ∈ range (2 * Kalt + 1), + r ^ (2 * k) * ((-1) ^ k * (4 ^ (k + 1) / (4 * (j : ℝ) + 1) ^ (2 * k + 1))) := + Finset.sum_le_sum fun j _ => Lz_le_alt j r Kalt + _ = ∑ k ∈ range (2 * Kalt + 1), r ^ (2 * k) + * ((-1) ^ k * ∑ j ∈ Ico nS (Nser + 1), (4 : ℝ) ^ (k + 1) / (4 * (j : ℝ) + 1) ^ (2 * k + 1)) := by + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [Finset.mul_sum, Finset.mul_sum] + _ ≤ ∑ k ∈ range (2 * Kalt + 1), r ^ (2 * k) * ((gAlt k : ℚ) : ℝ) := by + refine Finset.sum_le_sum fun k _ => ?_ + exact mul_le_mul_of_nonneg_left (gAlt_ge k) (by rw [pow_mul]; exact pow_nonneg (sq_nonneg r) k) + +/-! ## E. The integral tail of the series. -/ + +lemma serG_N_ge (N : ℕ) (r : ℝ) : + (1 / 4) / ((N : ℝ) + 5 / 4) + r ^ 2 / (8 * ((N : ℝ) + 5 / 4) ^ 2) + - r ^ 4 / (32 * ((N : ℝ) + 5 / 4) ^ 4) ≤ serG (r / 2) N := by + have hX : (0 : ℝ) < (N : ℝ) + 1 + 1 / 4 := by positivity + have hx1 : (0 : ℝ) < (N : ℝ) + 1 := by positivity + set w : ℝ := (r / 2) ^ 2 / ((N : ℝ) + 1 + 1 / 4) ^ 2 with hw_def + have hw : 0 ≤ w := by positivity + have e : serG (r / 2) N + = Real.log (((N : ℝ) + 1 + 1 / 4) / ((N : ℝ) + 1)) + (1 / 2) * Real.log (1 + w) := by + unfold serG + rw [Real.log_div hX.ne' hx1.ne'] + have h2 : ((N : ℝ) + 1 + 1 / 4) ^ 2 + (r / 2) ^ 2 = ((N : ℝ) + 1 + 1 / 4) ^ 2 * (1 + w) := by + rw [hw_def]; field_simp + rw [h2, Real.log_mul (by positivity) (by positivity), Real.log_pow] + push_cast + ring + have h1 : 1 - ((N : ℝ) + 1) / ((N : ℝ) + 1 + 1 / 4) + ≤ Real.log (((N : ℝ) + 1 + 1 / 4) / ((N : ℝ) + 1)) := by + have := Real.one_sub_inv_le_log_of_pos (x := ((N : ℝ) + 1 + 1 / 4) / ((N : ℝ) + 1)) (by positivity) + rwa [inv_div] at this + have h2 : w - w ^ 2 ≤ Real.log (1 + w) := by + have := Real.one_sub_inv_le_log_of_pos (x := 1 + w) (by positivity) + have h3 : w - w ^ 2 ≤ 1 - (1 + w)⁻¹ := by + rw [← sub_nonneg] + have e2 : 1 - (1 + w)⁻¹ - (w - w ^ 2) = w ^ 3 / (1 + w) := by + field_simp + ring + rw [e2] + positivity + linarith + have e3 : 1 - ((N : ℝ) + 1) / ((N : ℝ) + 1 + 1 / 4) = (1 / 4) / ((N : ℝ) + 5 / 4) := by + field_simp + ring + have e4 : w = r ^ 2 / (4 * ((N : ℝ) + 5 / 4) ^ 2) := by + rw [hw_def]; field_simp; ring + rw [e] + rw [e3] at h1 + have e5 : (1 / 2) * (w - w ^ 2) + = r ^ 2 / (8 * ((N : ℝ) + 5 / 4) ^ 2) - r ^ 4 / (32 * ((N : ℝ) + 5 / 4) ^ 4) := by + rw [e4] + field_simp + ring + linarith [h1, h2, e5] + +lemma serG_NM_le (N M : ℕ) (r : ℝ) : + serG (r / 2) ((N : ℝ) + M) + ≤ (1 / 2) * ((((N : ℝ) + M + 5 / 4) ^ 2 - ((N : ℝ) + M + 1) ^ 2) / ((N : ℝ) + M + 1) ^ 2) + + r ^ 2 / (8 * ((N : ℝ) + M + 1) ^ 2) := by + have h := (serG_bounds (r / 2) (x := (N : ℝ) + M) (by positivity)).2 + have hx1 : (0 : ℝ) < (N : ℝ) + M + 1 := by positivity + refine h.trans (le_of_eq ?_) + field_simp + ring + +/-! ## F. Assembly. -/ + +/-- The global part of the lower bound (constants, integral tail, large Lorentzians). -/ +def globPoly (r : ℝ) : ℝ := + ((C0 : ℚ) : ℝ) + ((C1 : ℚ) : ℝ) * r ^ 2 + ((C2 : ℚ) : ℝ) * r ^ 4 + - ∑ k ∈ range (2 * Kalt + 1), r ^ (2 * k) * ((gAlt k : ℚ) : ℝ) + +lemma HNr_le_Q : HNr ≤ ∑ n ∈ range Nser, (1 : ℚ) / ((n : ℚ) + 1) := by + unfold HNr + rw [Finset.sum_div] + refine Finset.sum_le_sum fun n _ => ?_ + have h1 : (((10 ^ 30 / (n + 1) : ℕ) : ℚ)) ≤ ((10 ^ 30 : ℕ) : ℚ) / ((n + 1 : ℕ) : ℚ) := Nat.cast_div_le + have hA : (0 : ℚ) < 10 ^ 30 := by positivity + rw [div_le_iff₀ hA] + calc (((10 ^ 30 / (n + 1) : ℕ) : ℚ)) ≤ ((10 ^ 30 : ℕ) : ℚ) / ((n + 1 : ℕ) : ℚ) := h1 + _ = 1 / ((n : ℚ) + 1) * 10 ^ 30 := by push_cast; ring + +lemma HNr_le : ((HNr : ℚ) : ℝ) ≤ ∑ n ∈ range Nser, (1 : ℝ) / ((n : ℝ) + 1) := by + have := (Rat.cast_le (K := ℝ)).mpr HNr_le_Q + push_cast at this + exact this + +/-- **The global series floor**: `Psi r >= globPoly r - sum_{j<18} Lz(j + 1/4, r)` for all `r`. -/ +theorem Psi_ge_glob (r : ℝ) : + globPoly r - ∑ j ∈ range nS, Lz ((j : ℝ) + 1 / 4) r ≤ Psi r := by + have hs := psi_series_Lz r Nser Mser + have hsplit : ∑ j ∈ range (Nser + 1), Lz ((j : ℝ) + 1 / 4) r + = ∑ j ∈ range nS, Lz ((j : ℝ) + 1 / 4) r + ∑ j ∈ Ico nS (Nser + 1), Lz ((j : ℝ) + 1 / 4) r := by + rw [Finset.range_eq_Ico, Finset.range_eq_Ico, + Finset.sum_Ico_consecutive _ (Nat.zero_le nS) (by unfold nS Nser; norm_num)] + have hlarge := sum_Lz_large_le r + have hG1 := serG_N_ge Nser r + have hG2 := serG_NM_le Nser Mser r + have hH := HNr_le + have hg := gamma_le + have hp := log_pi_le + unfold Psi globPoly + have hC0 : ((C0 : ℚ) : ℝ) = -((gammaUpQ : ℚ) : ℝ) - ((logPiUpQ : ℚ) : ℝ) + ((HNr : ℚ) : ℝ) + + (1 / 4) / ((Nser : ℝ) + 5 / 4) + - (1 / 2) * ((((Nser : ℝ) + Mser + 5 / 4) ^ 2 - ((Nser : ℝ) + Mser + 1) ^ 2) + / ((Nser : ℝ) + Mser + 1) ^ 2) := by + unfold C0 NQ MQ + push_cast + ring + have hC1 : ((C1 : ℚ) : ℝ) = 1 / (8 * ((Nser : ℝ) + 5 / 4) ^ 2) - 1 / (8 * ((Nser : ℝ) + Mser + 1) ^ 2) := by + unfold C1 NQ MQ + push_cast + ring + have hC2 : ((C2 : ℚ) : ℝ) = -1 / (32 * ((Nser : ℝ) + 5 / 4) ^ 4) := by + unfold C2 NQ + push_cast + ring + rw [hC0, hC1, hC2] + rw [hsplit] at hs + have e1 : r ^ 2 / (8 * ((Nser : ℝ) + 5 / 4) ^ 2) = 1 / (8 * ((Nser : ℝ) + 5 / 4) ^ 2) * r ^ 2 := by ring + have e2 : r ^ 4 / (32 * ((Nser : ℝ) + 5 / 4) ^ 4) = -(-1 / (32 * ((Nser : ℝ) + 5 / 4) ^ 4) * r ^ 4) := by + ring + have e3 : r ^ 2 / (8 * ((Nser : ℝ) + Mser + 1) ^ 2) = 1 / (8 * ((Nser : ℝ) + Mser + 1) ^ 2) * r ^ 2 := by + ring + rw [e1, e2] at hG1 + rw [e3] at hG2 + linarith + +/-- The global polynomial dominates its rounded kernel coefficients. -/ +theorem globC_poly_le (r : ℝ) : + ∑ p ∈ range (Dmax + 1), ((globC p : ℚ) : ℝ) * r ^ p ≤ globPoly r := by + have hle : ∀ p ∈ range (Dmax + 1), ((globC p : ℚ) : ℝ) * r ^ p ≤ ((globRaw p : ℚ) : ℝ) * r ^ p := by + intro p _ + rcases Nat.even_or_odd p with ⟨m, hm⟩ | hodd + · have hr : 0 ≤ r ^ p := by rw [hm, ← two_mul, pow_mul]; positivity + exact mul_le_mul_of_nonneg_right (by exact_mod_cast floorR_le _ _) hr + · have h0 : globRaw p = 0 := by + unfold globRaw + have h1 : p % 2 = 1 := Nat.odd_iff.mp hodd + have hp0 : p ≠ 0 := by omega + have hp2 : p ≠ 2 := by omega + have hp4 : p ≠ 4 := by omega + simp [hp0, hp2, hp4, h1] + have hc : globC p = 0 := by + unfold globC; rw [h0]; simp [floorR] + rw [hc, h0] + refine (Finset.sum_le_sum hle).trans (le_of_eq ?_) + unfold globPoly globRaw + simp only [Dmax, Kalt, Finset.sum_range_succ, Finset.sum_range_zero] + norm_num + push_cast + ring + +/-! ## G. The shift-to-power identity. -/ + +lemma sum_ite_le_range {β : Type*} [AddCommMonoid β] (f : ℕ → β) {d D : ℕ} (h : d ≤ D) : + ∑ k ∈ range (D + 1), (if k ≤ d then f k else 0) = ∑ k ∈ range (d + 1), f k := by + rw [← Finset.sum_filter] + congr 1 + ext k + simp only [Finset.mem_filter, Finset.mem_range] + omega + +theorem wpoly_eq {i : ℕ} (r : ℝ) : + wpoly i r = ∑ p ∈ range (Dmax + 1), ((globC p : ℚ) : ℝ) * r ^ p + - ∑ k ∈ range (Dmax + 1), ((uCoef i k : ℚ) : ℝ) * (r - pcen i) ^ k - ((rhoR i : ℚ) : ℝ) := by + unfold wpoly + have hw : ∀ p ∈ range (Dmax + 1), (((wpList i).getD p 0 : ℚ) : ℝ) * r ^ p + = ((globC p : ℚ) : ℝ) * r ^ p + - ∑ k ∈ range (Dmax + 1), (if p ≤ k then ((uCoef i k : ℚ) : ℝ) * (k.choose p : ℝ) + * (-(pcen i : ℝ)) ^ (k - p) * r ^ p else 0) + - (if p = 0 then ((rhoR i : ℚ) : ℝ) else 0) := by + intro p hp + have hp' := Finset.mem_range.mp hp + unfold wpList + rw [getD_map_range _ _ hp'] + unfold wpCoef + rw [globList, getD_map_range _ _ hp'] + push_cast + rw [sub_mul, sub_mul, Finset.sum_mul] + congr 1 + · congr 1 + refine Finset.sum_congr rfl fun k hk => ?_ + split_ifs + · rw [uList, getD_map_range _ _ (Finset.mem_range.mp hk)] + push_cast + ring + · simp + · split_ifs with h0 <;> simp [h0] + rw [Finset.sum_congr rfl hw, Finset.sum_sub_distrib, Finset.sum_sub_distrib] + congr 1 + · congr 1 + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun k hk => ?_ + have hk' : k ≤ Dmax := Nat.lt_succ_iff.mp (Finset.mem_range.mp hk) + have e : ∑ p ∈ range (Dmax + 1), (if p ≤ k then ((uCoef i k : ℚ) : ℝ) * (k.choose p : ℝ) + * (-(pcen i : ℝ)) ^ (k - p) * r ^ p else 0) + = ∑ p ∈ range (k + 1), ((uCoef i k : ℚ) : ℝ) * (k.choose p : ℝ) * (-(pcen i : ℝ)) ^ (k - p) + * r ^ p := sum_ite_le_range _ hk' + rw [e, sub_eq_add_neg r, add_pow, Finset.mul_sum] + refine Finset.sum_congr rfl fun p _ => ?_ + ring + · rw [Finset.sum_ite_eq' (range (Dmax + 1)) 0 (fun _ => ((rhoR i : ℚ) : ℝ))] + simp [Dmax] + +/-! ## H. The minorant on each piece. -/ + +lemma brk_nonneg (i : ℕ) : 0 ≤ brk i := by + unfold brk + split <;> norm_num + +lemma brk_le_succ {i : ℕ} (hi : i < nPc) : brk i ≤ brk (i + 1) := by + unfold nPc at hi + interval_cases i <;> norm_num [brk] + +theorem sum_Lz_small_le {i : ℕ} (hi : i < nPc) {r : ℝ} (hu : |r - (pcen i : ℝ)| ≤ (phw i : ℝ)) : + ∑ j ∈ range nS, Lz ((j : ℝ) + 1 / 4) r + ≤ ∑ k ∈ range (Dmax + 1), ((uCoef i k : ℚ) : ℝ) * (r - pcen i) ^ k + ((rhoR i : ℚ) : ℝ) := by + have hc : 0 ≤ pcen i := by + unfold pcen; have := brk_nonneg i; have := brk_nonneg (i + 1); linarith + have hh : 0 ≤ phw i := by unfold phw; have := brk_le_succ hi; linarith + have hj : ∀ j ∈ range nS, Lz ((j : ℝ) + 1 / 4) r + ≤ ∑ k ∈ range (Dmax + 1), (if k ≤ deg i j then ((kapR (bS j) (pcen i) k : ℚ) : ℝ) else 0) + * (r - pcen i) ^ k + + (((remB (bS j) (pcen i) (phw i) (deg i j) + + (∑ k ∈ range (deg i j + 1), phw i ^ k) / 10 ^ Rk : ℚ)) : ℝ) := by + intro j hjm + have hjS := Finset.mem_range.mp hjm + obtain ⟨hlt, hdeg⟩ := pieceCheck_sound piece_ok hi hjS + have hb : (0 : ℚ) < bS j := by unfold bS; positivity + have hL := Lz_le_kapR hb hc hh hlt hu (deg i j) + have hx : ((bS j : ℚ) : ℝ) / 2 = (j : ℝ) + 1 / 4 := by unfold bS; push_cast; ring + rw [hx] at hL + have e : ∑ k ∈ range (Dmax + 1), (if k ≤ deg i j then ((kapR (bS j) (pcen i) k : ℚ) : ℝ) else 0) + * (r - pcen i) ^ k + = ∑ k ∈ range (deg i j + 1), ((kapR (bS j) (pcen i) k : ℚ) : ℝ) * (r - pcen i) ^ k := by + rw [← sum_ite_le_range _ hdeg] + refine Finset.sum_congr rfl fun k _ => ?_ + split_ifs <;> simp + rw [e] + push_cast at hL ⊢ + linarith + refine (Finset.sum_le_sum hj).trans ?_ + rw [Finset.sum_add_distrib, Finset.sum_comm] + have hu1 : ∀ k ∈ range (Dmax + 1), ∑ j ∈ range nS, (if k ≤ deg i j then + ((kapR (bS j) (pcen i) k : ℚ) : ℝ) else 0) * (r - pcen i) ^ k + = ((uCoef i k : ℚ) : ℝ) * (r - pcen i) ^ k := by + intro k _ + unfold uCoef + push_cast + rw [Finset.sum_mul] + refine Finset.sum_congr rfl fun j _ => ?_ + split_ifs <;> simp + rw [Finset.sum_congr rfl hu1] + have hrho : ∑ j ∈ range nS, (((remB (bS j) (pcen i) (phw i) (deg i j) + + (∑ k ∈ range (deg i j + 1), phw i ^ k) / 10 ^ Rk : ℚ)) : ℝ) ≤ ((rhoR i : ℚ) : ℝ) := by + have h1 := le_ceilR (rhoRaw i) Rk + have h2 : ((rhoRaw i : ℚ) : ℝ) ≤ ((rhoR i : ℚ) : ℝ) := by exact_mod_cast h1 + refine le_trans (le_of_eq ?_) h2 + unfold rhoRaw + push_cast + rfl + linarith + +/-- **The minorant**: on piece `i`, `wpoly i t <= Psi t`. -/ +theorem wpoly_le_Psi {i : ℕ} (hi : i < nPc) {t : ℝ} (ha : ((brk i : ℚ) : ℝ) ≤ t) + (hb : t ≤ ((brk (i + 1) : ℚ) : ℝ)) : wpoly i t ≤ Psi t := by + have hu : |t - (pcen i : ℝ)| ≤ (phw i : ℝ) := by + unfold pcen phw + push_cast + rw [abs_le] + constructor <;> linarith + rw [wpoly_eq] + have h1 := globC_poly_le t + have h2 := sum_Lz_small_le hi hu + have h3 := Psi_ge_glob t + linarith + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Split.lean b/telperion/examples/rvm_bridge/lean/KWin_Split.lean new file mode 100644 index 000000000..c8370a571 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Split.lean @@ -0,0 +1,357 @@ +/- + KWin_Split -- the Zhu frequency split of the Weil form on the prime-free window, in the sector + form consumed by the KWin certificate (rvm_bridge island, 2026-09-24). + + conjecture1_proved = False. (Finite-window Weil positivity is not RH; PR #604: the 1.3e-3 + full-class margin at this window is zero content; not Connes-Consani, whose theorem is for the + pole-free class.) + + PROVED HERE (`Q_ge_Rb`): for a real test v of parity par (v(-u) = eps v(u), eps = +1 / -1), + smooth, compactly supported in [-L0, L0], L0 = log 2 / 2, + Rb par v v <= Re weilForm (autocorr v) + where Rb (KWin_Head) = 2 eps (int v poleF)^2 + beta0 int v^2 + (1/pi) int_0^20 (Psi - beta0) Tr v^2. + Route: Zhu eq. (2) (`symbol_representation_ofReal`, PROVED in ZhuSymbol) at L = L0, where the + comb is empty (KWin_Constants: weilSymbol L0 = Psi); the transform on the line is the sector + transform (the other trigonometric half vanishes by parity) and the pole term is the sector + pole functional; Plancherel (Fourier inversion of the autocorrelation at 0, as in ZhuSymbol); + evenness in t, and Psi >= beta*(L0, 20) >= beta0 on [20, oo) (ZhuSplit + KWin_Constants). + No `sorry`. +-/ +import KWin_Head +import ZhuParity + +open Real MeasureTheory Set +open scoped ComplexConjugate + +noncomputable section + +namespace KWin +open RvMBridge11 RvMBridgeZhu WeilExplicit RvMBridge4 RvMBridge5 Zeta23 + +/-! ## A. Support and the conversion to [-l, l]. -/ + +lemma v_eq_zero_of_not_mem {v : ℝ → ℝ} (hsupp : tsupport (fun u => (v u : ℂ)) ⊆ Icc (-L0) L0) + {x : ℝ} (hx : x ∉ Icc (-L0) L0) : v x = 0 := by + have h : (fun u => (v u : ℂ)) x = 0 := + image_eq_zero_of_notMem_tsupport (f := fun u => (v u : ℂ)) (fun hm => hx (hsupp hm)) + simpa using h + +lemma integral_eq_interval {v : ℝ → ℝ} (hsupp : tsupport (fun u => (v u : ℂ)) ⊆ Icc (-L0) L0) + (w : ℝ → ℝ) : ∫ x, v x * w x = ∫ x in (-ellR)..ellR, v x * w x := by + have hlt := L0_lt_ell + have hL0 := L0_pos + have hle : -ellR ≤ ellR := by unfold ellR; linarith + rw [intervalIntegral.integral_of_le hle] + refine (setIntegral_eq_integral_of_forall_compl_eq_zero fun x hx => ?_).symm + have : x ∉ Icc (-L0) L0 := by + intro hm + apply hx + rw [mem_Ioc] + unfold ellR + constructor + · linarith [hm.1] + · linarith [hm.2] + rw [v_eq_zero_of_not_mem hsupp this, zero_mul] + +lemma integral_odd_eq_zero {g : ℝ → ℝ} (h : ∀ u, g (-u) = -g u) : ∫ u, g u = 0 := by + have h1 := integral_neg_eq_self g volume + have h2 : ∫ x, g (-x) = -∫ x, g x := by + rw [← integral_neg]; exact integral_congr_ae (Filter.Eventually.of_forall h) + rw [h2] at h1 + linarith + +lemma continuous_v {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) : Continuous v := by + have h := Complex.continuous_re.comp hf.1.continuous + have e : (Complex.re ∘ fun u => (v u : ℂ)) = v := by funext u; simp + rwa [e] at h + +lemma compact_v {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) : HasCompactSupport v := by + have h := hf.2.comp_left (g := Complex.re) (by simp) + have e : (Complex.re ∘ fun u => (v u : ℂ)) = v := by funext u; simp + rwa [e] at h + +lemma integrable_v_mul {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) {w : ℝ → ℝ} + (hw : Continuous w) : Integrable (fun u => v u * w u) := + ((continuous_v hf).mul hw).integrable_of_hasCompactSupport (compact_v hf).mul_right + +/-! ## B. The transform on the line and the pole term. -/ + +lemma paperFT_ofReal_line {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) (t : ℝ) : + paperFT (fun u => (v u : ℂ)) t + = ((∫ u, v u * Real.cos (t * u) : ℝ) : ℂ) + ((∫ u, v u * Real.sin (t * u) : ℝ) : ℂ) * Complex.I := by + unfold paperFT + have e : (fun u : ℝ => (v u : ℂ) * Complex.exp (Complex.I * (t : ℂ) * (u : ℂ))) + = fun u => ((v u * Real.cos (t * u) : ℝ) : ℂ) + ((v u * Real.sin (t * u) : ℝ) : ℂ) * Complex.I := by + funext u + rw [show Complex.I * (t : ℂ) * (u : ℂ) = ((t * u : ℝ) : ℂ) * Complex.I by push_cast; ring, + Complex.exp_mul_I, ← Complex.ofReal_cos, ← Complex.ofReal_sin] + push_cast + ring + have hc : Integrable (fun u => ((v u * Real.cos (t * u) : ℝ) : ℂ)) := + (integrable_v_mul hf (by fun_prop)).ofReal + have hs : Integrable (fun u => ((v u * Real.sin (t * u) : ℝ) : ℂ) * Complex.I) := + ((integrable_v_mul hf (by fun_prop)).ofReal).mul_const _ + rw [e, integral_add hc hs, integral_mul_const, integral_complex_ofReal, integral_complex_ofReal] + +lemma norm_sq_line {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) (t : ℝ) : + ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (t : ℂ) * Complex.I)‖ ^ 2 + = (∫ u, v u * Real.cos (t * u)) ^ 2 + (∫ u, v u * Real.sin (t * u)) ^ 2 := by + rw [weilKernel_line, paperFT_ofReal_line hf, Complex.sq_norm, Complex.normSq_add_mul_I] + +/-- On the line, `|F(t)|^2` is the square of the sector transform. -/ +lemma norm_sq_line_sector {v : ℝ → ℝ} {par : ℕ} (hpar : par = 0 ∨ par = 1) + (hf : IsWeilTest (fun u => (v u : ℂ))) (hev : ∀ u, v (-u) = epsR par * v u) + (hsupp : tsupport (fun u => (v u : ℂ)) ⊆ Icc (-L0) L0) (t : ℝ) : + ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (t : ℂ) * Complex.I)‖ ^ 2 = (Tr ellR par v t) ^ 2 := by + rw [norm_sq_line hf] + unfold Tr + rw [← integral_eq_interval hsupp] + rcases hpar with h | h <;> subst h + · have hs : ∫ u, v u * Real.sin (t * u) = 0 := integral_odd_eq_zero fun u => by + have h1 := hev u + simp only [epsR, if_true, one_mul] at h1 + rw [h1, mul_neg, Real.sin_neg]; ring + rw [hs] + simp [phiF] + · have hc : ∫ u, v u * Real.cos (t * u) = 0 := integral_odd_eq_zero fun u => by + have h1 := hev u + simp only [epsR, one_ne_zero, if_false] at h1 + rw [h1, mul_neg, Real.cos_neg]; ring + rw [hc] + simp [phiF] + +lemma weilKernel_zero_ofReal (v : ℝ → ℝ) : + weilKernel (fun u => (v u : ℂ)) 0 = ((∫ u, v u * Real.exp (-(u / 2)) : ℝ) : ℂ) := by + unfold weilKernel + rw [← integral_complex_ofReal] + congr 1 + funext u + push_cast + congr 2 + ring + +lemma exp_moment_parity {v : ℝ → ℝ} {par : ℕ} (hev : ∀ u, v (-u) = epsR par * v u) : + ∫ u, v u * Real.exp (-(u / 2)) = epsR par * ∫ u, v u * Real.exp (u / 2) := by + have h := integral_neg_eq_self (fun u => v u * Real.exp (-(u / 2))) volume + rw [← h, ← integral_const_mul] + congr 1 + funext u + rw [hev u] + have : -(-u / 2) = u / 2 := by ring + rw [this] + ring + +/-- The pole term: `|F(i/2)|^2` is the square of the sector pole functional. -/ +lemma K0_sq {v : ℝ → ℝ} {par : ℕ} (hpar : par = 0 ∨ par = 1) + (hf : IsWeilTest (fun u => (v u : ℂ))) (hev : ∀ u, v (-u) = epsR par * v u) + (hsupp : tsupport (fun u => (v u : ℂ)) ⊆ Icc (-L0) L0) : + ‖weilKernel (fun u => (v u : ℂ)) 0‖ ^ 2 = (Pl ellR par v) ^ 2 := by + rw [weilKernel_zero_ofReal, Complex.norm_real, Real.norm_eq_abs, sq_abs] + have hE := exp_moment_parity hev + have hPl : Pl ellR par v = ∫ u, v u * poleF par u := (integral_eq_interval hsupp _).symm + have hi1 : Integrable (fun u => v u * Real.exp (u / 2)) := integrable_v_mul hf (by fun_prop) + have hi2 : Integrable (fun u => v u * Real.exp (-(u / 2))) := integrable_v_mul hf (by fun_prop) + rw [hPl] + rcases hpar with h | h <;> subst h + · have e : (fun u => v u * poleF 0 u) + = fun u => (1 / 2 : ℝ) * (v u * Real.exp (u / 2) + v u * Real.exp (-(u / 2))) := by + funext u; simp only [poleF, if_true, Real.cosh_eq]; ring + rw [e, integral_const_mul, integral_add hi1 hi2] + simp only [epsR, if_true, one_mul] at hE + rw [hE] + ring + · have e : (fun u => v u * poleF 1 u) + = fun u => (1 / 2 : ℝ) * (v u * Real.exp (u / 2) - v u * Real.exp (-(u / 2))) := by + funext u; simp only [poleF, one_ne_zero, if_false, Real.sinh_eq]; ring + rw [e, integral_const_mul, integral_sub hi1 hi2] + simp only [epsR, one_ne_zero, if_false] at hE + rw [hE] + ring + +/-! ## C. Plancherel and integrability. -/ + +theorem plancherel_ofReal {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) : + (∫ x, v x ^ 2) = (1 / (2 * Real.pi)) + * ∫ r : ℝ, ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2 := by + set fC : ℝ → ℂ := fun u => (v u : ℂ) with hfC + set g : ℝ → ℂ := WeilExplicit.autocorr fC with hgdef + have hg : IsWeilTest g := isWeilTest_autocorr hf + set F : ℝ → ℝ := fun r => ‖weilKernel fC (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2 with hF + have hline : ∀ r : ℝ, paperFT g r = (F r : ℂ) := by + intro r + rw [← weilKernel_line, hgdef, weilKernel_autocorr_line hf, hF] + simp only + rw [weilKernel_line] + push_cast + ring + have hg0 : g 0 = ((∫ x : ℝ, ‖fC x‖ ^ 2 : ℝ) : ℂ) := by + rw [hgdef] + unfold WeilExplicit.autocorr + rw [← integral_complex_ofReal] + congr 1 + funext x + rw [sub_zero, Complex.mul_conj'] + push_cast + ring + have h := inversion_zero hg + rw [hg0] at h + have h2 : ∫ r : ℝ, paperFT g r = ((∫ r, F r : ℝ) : ℂ) := by + rw [← integral_complex_ofReal] + congr 1 + funext r + exact hline r + rw [h2] at h + have h3 : ((1 / (2 * Real.pi) * ∫ r, F r : ℝ) : ℂ) = ((∫ x : ℝ, ‖fC x‖ ^ 2 : ℝ) : ℂ) := by + push_cast + exact h + have h4 := (Complex.ofReal_inj.mp h3).symm + have e : (fun x => ‖fC x‖ ^ 2) = fun x => v x ^ 2 := by + funext x; rw [hfC]; simp only; rw [Complex.norm_real, Real.norm_eq_abs, sq_abs] + rw [e] at h4 + rw [h4] + +theorem integrable_line_sq {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) : + Integrable (fun r : ℝ => ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2) := by + set fC : ℝ → ℂ := fun u => (v u : ℂ) + set g : ℝ → ℂ := WeilExplicit.autocorr fC with hgdef + have hg : IsWeilTest g := isWeilTest_autocorr hf + have hline : ∀ r : ℝ, paperFT g r = ((‖weilKernel fC (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2 : ℝ) : ℂ) := by + intro r + rw [← weilKernel_line, hgdef, weilKernel_autocorr_line hf] + rw [weilKernel_line] + push_cast + ring + have := (integrable_paperFT hg).re + refine this.congr (Filter.Eventually.of_forall fun r => ?_) + simp only [RCLike.re_to_complex] + rw [hline r, Complex.ofReal_re] + +theorem integrable_line_sq_mul_psi {v : ℝ → ℝ} (hf : IsWeilTest (fun u => (v u : ℂ))) : + Integrable (fun r : ℝ => ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2 + * psiR r) := by + set fC : ℝ → ℂ := fun u => (v u : ℂ) + set g : ℝ → ℂ := WeilExplicit.autocorr fC with hgdef + have hg : IsWeilTest g := isWeilTest_autocorr hf + have harch : ∀ r : ℝ, archIntegrand g r + = (((‖weilKernel fC (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2) * psiR r : ℝ) : ℂ) := by + intro r + unfold archIntegrand + rw [hgdef, weilKernel_autocorr_line hf] + rw [weilKernel_line] + unfold psiR + push_cast + ring + have := (integrable_archIntegrand hg).re + refine this.congr (Filter.Eventually.of_forall fun r => ?_) + simp only [RCLike.re_to_complex] + rw [harch r, Complex.ofReal_re] + +/-! ## D. The split. -/ + +/-- The half-line split of an even integrand at `T = 20`. -/ +theorem split_line {F : ℝ → ℝ} (hFi : Integrable F) (hFPi : Integrable fun t => F t * Psi t) + (hF0 : ∀ t, 0 ≤ F t) (hFe : ∀ t, F (-t) = F t) (hFc : Continuous F) : + (1 / Real.pi) * (∫ t in (0 : ℝ)..20, (Psi t - beta0R) * F t) + + beta0R * ((1 / (2 * Real.pi)) * ∫ t, F t) + ≤ (1 / (2 * Real.pi)) * ∫ t, F t * Psi t := by + have hpi := Real.pi_pos + have hPe : ∀ t, Psi (-t) = Psi t := fun t => by unfold Psi; rw [RvMBridge30.psiR_neg] + have habs1 : ∫ t, F t * Psi t = 2 * ∫ t in Ioi (0 : ℝ), F t * Psi t := by + rw [← integral_comp_abs (f := fun t => F t * Psi t)] + congr 1; funext t + rcases le_or_gt 0 t with h | h + · rw [abs_of_nonneg h] + · rw [abs_of_neg h, hFe, hPe] + have habs2 : ∫ t, F t = 2 * ∫ t in Ioi (0 : ℝ), F t := by + rw [← integral_comp_abs (f := F)] + congr 1; funext t + rcases le_or_gt 0 t with h | h + · rw [abs_of_nonneg h] + · rw [abs_of_neg h, hFe] + have hU : Ioc (0 : ℝ) 20 ∪ Ioi 20 = Ioi 0 := Ioc_union_Ioi_eq_Ioi (by norm_num) + have hD : Disjoint (Ioc (0 : ℝ) 20) (Ioi 20) := by + rw [Set.disjoint_left]; intro x hx hx'; exact absurd hx.2 (not_le.mpr hx') + have hs1 : ∫ t in Ioi (0 : ℝ), F t * Psi t + = (∫ t in Ioc (0 : ℝ) 20, F t * Psi t) + ∫ t in Ioi (20 : ℝ), F t * Psi t := by + rw [← hU, setIntegral_union hD measurableSet_Ioi hFPi.integrableOn hFPi.integrableOn] + have hs2 : ∫ t in Ioi (0 : ℝ), F t + = (∫ t in Ioc (0 : ℝ) 20, F t) + ∫ t in Ioi (20 : ℝ), F t := by + rw [← hU, setIntegral_union hD measurableSet_Ioi hFi.integrableOn hFi.integrableOn] + have hmono : beta0R * ∫ t in Ioi (20 : ℝ), F t ≤ ∫ t in Ioi (20 : ℝ), F t * Psi t := by + rw [← integral_const_mul] + refine setIntegral_mono_on (hFi.integrableOn.const_mul _) hFPi.integrableOn measurableSet_Ioi + fun t ht => ?_ + have hb := beta0_le_betaStar + have hs := weilSymbol_ge_betaStar (L := L0) (by norm_num : (15 : ℝ) / 4 ≤ 20) (le_of_lt ht) + rw [weilSymbol_L0] at hs + have : beta0R ≤ Psi t := by unfold beta0R; linarith + rw [mul_comm] + exact mul_le_mul_of_nonneg_left this (hF0 t) + have hIoc : ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * F t + = (∫ t in Ioc (0 : ℝ) 20, F t * Psi t) - beta0R * ∫ t in Ioc (0 : ℝ) 20, F t := by + rw [intervalIntegral.integral_of_le (by norm_num), ← integral_const_mul, + ← integral_sub hFPi.integrableOn (hFi.integrableOn.const_mul _)] + congr 1; funext t; ring + rw [hIoc, habs1, habs2, hs1, hs2] + have e : (1 / Real.pi) = 2 * (1 / (2 * Real.pi)) := by field_simp + rw [e] + have hc : 0 < 1 / (2 * Real.pi) := by positivity + nlinarith [hmono] + +/-- **The split**: `Rb par v v <= Q(v)` on the window. -/ +theorem Q_ge_Rb {v : ℝ → ℝ} {par : ℕ} (hpar : par = 0 ∨ par = 1) + (hf : IsWeilTest (fun u => (v u : ℂ))) (hev : ∀ u, v (-u) = epsR par * v u) + (hsupp : tsupport (fun u => (v u : ℂ)) ⊆ Icc (-L0) L0) : + Rb par v v ≤ (WeilForm.weilForm (WeilForm.autocorr (fun u => (v u : ℂ)))).re := by + have hε : epsR par * epsR par = 1 := by unfold epsR; split_ifs <;> norm_num + rw [symbol_representation_ofReal hε hf hev hsupp] + set F : ℝ → ℝ := fun r => ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2 + with hF + have hFT : ∀ t, F t = (Tr ellR par v t) ^ 2 := fun t => norm_sq_line_sector hpar hf hev hsupp t + have hFc : Continuous F := by + have : F = fun t => (Tr ellR par v t) ^ 2 := funext hFT + rw [this] + exact (continuous_Tr ellR par (continuous_v hf)).pow 2 + have hFi : Integrable F := integrable_line_sq hf + have hFpsi := integrable_line_sq_mul_psi hf + have hFPi : Integrable fun t => F t * Psi t := by + have e : (fun t => F t * Psi t) = fun t => F t * psiR t - F t * Real.log Real.pi := by + funext t; unfold Psi; ring + rw [e] + exact hFpsi.sub (hFi.mul_const _) + have hF0 : ∀ t, 0 ≤ F t := fun t => by rw [hF]; positivity + have hTneg : ∀ t, Tr ellR par v (-t) = (if par = 0 then (1 : ℝ) else -1) * Tr ellR par v t := by + intro t + unfold Tr + rw [← intervalIntegral.integral_const_mul] + congr 1 + funext x + rw [show -t * x = -(t * x) by ring, phiF_neg par hpar] + ring + have hFe : ∀ t, F (-t) = F t := by + intro t + rw [hFT, hFT, hTneg, mul_pow] + split_ifs <;> norm_num + have hsplit := split_line hFi hFPi hF0 hFe hFc + have e1 : (fun t : ℝ => ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (t : ℂ) * Complex.I)‖ ^ 2 + * WeilWindow.weilSymbol L0 t) = fun t => F t * Psi t := by + funext t; rw [weilSymbol_L0] + rw [e1] + have hplan := plancherel_ofReal hf + have hip : ip ellR v v = ∫ x, v x ^ 2 := by + unfold ip + rw [← integral_eq_interval hsupp] + congr 1; funext x; ring + have hpole := K0_sq hpar hf hev hsupp + unfold Rb + rw [hpole, hip, hplan] + have e2 : (fun t => (Psi t - beta0R) * (Tr ellR par v t * Tr ellR par v t)) + = fun t => (Psi t - beta0R) * F t := by funext t; rw [hFT]; ring + rw [e2] + have e3 : (fun r : ℝ => ‖weilKernel (fun u => (v u : ℂ)) (1 / 2 + (r : ℂ) * Complex.I)‖ ^ 2) = F := rfl + rw [e3] + nlinarith [hsplit] + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Tail.lean b/telperion/examples/rvm_bridge/lean/KWin_Tail.lean new file mode 100644 index 000000000..91b4607c0 --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Tail.lean @@ -0,0 +1,393 @@ +/- + KWin_Tail -- the projection tail and the sector floor of the split form (rvm_bridge island, + 2026-09-24). + + conjecture1_proved = False. (Finite-window Weil positivity is not RH; PR #604: the 1.3e-3 + full-class margin at this window is zero content; not Connes-Consani, whose theorem is for the + pole-free class.) + + PROVED HERE (`Rb_floor`): for EVERY continuous v and each sector, + lam' int_{-l}^{l} v^2 <= Rb par v v, lam' = 9/10000, + from the head certificate (KWin_Head.head_floor) and a PROJECTION tail that needs no Legendre + completeness: h = sum_{k= dT int r^2, + and (lam - lam')(dT - lam') >= 4 kapT^2 l^2 (kernel-checked) closes the 2x2 bound through + (int|f|)^2 <= 2 l int f^2. No `sorry`. +-/ +import KWin_Head + +open Real Finset MeasureTheory intervalIntegral + +noncomputable section + +namespace KWin +open RvMBridge11 + +/-! ## A. Linearity. -/ + +lemma int_add_mul {f g w : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (hw : Continuous w) (a b : ℝ) : + ∫ x in a..b, (f x + g x) * w x = (∫ x in a..b, f x * w x) + ∫ x in a..b, g x * w x := by + have h1 : IntervalIntegrable (fun x => f x * w x) volume a b := (hf.mul hw).intervalIntegrable _ _ + have h2 : IntervalIntegrable (fun x => g x * w x) volume a b := (hg.mul hw).intervalIntegrable _ _ + rw [← intervalIntegral.integral_add h1 h2] + congr 1; funext x; ring + +lemma Pl_add {par : ℕ} {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) : + Pl ellR par (fun x => f x + g x) = Pl ellR par f + Pl ellR par g := + int_add_mul hf hg (continuous_poleF par) _ _ + +lemma Tr_add {par : ℕ} {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (t : ℝ) : + Tr ellR par (fun x => f x + g x) t = Tr ellR par f t + Tr ellR par g t := + int_add_mul hf hg ((continuous_phiF par).comp (continuous_const.mul continuous_id)) _ _ + +lemma ip_add_left {f g w : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (hw : Continuous w) : + ip ellR (fun x => f x + g x) w = ip ellR f w + ip ellR g w := + int_add_mul hf hg hw _ _ + +lemma ip_comm (f g : ℝ → ℝ) : ip ellR f g = ip ellR g f := by + unfold ip; congr 1; funext x; ring + +lemma mo_sub {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) (n : ℕ) : + mo ellR (fun x => f x - g x) n = mo ellR f n - mo ellR g n := by + unfold mo + have h1 : IntervalIntegrable (fun x => f x * (x / ellR) ^ n) volume (-ellR) ellR := + (hf.mul (by fun_prop)).intervalIntegrable _ _ + have h2 : IntervalIntegrable (fun x => g x * (x / ellR) ^ n) volume (-ellR) ellR := + (hg.mul (by fun_prop)).intervalIntegrable _ _ + rw [← intervalIntegral.integral_sub h1 h2] + congr 1; funext x; beta_reduce; ring + +lemma Rb_comm (par : ℕ) (f g : ℝ → ℝ) : Rb par f g = Rb par g f := by + unfold Rb + rw [ip_comm f g] + have e : (fun t => (Psi t - beta0R) * (Tr ellR par f t * Tr ellR par g t)) + = fun t => (Psi t - beta0R) * (Tr ellR par g t * Tr ellR par f t) := by funext t; ring + rw [e] + ring + +/-- The bilinear expansion `R(h + r) = R(h) + 2 R(h, r) + R(r)`. -/ +theorem Rb_expand (par : ℕ) {h r : ℝ → ℝ} (hh : Continuous h) (hr : Continuous r) : + Rb par (fun x => h x + r x) (fun x => h x + r x) = Rb par h h + 2 * Rb par h r + Rb par r r := by + have hs : Continuous (fun x => h x + r x) := hh.add hr + unfold Rb + rw [Pl_add hh hr, ip_add_left hh hr hs, ip_comm h, ip_comm r, ip_add_left hh hr hh, + ip_add_left hh hr hr, ip_comm r h] + have cTh := continuous_Tr ellR par hh + have cTr := continuous_Tr ellR par hr + have cP : Continuous fun t => Psi t - beta0R := continuous_Psi.sub continuous_const + have e : (fun t => (Psi t - beta0R) * (Tr ellR par (fun x => h x + r x) t + * Tr ellR par (fun x => h x + r x) t)) + = fun t => ((Psi t - beta0R) * (Tr ellR par h t * Tr ellR par h t) + + 2 * ((Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t))) + + (Psi t - beta0R) * (Tr ellR par r t * Tr ellR par r t) := by + funext t; rw [Tr_add hh hr t]; ring + rw [e, intervalIntegral.integral_add (Continuous.intervalIntegrable (by fun_prop) _ _) + (Continuous.intervalIntegrable (by fun_prop) _ _), + intervalIntegral.integral_add (Continuous.intervalIntegrable (by fun_prop) _ _) + (Continuous.intervalIntegrable (by fun_prop) _ _), + intervalIntegral.integral_const_mul] + ring + +/-! ## B. Integral bounds on [0, 20]. -/ + +lemma abs_int_le_of_abs_le {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) + (h : ∀ t ∈ Set.Icc (0 : ℝ) 20, |f t| ≤ g t) : + |∫ t in (0 : ℝ)..20, f t| ≤ ∫ t in (0 : ℝ)..20, g t := by + refine (intervalIntegral.abs_integral_le_integral_abs (by norm_num)).trans ?_ + exact intervalIntegral.integral_mono_on (by norm_num) (hf.abs.intervalIntegrable _ _) + (hg.intervalIntegrable _ _) h + +/-! ## C. The sector floor. -/ + +set_option maxHeartbeats 1000000 in +theorem Rb_floor {par N : ℕ} (hpar : par = 0 ∨ par = 1) {lam : ℚ} + (htail : tailCond par N lam = true) (hcert : psdCert (headMat par N lam) N = true) + (hginv : ginvCheck par N = true) {v : ℝ → ℝ} (hv : Continuous v) : + ((lamFloor : ℚ) : ℝ) * ip ellR v v ≤ Rb par v v := by + obtain ⟨hl1, hl2, hl3, _, _, hN, _⟩ := tailCond_sound htail + have hl := ellR_pos + -- the projection + set b : ℕ → ℝ := fun l => mo ellR v (2 * l + par) with hbdef + set a : ℕ → ℝ := fun j => ∑ l ∈ range N, ((mget (ginv par) j l : ℚ) : ℝ) * b l with hadef + set h := hfun par N a with hhdef + have hc : Continuous h := continuous_hfun par N a + set r : ℝ → ℝ := fun x => v x - h x with hrdef + have hrc : Continuous r := hv.sub hc + have hvhr : v = fun x => h x + r x := by funext x; simp only [hrdef]; ring + -- orthogonality + have horth : ∀ m < N, mo ellR r (2 * m + par) = 0 := by + intro m hm + rw [hrdef, mo_sub hv hc, hhdef, mo_hfun] + have hsum : ∑ k ∈ range N, a k * ((Gm par k m : ℚ) : ℝ) = b m := by + rw [hadef] + simp only + simp_rw [Finset.sum_mul] + rw [Finset.sum_comm] + have hδ : ∀ l ∈ range N, ∑ k ∈ range N, ((mget (ginv par) k l : ℚ) : ℝ) * b l * ((Gm par k m : ℚ) : ℝ) + = if m = l then b l else 0 := by + intro l hlN + have hG := ginvCheck_sound hginv hm (Finset.mem_range.mp hlN) + have hG' : ∑ k ∈ range N, ((Gm par m k : ℚ) : ℝ) * ((mget (ginv par) k l : ℚ) : ℝ) + = if m = l then 1 else 0 := by + have := congrArg (fun q : ℚ => (q : ℝ)) hG + push_cast at this + rw [this] + split_ifs <;> simp + have e : ∑ k ∈ range N, ((mget (ginv par) k l : ℚ) : ℝ) * b l * ((Gm par k m : ℚ) : ℝ) + = (∑ k ∈ range N, ((Gm par m k : ℚ) : ℝ) * ((mget (ginv par) k l : ℚ) : ℝ)) * b l := by + rw [Finset.sum_mul] + refine Finset.sum_congr rfl fun k _ => ?_ + rw [Gm_symm par k m] + ring + rw [e, hG'] + split_ifs <;> simp + rw [Finset.sum_congr rfl hδ, Finset.sum_ite_eq] + simp [Finset.mem_range.mpr hm] + rw [hsum] + simp [hbdef] + -- int h r = 0 + have hhr : ip ellR h r = 0 := by + rw [hhdef, ip_hfun_left par N a hrc] + exact Finset.sum_eq_zero fun k hk => by rw [horth k (Finset.mem_range.mp hk), mul_zero] + -- tail transform and pole bounds + set A := A1 ellR h with hAdef + set B := A1 ellR r with hBdef + have hA0 : 0 ≤ A := A1_nonneg hl.le h + have hB0 : 0 ≤ B := A1_nonneg hl.le r + set X := ip ellR h h with hXdef + set Y := ip ellR r r with hYdef + have hsqX : A ^ 2 ≤ 2 * ellR * X := by + have := A1_sq_le hl hc + rw [hXdef]; unfold ip + have e : (fun x => h x ^ 2) = fun x => h x * h x := by funext x; ring + rwa [e] at this + have hsqY : B ^ 2 ≤ 2 * ellR * Y := by + have := A1_sq_le hl hrc + rw [hYdef]; unfold ip + have e : (fun x => r x ^ 2) = fun x => r x * r x := by funext x; ring + rwa [e] at this + have hX0 : 0 ≤ X := by + rw [hXdef]; unfold ip + exact intervalIntegral.integral_nonneg (by linarith) fun x _ => mul_self_nonneg _ + have hY0 : 0 ≤ Y := by + rw [hYdef]; unfold ip + exact intervalIntegral.integral_nonneg (by linarith) fun x _ => mul_self_nonneg _ + have hTr : ∀ t ∈ Set.Icc (0 : ℝ) 20, |Tr ellR par r t| ≤ epsW (2 * N + par) t * B := by + intro t ht + have htl : t * ellR ≤ (2 * N + par + 1) / 2 := by + have h1 : t * ellR ≤ 20 * ellR := mul_le_mul_of_nonneg_right ht.2 hl.le + have h2 := (Rat.cast_le (K := ℝ)).mpr hN + unfold TQ at h2 + push_cast at h2 + have e : (20 : ℝ) * ellR = (20 : ℝ) * ((ellQ : ℚ) : ℝ) := rfl + linarith + have := Tr_sub_le hl hpar hrc ht.1 htl + have hz : ∑ m ∈ range N, (-1) ^ m * (t * ellR) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo ellR r (2 * m + par) = 0 := + Finset.sum_eq_zero fun m hm => by rw [horth m (Finset.mem_range.mp hm), mul_zero] + rw [hz, sub_zero] at this + unfold epsW + exact this + set dN : ℝ := 2 * (ellR / 2) ^ (2 * N + par) / ((2 * N + par).factorial : ℝ) with hdN + have hdN0 : 0 ≤ dN := by rw [hdN]; positivity + have hPr : |Pl ellR par r| ≤ dN * B := by + have hNpos : 0 < 2 * N + par := by + by_contra hc' + have h0 : N = 0 ∧ par = 0 := by omega + obtain ⟨h1, h2⟩ := h0 + subst h1 h2 + unfold TQ ellQ at hN + norm_num at hN + have := Pl_sub_le hl (by rw [ellR_eq]; norm_num) hpar hNpos hrc + have hz : ∑ m ∈ range N, (ellR / 2) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo ellR r (2 * m + par) = 0 := + Finset.sum_eq_zero fun m hm => by rw [horth m (Finset.mem_range.mp hm), mul_zero] + rw [hz, sub_zero] at this + rw [hdN]; exact this + have hPh : |Pl ellR par h| ≤ ((CpQ : ℚ) : ℝ) * A := by + have h1 := abs_Pl_le hl par hc + have h2 := cosh_half_ell_le + exact h1.trans (mul_le_mul_of_nonneg_right h2 hA0) + have hTh : ∀ t, |Tr ellR par h t| ≤ A := fun t => abs_Tr_le hl par hc t + -- constants + have hpi := Real.pi_pos + have hpi3 : 3 ≤ Real.pi := Real.pi_gt_three.le + have hS0 : (0 : ℝ) ≤ ((S0Q : ℚ) : ℝ) := by unfold S0Q; push_cast; norm_num + have hCp : (0 : ℝ) ≤ ((CpQ : ℚ) : ℝ) := by unfold CpQ; push_cast; norm_num + set I1 := ∫ t in (0 : ℝ)..20, epsW (2 * N + par) t with hI1 + set I2 := ∫ t in (0 : ℝ)..20, epsW (2 * N + par) t ^ 2 with hI2 + have hI10 : 0 ≤ I1 := intervalIntegral.integral_nonneg (by norm_num) fun t ht => epsW_nonneg _ ht.1 + have hI20 : 0 ≤ I2 := intervalIntegral.integral_nonneg (by norm_num) fun t _ => sq_nonneg _ + have hkap : ((kapT par N : ℚ) : ℝ) = 2 * ((CpQ : ℚ) : ℝ) * dN + ((S0Q : ℚ) : ℝ) / 3 * I1 := by + rw [hI1, int_epsW] + unfold kapT dPT I1T + rw [hdN] + unfold ellR TQ + push_cast + ring + have hdT : ((dT par N : ℚ) : ℝ) = beta0R - 2 * ellR * (2 * dN ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2) := by + rw [hI2, int_epsW_sq] + unfold dT dPT I2T + rw [hdN] + unfold ellR TQ beta0R + push_cast + ring + have hcP : Continuous fun t => Psi t - beta0R := continuous_Psi.sub continuous_const + have cTh := continuous_Tr ellR par hc + have cTr := continuous_Tr ellR par hrc + have hce := continuous_epsW (2 * N + par) + -- the coupling + have hcross : |Rb par h r| ≤ ((kapT par N : ℚ) : ℝ) * (A * B) := by + unfold Rb + rw [hhr, mul_zero, add_zero] + have h1 : |2 * epsR par * Pl ellR par h * Pl ellR par r| ≤ 2 * ((CpQ : ℚ) : ℝ) * dN * (A * B) := by + have he : |epsR par| = 1 := by unfold epsR; split_ifs <;> simp + rw [abs_mul, abs_mul, abs_mul, he, abs_two] + calc 2 * 1 * |Pl ellR par h| * |Pl ellR par r| ≤ 2 * 1 * (((CpQ : ℚ) : ℝ) * A) * (dN * B) := by + gcongr + _ = 2 * ((CpQ : ℚ) : ℝ) * dN * (A * B) := by ring + have h2 : |(1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t)| + ≤ ((S0Q : ℚ) : ℝ) / 3 * I1 * (A * B) := by + rw [abs_mul, abs_of_pos (by positivity : (0 : ℝ) < 1 / Real.pi)] + have hb := abs_int_le_of_abs_le (f := fun t => (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t)) + (g := fun t => ((S0Q : ℚ) : ℝ) * (A * (epsW (2 * N + par) t * B))) (by fun_prop) (by fun_prop) + (by + intro t ht + rw [abs_mul, abs_mul] + exact mul_le_mul (abs_Psi_sub_beta0_le ht.1 ht.2) + (mul_le_mul (hTh t) (hTr t ht) (abs_nonneg _) hA0) (by positivity) hS0) + have e : ∫ t in (0 : ℝ)..20, ((S0Q : ℚ) : ℝ) * (A * (epsW (2 * N + par) t * B)) + = ((S0Q : ℚ) : ℝ) * I1 * (A * B) := by + rw [hI1] + have e2 : (fun t => ((S0Q : ℚ) : ℝ) * (A * (epsW (2 * N + par) t * B))) + = fun t => (((S0Q : ℚ) : ℝ) * (A * B)) * epsW (2 * N + par) t := by funext t; ring + rw [e2, intervalIntegral.integral_const_mul] + ring + rw [e] at hb + have hSIAB : 0 ≤ ((S0Q : ℚ) : ℝ) * I1 * (A * B) := by positivity + calc 1 / Real.pi * |∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t)| + ≤ 1 / Real.pi * (((S0Q : ℚ) : ℝ) * I1 * (A * B)) := + mul_le_mul_of_nonneg_left hb (by positivity) + _ ≤ 1 / 3 * (((S0Q : ℚ) : ℝ) * I1 * (A * B)) := + mul_le_mul_of_nonneg_right (one_div_le_one_div_of_le (by norm_num) hpi3) hSIAB + _ = ((S0Q : ℚ) : ℝ) / 3 * I1 * (A * B) := by ring + rw [hkap] + calc |2 * epsR par * Pl ellR par h * Pl ellR par r + + (1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t)| + ≤ |2 * epsR par * Pl ellR par h * Pl ellR par r| + + |(1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par h t * Tr ellR par r t)| := + abs_add_le _ _ + _ ≤ 2 * ((CpQ : ℚ) : ℝ) * dN * (A * B) + ((S0Q : ℚ) : ℝ) / 3 * I1 * (A * B) := add_le_add h1 h2 + _ = (2 * ((CpQ : ℚ) : ℝ) * dN + ((S0Q : ℚ) : ℝ) / 3 * I1) * (A * B) := by ring + -- the tail term + have htailR : ((dT par N : ℚ) : ℝ) * Y ≤ Rb par r r := by + unfold Rb + rw [← hYdef] + have h1 : -2 * dN ^ 2 * B ^ 2 ≤ 2 * epsR par * Pl ellR par r * Pl ellR par r := by + have hP2 : Pl ellR par r ^ 2 ≤ (dN * B) ^ 2 := + sq_le_sq' (abs_le.mp hPr).1 (abs_le.mp hPr).2 + unfold epsR + split_ifs + · nlinarith [sq_nonneg (Pl ellR par r)] + · nlinarith + have h2 : -(((S0Q : ℚ) : ℝ) / 3 * I2 * B ^ 2) + ≤ (1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par r t * Tr ellR par r t) := by + have hb := abs_int_le_of_abs_le (f := fun t => (Psi t - beta0R) * (Tr ellR par r t * Tr ellR par r t)) + (g := fun t => ((S0Q : ℚ) : ℝ) * (epsW (2 * N + par) t ^ 2 * B ^ 2)) (by fun_prop) (by fun_prop) + (by + intro t ht + rw [abs_mul, abs_mul] + have hT := hTr t ht + have hTT : |Tr ellR par r t| * |Tr ellR par r t| ≤ epsW (2 * N + par) t ^ 2 * B ^ 2 := by + have := mul_le_mul hT hT (abs_nonneg _) (by have := epsW_nonneg (2 * N + par) ht.1; positivity) + nlinarith + exact mul_le_mul (abs_Psi_sub_beta0_le ht.1 ht.2) hTT (by positivity) hS0) + have e : ∫ t in (0 : ℝ)..20, ((S0Q : ℚ) : ℝ) * (epsW (2 * N + par) t ^ 2 * B ^ 2) + = ((S0Q : ℚ) : ℝ) * I2 * B ^ 2 := by + rw [hI2] + have e2 : (fun t => ((S0Q : ℚ) : ℝ) * (epsW (2 * N + par) t ^ 2 * B ^ 2)) + = fun t => (((S0Q : ℚ) : ℝ) * B ^ 2) * epsW (2 * N + par) t ^ 2 := by funext t; ring + rw [e2, intervalIntegral.integral_const_mul] + ring + rw [e] at hb + have hSIB : 0 ≤ ((S0Q : ℚ) : ℝ) * I2 * B ^ 2 := by positivity + have hq := neg_abs_le (∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par r t * Tr ellR par r t)) + have h3 : -(1 / Real.pi) * (((S0Q : ℚ) : ℝ) * I2 * B ^ 2) + ≤ (1 / Real.pi) * ∫ t in (0 : ℝ)..20, (Psi t - beta0R) * (Tr ellR par r t * Tr ellR par r t) := by + have := mul_le_mul_of_nonneg_left (le_trans (neg_le_neg hb) hq) (by positivity : (0 : ℝ) ≤ 1 / Real.pi) + linarith + have h4 : (1 / Real.pi) * (((S0Q : ℚ) : ℝ) * I2 * B ^ 2) ≤ 1 / 3 * (((S0Q : ℚ) : ℝ) * I2 * B ^ 2) := + mul_le_mul_of_nonneg_right (one_div_le_one_div_of_le (by norm_num) hpi3) hSIB + linarith + rw [hdT] + have hK0 : (0 : ℝ) ≤ 2 * dN ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2 := by positivity + have hK := mul_le_mul_of_nonneg_left hsqY hK0 + have e1 : (beta0R - 2 * ellR * (2 * dN ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2)) * Y + = beta0R * Y - (2 * dN ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2) * (2 * ellR * Y) := by ring + have e2 : (2 * dN ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2) * B ^ 2 + = 2 * dN ^ 2 * B ^ 2 + ((S0Q : ℚ) : ℝ) / 3 * I2 * B ^ 2 := by ring + rw [e1] + linarith [h1, h2, hK, e2] + -- the head term + have hhead : ((lam : ℚ) : ℝ) * X ≤ Rb par h h := by + rw [hXdef, hhdef] + exact head_floor hpar htail hcert a + -- assembly + have hRv : Rb par v v = Rb par h h + 2 * Rb par h r + Rb par r r := by + rw [hvhr]; exact Rb_expand par hc hrc + have hIv : ip ellR v v = X + Y := by + have hs : Continuous (fun x => h x + r x) := hc.add hrc + rw [hvhr, ip_add_left hc hrc hs, ip_comm h, ip_comm r, ip_add_left hc hrc hc, + ip_add_left hc hrc hrc, ip_comm r h, hhr, hXdef, hYdef] + ring + rw [hRv, hIv] + have hl1R : ((lamFloor : ℚ) : ℝ) ≤ ((lam : ℚ) : ℝ) := by exact_mod_cast hl1 + have hl2R : ((lamFloor : ℚ) : ℝ) ≤ ((dT par N : ℚ) : ℝ) := by exact_mod_cast hl2 + have hl3R : 4 * ((kapT par N : ℚ) : ℝ) ^ 2 * ellR ^ 2 + ≤ (((lam : ℚ) : ℝ) - ((lamFloor : ℚ) : ℝ)) * (((dT par N : ℚ) : ℝ) - ((lamFloor : ℚ) : ℝ)) := by + have := (Rat.cast_le (K := ℝ)).mpr hl3 + push_cast at this + exact this + have hk0 : 0 ≤ ((kapT par N : ℚ) : ℝ) := by rw [hkap]; positivity + -- 2x2: (lam - lam') X + (d - lam') Y >= 2 kap A B + set α := ((lam : ℚ) : ℝ) - ((lamFloor : ℚ) : ℝ) with hα + set δ := ((dT par N : ℚ) : ℝ) - ((lamFloor : ℚ) : ℝ) with hδ + set κ := ((kapT par N : ℚ) : ℝ) with hκ + have hα0 : 0 ≤ α := by rw [hα]; linarith + have hδ0 : 0 ≤ δ := by rw [hδ]; linarith + have hAB : (A * B) ^ 2 ≤ 4 * ellR ^ 2 * (X * Y) := by + have := mul_le_mul hsqX hsqY (sq_nonneg B) (by positivity) + nlinarith + have hkey : 2 * κ * (A * B) ≤ α * X + δ * Y := by + have hsq1 : (2 * κ * (A * B)) ^ 2 ≤ (α * X + δ * Y) ^ 2 := by + have e1 : (2 * κ * (A * B)) ^ 2 = 4 * κ ^ 2 * (A * B) ^ 2 := by ring + have e2 : 4 * κ ^ 2 * (A * B) ^ 2 ≤ 4 * κ ^ 2 * (4 * ellR ^ 2 * (X * Y)) := + mul_le_mul_of_nonneg_left hAB (by positivity) + have e3 : 4 * κ ^ 2 * (4 * ellR ^ 2 * (X * Y)) ≤ 4 * (α * δ) * (X * Y) := by + have := mul_le_mul_of_nonneg_right hl3R (by positivity : (0 : ℝ) ≤ 4 * (X * Y)) + nlinarith + have e4 : 4 * (α * δ) * (X * Y) ≤ (α * X + δ * Y) ^ 2 := by + nlinarith [sq_nonneg (α * X - δ * Y)] + linarith + have hpos : 0 ≤ α * X + δ * Y := by positivity + exact (pow_le_pow_iff_left₀ (by positivity) hpos (by norm_num : (2 : ℕ) ≠ 0)).mp hsq1 + have hcr := (abs_le.mp hcross).1 + have hl' : ((lam : ℚ) : ℝ) = α + ((lamFloor : ℚ) : ℝ) := by rw [hα]; ring + have hd' : ((dT par N : ℚ) : ℝ) = δ + ((lamFloor : ℚ) : ℝ) := by rw [hδ]; ring + rw [hl'] at hhead + rw [hd'] at htailR + have e3 : (α + ((lamFloor : ℚ) : ℝ)) * X = α * X + ((lamFloor : ℚ) : ℝ) * X := by ring + have e4 : (δ + ((lamFloor : ℚ) : ℝ)) * Y = δ * Y + ((lamFloor : ℚ) : ℝ) * Y := by ring + rw [e3] at hhead + rw [e4] at htailR + have e5 : ((lamFloor : ℚ) : ℝ) * (X + Y) = ((lamFloor : ℚ) : ℝ) * X + ((lamFloor : ℚ) : ℝ) * Y := by ring + rw [e5] + linarith [hkey, hhead, htailR, hcr] + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Taylor.lean b/telperion/examples/rvm_bridge/lean/KWin_Taylor.lean new file mode 100644 index 000000000..8ccefbf0b --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Taylor.lean @@ -0,0 +1,427 @@ +/- + KWin_Taylor -- parity-generic Taylor remainders and the finite-interval transform calculus of + the KWin certificate (rvm_bridge island, 2026-09-24). + + For par = 0 (even sector) / par = 1 (odd sector): + phiF par = cos / sin, poleF par x = cosh(x/2) / sinh(x/2), + tayl par M y = sum_{m Tr f t. Pure real analysis; nothing + about zeros. conjecture1_proved = False. No `sorry`. +-/ +import Mathlib + +open Finset MeasureTheory intervalIntegral + +noncomputable section + +namespace KWin + +/-! ## A. Definitions. -/ + +def phiF (par : ℕ) (y : ℝ) : ℝ := if par = 0 then Real.cos y else Real.sin y +def poleF (par : ℕ) (x : ℝ) : ℝ := if par = 0 then Real.cosh (x / 2) else Real.sinh (x / 2) +def tayl (par M : ℕ) (y : ℝ) : ℝ := + ∑ m ∈ range M, (-1) ^ m * y ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) +def ptayl (par M : ℕ) (y : ℝ) : ℝ := ∑ m ∈ range M, y ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + +/-- `int_{-l}^{l} |f|`. -/ +def A1 (l : ℝ) (f : ℝ → ℝ) : ℝ := ∫ x in (-l)..l, |f x| +/-- `int_{-l}^{l} f(x) (x/l)^n dx`. -/ +def mo (l : ℝ) (f : ℝ → ℝ) (n : ℕ) : ℝ := ∫ x in (-l)..l, f x * (x / l) ^ n +/-- The sector transform `int_{-l}^{l} f(x) phiF(t x) dx` (cosine / sine transform). -/ +def Tr (l : ℝ) (par : ℕ) (f : ℝ → ℝ) (t : ℝ) : ℝ := ∫ x in (-l)..l, f x * phiF par (t * x) +/-- The sector pole functional `int_{-l}^{l} f(x) poleF(x) dx`. -/ +def Pl (l : ℝ) (par : ℕ) (f : ℝ → ℝ) : ℝ := ∫ x in (-l)..l, f x * poleF par x +/-- `int_{-l}^{l} f g`. -/ +def ip (l : ℝ) (f g : ℝ → ℝ) : ℝ := ∫ x in (-l)..l, f x * g x + +lemma continuous_phiF (par : ℕ) : Continuous (phiF par) := by + by_cases h : par = 0 + · have e : phiF par = Real.cos := by funext y; simp [phiF, h] + rw [e]; exact Real.continuous_cos + · have e : phiF par = Real.sin := by funext y; simp [phiF, h] + rw [e]; exact Real.continuous_sin + +lemma continuous_poleF (par : ℕ) : Continuous (poleF par) := by + by_cases h : par = 0 + · have e : poleF par = fun x => Real.cosh (x / 2) := by funext y; simp [poleF, h] + rw [e]; fun_prop + · have e : poleF par = fun x => Real.sinh (x / 2) := by funext y; simp [poleF, h] + rw [e]; fun_prop + +lemma continuous_tayl (par M : ℕ) : Continuous (tayl par M) := by + unfold tayl; fun_prop + +lemma continuous_ptayl (par M : ℕ) : Continuous (ptayl par M) := by + unfold ptayl; fun_prop + +lemma abs_phiF_le (par : ℕ) (y : ℝ) : |phiF par y| ≤ 1 := by + by_cases h : par = 0 + · simp only [phiF, h, if_true]; exact Real.abs_cos_le_one y + · simp only [phiF, h, if_false]; exact Real.abs_sin_le_one y + +lemma phiF_neg (par : ℕ) (hpar : par = 0 ∨ par = 1) (y : ℝ) : + phiF par (-y) = (if par = 0 then 1 else -1) * phiF par y := by + rcases hpar with h | h <;> subst h <;> simp [phiF] + +/-! ## B. Finite-sum bookkeeping. -/ + +lemma sum_range_two_mul {β : Type*} [AddCommMonoid β] (f : ℕ → β) (M : ℕ) : + ∑ k ∈ range (2 * M), f k = ∑ m ∈ range M, (f (2 * m) + f (2 * m + 1)) := by + induction M with + | zero => simp + | succ M ih => + rw [show 2 * (M + 1) = 2 * M + 1 + 1 by ring, Finset.sum_range_succ, Finset.sum_range_succ, ih, + Finset.sum_range_succ] + abel + +lemma expI_sum_even (y : ℝ) (M : ℕ) : + ∑ k ∈ range (2 * M), ((y : ℂ) * Complex.I) ^ k / (k.factorial : ℂ) + = ((tayl 0 M y : ℝ) : ℂ) + ((tayl 1 M y : ℝ) : ℂ) * Complex.I := by + rw [sum_range_two_mul] + unfold tayl + push_cast + rw [Finset.sum_mul, ← Finset.sum_add_distrib] + refine Finset.sum_congr rfl fun m _ => ?_ + have h1 : ((y : ℂ) * Complex.I) ^ (2 * m) = (-1) ^ m * (y : ℂ) ^ (2 * m) := by + rw [mul_pow, pow_mul Complex.I, Complex.I_sq]; ring + have h2 : ((y : ℂ) * Complex.I) ^ (2 * m + 1) = (-1) ^ m * (y : ℂ) ^ (2 * m + 1) * Complex.I := by + rw [pow_succ, h1]; ring + simp only [add_zero] + rw [h1, h2] + ring + +lemma expI_sum_odd (y : ℝ) (M : ℕ) : + ∑ k ∈ range (2 * M + 1), ((y : ℂ) * Complex.I) ^ k / (k.factorial : ℂ) + = ((tayl 0 (M + 1) y : ℝ) : ℂ) + ((tayl 1 M y : ℝ) : ℂ) * Complex.I := by + rw [Finset.sum_range_succ, expI_sum_even] + have h1 : ((y : ℂ) * Complex.I) ^ (2 * M) = (-1) ^ M * (y : ℂ) ^ (2 * M) := by + rw [mul_pow, pow_mul Complex.I, Complex.I_sq]; ring + rw [h1] + unfold tayl + rw [Finset.sum_range_succ] + push_cast + simp only [add_zero] + ring + +lemma exp_sum_add_neg_even (y : ℝ) (M : ℕ) : + ∑ k ∈ range (2 * M), y ^ k / (k.factorial : ℝ) + ∑ k ∈ range (2 * M), (-y) ^ k / (k.factorial : ℝ) + = 2 * ptayl 0 M y := by + rw [← Finset.sum_add_distrib, sum_range_two_mul] + unfold ptayl + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun m _ => ?_ + have e1 : (-y) ^ (2 * m) = y ^ (2 * m) := by rw [pow_mul, neg_sq, ← pow_mul] + have e2 : (-y) ^ (2 * m + 1) = -y ^ (2 * m + 1) := by rw [pow_succ, e1]; ring + simp only [add_zero] + rw [e1, e2] + ring + +lemma exp_sum_sub_neg_odd (y : ℝ) (M : ℕ) : + ∑ k ∈ range (2 * M + 1), y ^ k / (k.factorial : ℝ) + - ∑ k ∈ range (2 * M + 1), (-y) ^ k / (k.factorial : ℝ) = 2 * ptayl 1 M y := by + rw [← Finset.sum_sub_distrib, Finset.sum_range_succ, sum_range_two_mul] + have e0 : (-y) ^ (2 * M) = y ^ (2 * M) := by rw [pow_mul, neg_sq, ← pow_mul] + rw [e0, sub_self, add_zero] + unfold ptayl + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun m _ => ?_ + have e1 : (-y) ^ (2 * m) = y ^ (2 * m) := by rw [pow_mul, neg_sq, ← pow_mul] + have e2 : (-y) ^ (2 * m + 1) = -y ^ (2 * m + 1) := by rw [pow_succ, e1]; ring + rw [e1, e2] + ring + +/-! ## C. Pointwise Taylor remainders. -/ + +lemma cos_sub_tayl_le {y : ℝ} {M : ℕ} (hy : |y| ≤ (2 * M + 1) / 2) : + |Real.cos y - tayl 0 M y| ≤ 2 * |y| ^ (2 * M) / ((2 * M).factorial : ℝ) := by + have hx : ‖(y : ℂ) * Complex.I‖ / ((2 * M).succ : ℝ) ≤ 1 / 2 := by + rw [norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs, + div_le_iff₀ (by positivity)] + push_cast + linarith + have h := Complex.exp_bound' hx + rw [expI_sum_even] at h + have e : Complex.exp ((y : ℂ) * Complex.I) - (((tayl 0 M y : ℝ) : ℂ) + ((tayl 1 M y : ℝ) : ℂ) * Complex.I) + = ((Real.cos y - tayl 0 M y : ℝ) : ℂ) + ((Real.sin y - tayl 1 M y : ℝ) : ℂ) * Complex.I := by + rw [Complex.exp_mul_I, ← Complex.ofReal_cos, ← Complex.ofReal_sin] + push_cast + ring + rw [e] at h + have hre := Complex.abs_re_le_norm (((Real.cos y - tayl 0 M y : ℝ) : ℂ) + + ((Real.sin y - tayl 1 M y : ℝ) : ℂ) * Complex.I) + simp only [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im, + Complex.I_im, mul_zero, zero_mul, sub_zero, add_zero] at hre + rw [norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs] at h + calc |Real.cos y - tayl 0 M y| ≤ _ := hre + _ ≤ _ := h + _ = 2 * |y| ^ (2 * M) / ((2 * M).factorial : ℝ) := by ring + +lemma sin_sub_tayl_le {y : ℝ} {M : ℕ} (hy : |y| ≤ (2 * M + 1 + 1) / 2) : + |Real.sin y - tayl 1 M y| ≤ 2 * |y| ^ (2 * M + 1) / ((2 * M + 1).factorial : ℝ) := by + have hx : ‖(y : ℂ) * Complex.I‖ / ((2 * M + 1).succ : ℝ) ≤ 1 / 2 := by + rw [norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs, + div_le_iff₀ (by positivity)] + push_cast + linarith + have h := Complex.exp_bound' hx + rw [expI_sum_odd] at h + have e : Complex.exp ((y : ℂ) * Complex.I) + - (((tayl 0 (M + 1) y : ℝ) : ℂ) + ((tayl 1 M y : ℝ) : ℂ) * Complex.I) + = ((Real.cos y - tayl 0 (M + 1) y : ℝ) : ℂ) + ((Real.sin y - tayl 1 M y : ℝ) : ℂ) * Complex.I := by + rw [Complex.exp_mul_I, ← Complex.ofReal_cos, ← Complex.ofReal_sin] + push_cast + ring + rw [e] at h + have him := Complex.abs_im_le_norm (((Real.cos y - tayl 0 (M + 1) y : ℝ) : ℂ) + + ((Real.sin y - tayl 1 M y : ℝ) : ℂ) * Complex.I) + simp only [Complex.add_im, Complex.ofReal_im, Complex.mul_im, Complex.I_re, Complex.ofReal_re, + Complex.I_im, mul_zero, mul_one, zero_add, add_zero] at him + rw [norm_mul, Complex.norm_I, mul_one, Complex.norm_real, Real.norm_eq_abs] at h + calc |Real.sin y - tayl 1 M y| ≤ _ := him + _ ≤ _ := h + _ = 2 * |y| ^ (2 * M + 1) / ((2 * M + 1).factorial : ℝ) := by ring + +/-- The sector Taylor remainder. -/ +theorem phiF_sub_tayl_le {par M : ℕ} (hpar : par = 0 ∨ par = 1) {y : ℝ} + (hy : |y| ≤ (2 * M + par + 1) / 2) : + |phiF par y - tayl par M y| ≤ 2 * |y| ^ (2 * M + par) / ((2 * M + par).factorial : ℝ) := by + rcases hpar with h | h <;> subst h + · simp only [phiF, if_true, add_zero] at hy ⊢ + push_cast at hy + exact cos_sub_tayl_le (by simpa using hy) + · simp only [phiF, one_ne_zero, if_false] at hy ⊢ + push_cast at hy + exact sin_sub_tayl_le (by linarith) + +lemma real_exp_bound2 {y : ℝ} (hy : |y| ≤ 1) {n : ℕ} (hn : 0 < n) : + |Real.exp y - ∑ m ∈ range n, y ^ m / (m.factorial : ℝ)| ≤ 2 * |y| ^ n / (n.factorial : ℝ) := by + have h := Real.exp_bound hy hn + refine h.trans ?_ + have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn + have hf : (0 : ℝ) < (n.factorial : ℝ) := by exact_mod_cast Nat.factorial_pos n + have hp : 0 ≤ |y| ^ n := by positivity + rw [show (2 : ℝ) * |y| ^ n / (n.factorial : ℝ) = |y| ^ n * (2 / (n.factorial : ℝ)) by ring] + apply mul_le_mul_of_nonneg_left _ hp + push_cast + rw [div_le_div_iff₀ (by positivity) hf] + nlinarith + +/-- The pole Taylor remainder (`|x/2| <= 1`, at least one term). -/ +theorem poleF_sub_ptayl_le {par M : ℕ} (hpar : par = 0 ∨ par = 1) (hM : 0 < 2 * M + par) {x : ℝ} + (hx : |x / 2| ≤ 1) : + |poleF par x - ptayl par M (x / 2)| ≤ 2 * |x / 2| ^ (2 * M + par) / ((2 * M + par).factorial : ℝ) := by + have hx' : |-(x / 2)| ≤ 1 := by rwa [abs_neg] + have h1 := real_exp_bound2 hx hM + have h2 := real_exp_bound2 hx' hM + rw [abs_neg] at h2 + rcases hpar with h | h <;> subst h + · simp only [add_zero] at h1 h2 hM ⊢ + have hs := exp_sum_add_neg_even (x / 2) M + simp only [poleF, if_true] + rw [Real.cosh_eq] + have e : (Real.exp (x / 2) + Real.exp (-(x / 2))) / 2 - ptayl 0 M (x / 2) + = ((Real.exp (x / 2) - ∑ m ∈ range (2 * M), (x / 2) ^ m / (m.factorial : ℝ)) + + (Real.exp (-(x / 2)) - ∑ m ∈ range (2 * M), (-(x / 2)) ^ m / (m.factorial : ℝ))) / 2 := by + linarith + rw [e, abs_div, abs_two] + have := abs_add_le (Real.exp (x / 2) - ∑ m ∈ range (2 * M), (x / 2) ^ m / (m.factorial : ℝ)) + (Real.exp (-(x / 2)) - ∑ m ∈ range (2 * M), (-(x / 2)) ^ m / (m.factorial : ℝ)) + rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)] + linarith + · have hs := exp_sum_sub_neg_odd (x / 2) M + simp only [poleF, one_ne_zero, if_false] + rw [Real.sinh_eq] + have e : (Real.exp (x / 2) - Real.exp (-(x / 2))) / 2 - ptayl 1 M (x / 2) + = ((Real.exp (x / 2) - ∑ m ∈ range (2 * M + 1), (x / 2) ^ m / (m.factorial : ℝ)) + - (Real.exp (-(x / 2)) - ∑ m ∈ range (2 * M + 1), (-(x / 2)) ^ m / (m.factorial : ℝ))) / 2 := by + linarith + rw [e, abs_div, abs_two] + have := abs_sub (Real.exp (x / 2) - ∑ m ∈ range (2 * M + 1), (x / 2) ^ m / (m.factorial : ℝ)) + (Real.exp (-(x / 2)) - ∑ m ∈ range (2 * M + 1), (-(x / 2)) ^ m / (m.factorial : ℝ)) + rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)] + linarith + +/-! ## D. Integral calculus on [-l, l]. -/ + +lemma intervalIntegrable_of_cont {f : ℝ → ℝ} (hf : Continuous f) (a b : ℝ) : + IntervalIntegrable f volume a b := hf.intervalIntegrable a b + +/-- `|int f g| <= B int |f|` when `|g| <= B` on `[-l, l]`. -/ +lemma abs_int_mul_le {l : ℝ} (hl : 0 ≤ l) {f g : ℝ → ℝ} (hf : Continuous f) (hg : Continuous g) + {B : ℝ} (hB : ∀ x ∈ Set.Icc (-l) l, |g x| ≤ B) : + |∫ x in (-l)..l, f x * g x| ≤ B * A1 l f := by + have hab : -l ≤ l := by linarith + refine (intervalIntegral.abs_integral_le_integral_abs hab).trans ?_ + have hmono : ∫ x in (-l)..l, |f x * g x| ≤ ∫ x in (-l)..l, |f x| * B := by + apply intervalIntegral.integral_mono_on hab + · exact (hf.mul hg).abs.intervalIntegrable _ _ + · exact (hf.abs.mul continuous_const).intervalIntegrable _ _ + · intro x hx + rw [abs_mul] + exact mul_le_mul_of_nonneg_left (hB x hx) (abs_nonneg _) + refine hmono.trans (le_of_eq ?_) + rw [intervalIntegral.integral_mul_const] + unfold A1 + ring + +lemma A1_nonneg {l : ℝ} (hl : 0 ≤ l) (f : ℝ → ℝ) : 0 ≤ A1 l f := + intervalIntegral.integral_nonneg (by linarith) fun x _ => abs_nonneg _ + +/-- Cauchy-Schwarz on `[-l, l]`: `(int |f|)^2 <= 2 l int f^2`. -/ +theorem A1_sq_le {l : ℝ} (hl : 0 < l) {f : ℝ → ℝ} (hf : Continuous f) : + A1 l f ^ 2 ≤ 2 * l * ∫ x in (-l)..l, f x ^ 2 := by + set m := A1 l f / (2 * l) with hm + have hab : -l ≤ l := by linarith + have h0 : 0 ≤ ∫ x in (-l)..l, (|f x| - m) ^ 2 := + intervalIntegral.integral_nonneg hab fun x _ => sq_nonneg _ + have e : (fun x => (|f x| - m) ^ 2) = fun x => f x ^ 2 - (2 * m) * |f x| + m ^ 2 := by + funext x; rw [sub_sq, sq_abs]; ring + have hI1 : IntervalIntegrable (fun x => f x ^ 2) volume (-l) l := (hf.pow 2).intervalIntegrable _ _ + have hI2 : IntervalIntegrable (fun x => (2 * m) * |f x|) volume (-l) l := + (continuous_const.mul hf.abs).intervalIntegrable _ _ + rw [e, intervalIntegral.integral_add (hI1.sub hI2) intervalIntegrable_const, + intervalIntegral.integral_sub hI1 hI2, intervalIntegral.integral_const_mul, + intervalIntegral.integral_const] at h0 + simp only [smul_eq_mul, sub_neg_eq_add] at h0 + have hA : A1 l f = ∫ x in (-l)..l, |f x| := rfl + rw [← hA] at h0 + have hl2 : (l + l) = 2 * l := by ring + rw [hl2] at h0 + have hmm : 2 * m * A1 l f - m ^ 2 * (2 * l) = A1 l f ^ 2 / (2 * l) := by + rw [hm]; field_simp; ring + have : A1 l f ^ 2 / (2 * l) ≤ ∫ x in (-l)..l, f x ^ 2 := by linarith + rwa [div_le_iff₀ (by positivity), mul_comm] at this + +/-! ## E. The transforms: truncation, crude bounds, continuity. -/ + +lemma pow_mul_div_pow {l : ℝ} (hl : l ≠ 0) (t x : ℝ) (n : ℕ) : + (t * x) ^ n = (t * l) ^ n * (x / l) ^ n := by + rw [← mul_pow]; congr 1; field_simp + +/-- The truncated transform, as an integral. -/ +lemma int_mul_tayl {l : ℝ} (hl : 0 < l) {f : ℝ → ℝ} (hf : Continuous f) (par M : ℕ) (t : ℝ) : + ∫ x in (-l)..l, f x * tayl par M (t * x) + = ∑ m ∈ range M, (-1) ^ m * (t * l) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo l f (2 * m + par) := by + unfold tayl mo + simp_rw [Finset.mul_sum] + rw [intervalIntegral.integral_finsetSum] + · refine Finset.sum_congr rfl fun m _ => ?_ + rw [← intervalIntegral.integral_const_mul] + congr 1 + funext x + rw [pow_mul_div_pow hl.ne'] + ring + · intro m _ + exact (hf.mul (by fun_prop)).intervalIntegrable _ _ + +lemma int_mul_ptayl {l : ℝ} (hl : 0 < l) {f : ℝ → ℝ} (hf : Continuous f) (par M : ℕ) : + ∫ x in (-l)..l, f x * ptayl par M (x / 2) + = ∑ m ∈ range M, (l / 2) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) * mo l f (2 * m + par) := by + unfold ptayl mo + simp_rw [Finset.mul_sum] + rw [intervalIntegral.integral_finsetSum] + · refine Finset.sum_congr rfl fun m _ => ?_ + rw [← intervalIntegral.integral_const_mul] + congr 1 + funext x + have : (x / 2) ^ (2 * m + par) = (l / 2) ^ (2 * m + par) * (x / l) ^ (2 * m + par) := by + rw [← mul_pow]; congr 1; field_simp + rw [this] + ring + · intro m _ + exact (hf.mul (by fun_prop)).intervalIntegrable _ _ + +/-- **Transform truncation.** For `0 <= t`, `t l <= (2M+par+1)/2`. -/ +theorem Tr_sub_le {l : ℝ} (hl : 0 < l) {par M : ℕ} (hpar : par = 0 ∨ par = 1) {f : ℝ → ℝ} + (hf : Continuous f) {t : ℝ} (ht : 0 ≤ t) (htl : t * l ≤ (2 * M + par + 1) / 2) : + |Tr l par f t - ∑ m ∈ range M, (-1) ^ m * (t * l) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo l f (2 * m + par)| + ≤ 2 * (t * l) ^ (2 * M + par) / ((2 * M + par).factorial : ℝ) * A1 l f := by + have hI1 : IntervalIntegrable (fun x => f x * phiF par (t * x)) volume (-l) l := + (hf.mul ((continuous_phiF par).comp (continuous_const.mul continuous_id))).intervalIntegrable _ _ + have hI2 : IntervalIntegrable (fun x => f x * tayl par M (t * x)) volume (-l) l := + (hf.mul ((continuous_tayl par M).comp (continuous_const.mul continuous_id))).intervalIntegrable _ _ + rw [← int_mul_tayl hl hf, Tr, ← intervalIntegral.integral_sub hI1 hI2] + have e : (fun x => f x * phiF par (t * x) - f x * tayl par M (t * x)) + = fun x => f x * (phiF par (t * x) - tayl par M (t * x)) := by funext x; ring + rw [e] + apply abs_int_mul_le hl.le hf + · exact ((continuous_phiF par).comp (continuous_const.mul continuous_id)).sub + ((continuous_tayl par M).comp (continuous_const.mul continuous_id)) + · intro x hx + have hxl : |x| ≤ l := abs_le.mpr ⟨hx.1, hx.2⟩ + have htx : |t * x| ≤ t * l := by + rw [abs_mul, abs_of_nonneg ht]; exact mul_le_mul_of_nonneg_left hxl ht + refine (phiF_sub_tayl_le hpar (htx.trans htl)).trans ?_ + have hfac : (0 : ℝ) < ((2 * M + par).factorial : ℝ) := by exact_mod_cast Nat.factorial_pos _ + rw [div_le_div_iff_of_pos_right hfac] + exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (abs_nonneg _) htx _) (by norm_num) + +/-- **Pole truncation.** For `l/2 <= 1`. -/ +theorem Pl_sub_le {l : ℝ} (hl : 0 < l) (hl2 : l / 2 ≤ 1) {par M : ℕ} (hpar : par = 0 ∨ par = 1) + (hM : 0 < 2 * M + par) {f : ℝ → ℝ} (hf : Continuous f) : + |Pl l par f - ∑ m ∈ range M, (l / 2) ^ (2 * m + par) / ((2 * m + par).factorial : ℝ) + * mo l f (2 * m + par)| + ≤ 2 * (l / 2) ^ (2 * M + par) / ((2 * M + par).factorial : ℝ) * A1 l f := by + have hI1 : IntervalIntegrable (fun x => f x * poleF par x) volume (-l) l := + (hf.mul (continuous_poleF par)).intervalIntegrable _ _ + have hI2 : IntervalIntegrable (fun x => f x * ptayl par M (x / 2)) volume (-l) l := + (hf.mul ((continuous_ptayl par M).comp (continuous_id.div_const 2))).intervalIntegrable _ _ + rw [← int_mul_ptayl hl hf, Pl, ← intervalIntegral.integral_sub hI1 hI2] + have e : (fun x => f x * poleF par x - f x * ptayl par M (x / 2)) + = fun x => f x * (poleF par x - ptayl par M (x / 2)) := by funext x; ring + rw [e] + apply abs_int_mul_le hl.le hf + · exact (continuous_poleF par).sub ((continuous_ptayl par M).comp (continuous_id.div_const 2)) + · intro x hx + have hxl : |x / 2| ≤ l / 2 := by + rw [abs_div, abs_two] + exact div_le_div_of_nonneg_right (abs_le.mpr ⟨hx.1, hx.2⟩) (by norm_num) + refine (poleF_sub_ptayl_le hpar hM (hxl.trans hl2)).trans ?_ + have hfac : (0 : ℝ) < ((2 * M + par).factorial : ℝ) := by exact_mod_cast Nat.factorial_pos _ + rw [div_le_div_iff_of_pos_right hfac] + exact mul_le_mul_of_nonneg_left (pow_le_pow_left₀ (abs_nonneg _) hxl _) (by norm_num) + +theorem abs_Tr_le {l : ℝ} (hl : 0 < l) (par : ℕ) {f : ℝ → ℝ} (hf : Continuous f) (t : ℝ) : + |Tr l par f t| ≤ A1 l f := by + have := abs_int_mul_le hl.le hf ((continuous_phiF par).comp (continuous_const.mul continuous_id)) + (B := 1) fun x _ => abs_phiF_le par (t * x) + simpa [Tr] using this + +theorem abs_Pl_le {l : ℝ} (hl : 0 < l) (par : ℕ) {f : ℝ → ℝ} (hf : Continuous f) : + |Pl l par f| ≤ Real.cosh (l / 2) * A1 l f := by + apply abs_int_mul_le hl.le hf (continuous_poleF par) + intro x hx + have hc : Real.cosh (x / 2) ≤ Real.cosh (l / 2) := by + rw [Real.cosh_le_cosh, abs_of_nonneg (by linarith : 0 ≤ l / 2), abs_div, abs_two] + exact div_le_div_of_nonneg_right (abs_le.mpr ⟨hx.1, hx.2⟩) (by norm_num) + by_cases h : par = 0 + · simp only [poleF, h, if_true] + rw [abs_of_pos (Real.cosh_pos _)] + exact hc + · simp only [poleF, h, if_false] + refine le_trans ?_ hc + rw [abs_le] + constructor + · have := Real.sinh_lt_cosh (-(x / 2)) + rw [Real.sinh_neg, Real.cosh_neg] at this + linarith + · exact (Real.sinh_lt_cosh _).le + +theorem continuous_Tr (l : ℝ) (par : ℕ) {f : ℝ → ℝ} (hf : Continuous f) : Continuous (Tr l par f) := by + unfold Tr + have hc : Continuous (fun p : ℝ × ℝ => f p.2 * phiF par (p.1 * p.2)) := + (hf.comp continuous_snd).mul ((continuous_phiF par).comp (continuous_fst.mul continuous_snd)) + exact intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' hc (-l) l + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/KWin_Window.lean b/telperion/examples/rvm_bridge/lean/KWin_Window.lean new file mode 100644 index 000000000..9b525e15e --- /dev/null +++ b/telperion/examples/rvm_bridge/lean/KWin_Window.lean @@ -0,0 +1,178 @@ +/- + KWin_Window -- THE PRIME-FREE WINDOW at 2L = log 2, on the goal node's full test class, with no + Arb seam (rvm_bridge island, 2026-09-24). + + conjecture1_proved = False. A finite-window Weil positivity statement is NOT RH. PR #604 + recorded that the 1.3e-3 full-class margin at this window is zero content: on the window the + Weil form IS the zero sum (explicit formula), and over the first 200 zero pairs that sum is + 0.001301 against a least eigenvalue of 0.001329, so certifying the margin says nothing new about + the zeros. Nor is this Connes-Consani (arXiv 2006.13771, Theorem 1) or Yoshida (1992): their + theorem is for the POLE-FREE class paperFT g (i/2) = 0 (margin 0.547 here); the statement below + keeps the pole terms, i.e. it is the goal node's full class. + + PROVED HERE, hypothesis-free (every numeric fact kernel-checked; the guard prints only Lean's + three standard foundations propext / Classical.choice / Quot.sound): + * evenSectorFloor / oddSectorFloor: Zhu's sector floors EvenSectorFloor / OddSectorFloor at + L0 = log 2 / 2 with lam = 9/10000; + * windowFloor_L0: WeilWindow.WindowFloor (log 2 / 2) (9/10000), via Zhu Lemma 6.1 + (`windowFloor_of_sectors`, ZhuParity); + * kwin_primeFreeWindow: the LITERAL body of RvMBridge31.PrimeFreeWindowPositivity + (E6Bridge31, origin/main): for all g L, IsWeilTest g -> tsupport g ⊆ Icc (-L) L -> + 2 L <= log 2 -> 0 <= Re weilForm (autocorr g); + * kwin_primeFreeWindowArch: the literal body of RvMBridge31.PrimeFreeWindowArchPositivity + (Stage 0 re-proved below: the prime side of the autocorrelation vanishes on the window). + After origin/main (E6Bridge31) is merged into this branch the bridge is one line: + theorem primeFreeWindowPositivity : RvMBridge31.PrimeFreeWindowPositivity := + KWin.kwin_primeFreeWindow + (the bodies are syntactically identical; E6Bridge31 opens WeilExplicit). + + THE ROUTE (Q = Re weilForm (autocorr v), real v of parity eps, supported in [-L0, L0]): + Q >= Rb v v KWin_Split (Zhu eq. (2) + split at T = 20, beta0 = 1.107) + Rb v v >= (9/10000) int v^2 KWin_Tail (projection tail, N = 12 even / 10 odd modes) + <- Rb h h >= lam int h^2 KWin_Head (pi-scaled head matrix; minorant; moments) + <- psdCert (headMat ...) = true KWin_Cert (decide +kernel: exact LDL^T, re-verified) + <- w_i <= Psi on 7 pieces KWin_Minorant (digamma series, geometric Lorentzian bounds) + No `sorry`. +-/ +import KWin_Split +import KWin_Tail + +open Real MeasureTheory Set + +noncomputable section + +namespace KWin +open WeilExplicit RvMBridgeZhu + +/-! ## A. The two sector floors at L0 = log 2 / 2. -/ + +lemma lamFloor_cast : ((lamFloor : ℚ) : ℝ) = 9 / 10000 := by unfold lamFloor; push_cast; norm_num + +/-- A real sector test: the common core of both sector floors. -/ +theorem sector_floor_core {par N : ℕ} (hpar : par = 0 ∨ par = 1) {lam : ℚ} + (htail : tailCond par N lam = true) (hcert : psdCert (headMat par N lam) N = true) + (hginv : ginvCheck par N = true) {f : ℝ → ℂ} (hf : IsWeilTest f) (hre : ∀ x, (f x).im = 0) + (hpf : ∀ x, f (-x) = (epsR par : ℂ) * f x) (hs : tsupport f ⊆ Icc (-L0) L0) : + (9 / 10000 : ℝ) * (∫ x : ℝ, ‖f x‖ ^ 2) ≤ (WeilForm.weilForm (WeilForm.autocorr f)).re := by + set v : ℝ → ℝ := fun u => (f u).re with hvdef + have hfv : f = fun u => (v u : ℂ) := by + funext u; exact Complex.ext (by simp [hvdef]) (by simp [hvdef, hre u]) + rw [hfv] at hf hs ⊢ + have hev : ∀ u, v (-u) = epsR par * v u := by + intro u + have h := congrArg Complex.re (hpf u) + rw [hfv] at h + simpa [epsR] using h + have hQ := Q_ge_Rb hpar hf hev hs + have hR := Rb_floor hpar htail hcert hginv (continuous_v hf) + have hip : ip ellR v v = ∫ x : ℝ, ‖(v x : ℂ)‖ ^ 2 := by + unfold ip + rw [← integral_eq_interval hs] + congr 1; funext x + rw [Complex.norm_real, Real.norm_eq_abs, sq_abs]; ring + rw [lamFloor_cast, hip] at hR + linarith + +theorem evenSectorFloor : WeilWindow.EvenSectorFloor L0 (9 / 10000) := by + intro f hf hre hev hs + exact sector_floor_core (par := 0) (N := 12) (Or.inl rfl) tail_even cert_even ginv_even hf hre + (fun x => by rw [hev x]; simp [epsR]) hs + +theorem oddSectorFloor : WeilWindow.OddSectorFloor L0 (9 / 10000) := by + intro f hf hre hodd hs + exact sector_floor_core (par := 1) (N := 10) (Or.inr rfl) tail_odd cert_odd ginv_odd hf hre + (fun x => by rw [hodd x]; simp [epsR]) hs + +/-! ## B. The window floor and the prime-free window. -/ + +/-- **Zhu's window floor at the edge of the prime-free window**: every smooth compactly supported +test `f` (complex, no parity) supported in `[-log 2 / 2, log 2 / 2]` has +`Re weilForm (autocorr f) >= (9/10000) ||f||_2^2`. -/ +theorem windowFloor_L0 : WeilWindow.WindowFloor L0 (9 / 10000) := + windowFloor_of_sectors evenSectorFloor oddSectorFloor + +/-- The literal body of `RvMBridge31.PrimeFreeWindowPositivity` (E6Bridge31). -/ +def PrimeFreeWindowPositivityBody : Prop := + ∀ (g : ℝ → ℂ) (L : ℝ), IsWeilTest g → tsupport g ⊆ Set.Icc (-L) L → 2 * L ≤ Real.log 2 → + 0 ≤ (weilForm (autocorr g)).re + +/-- The literal body of `RvMBridge31.PrimeFreeWindowArchPositivity` (E6Bridge31). -/ +def PrimeFreeWindowArchPositivityBody : Prop := + ∀ (g : ℝ → ℂ) (L : ℝ), IsWeilTest g → tsupport g ⊆ Set.Icc (-L) L → 2 * L ≤ Real.log 2 → + 0 ≤ (archSide (autocorr g)).re + +/-- **THE PRIME-FREE WINDOW, PROVED** (hypothesis-free, no Arb seam): Weil positivity on the goal +node's full test class for every support window with `2 L <= log 2`. -/ +theorem kwin_primeFreeWindow : PrimeFreeWindowPositivityBody := by + intro g L hg hs hL + have hLL : L ≤ L0 := by unfold L0; linarith + have hs' : tsupport g ⊆ Icc (-L0) L0 := hs.trans (Icc_subset_Icc (by linarith) hLL) + have h := windowFloor_L0 g hg hs' + have hm : 0 ≤ ∫ x : ℝ, ‖g x‖ ^ 2 := integral_nonneg fun x => by positivity + have h2 : (0 : ℝ) ≤ (9 / 10000) * ∫ x : ℝ, ‖g x‖ ^ 2 := by positivity + rw [weilForm_autocorr_eq] at h + linarith + +/-! ## C. Stage 0 (re-proved from E6Bridge31): the prime side vanishes on the window. -/ + +lemma eq_zero_of_tsupport_subset_Icc_right' {f : ℝ → ℂ} {a b : ℝ} (hf : Continuous f) + (hs : tsupport f ⊆ Set.Icc a b) {x : ℝ} (hx : b ≤ x) : f x = 0 := by + by_contra h + obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff.mp (hf.continuousAt.eventually_ne h) + have hne : f (x + ε / 2) ≠ 0 := hball (by rw [Real.dist_eq]; rw [abs_lt]; constructor <;> linarith) + have hmem : x + ε / 2 ∈ tsupport f := subset_tsupport f (Function.mem_support.mpr hne) + have := (hs hmem).2 + linarith + +lemma eq_zero_of_tsupport_subset_Icc_left' {f : ℝ → ℂ} {a b : ℝ} (hf : Continuous f) + (hs : tsupport f ⊆ Set.Icc a b) {x : ℝ} (hx : x ≤ a) : f x = 0 := by + by_contra h + obtain ⟨ε, hε, hball⟩ := Metric.eventually_nhds_iff.mp (hf.continuousAt.eventually_ne h) + have hne : f (x - ε / 2) ≠ 0 := hball (by rw [Real.dist_eq]; rw [abs_lt]; constructor <;> linarith) + have hmem : x - ε / 2 ∈ tsupport f := subset_tsupport f (Function.mem_support.mpr hne) + have := (hs hmem).1 + linarith + +lemma tsupport_autocorr_subset' {g : ℝ → ℂ} {L : ℝ} (hg : tsupport g ⊆ Set.Icc (-L) L) : + tsupport (autocorr g) ⊆ Set.Icc (-(2 * L)) (2 * L) := by + rw [RvMBridge5.autocorr_eq_weilTest] + have h : tsupport g ⊆ Set.Icc (-((2 * L) / 2)) ((2 * L) / 2) := by + rwa [show (2 * L) / 2 = L by ring] + exact Zeta23.EF.tsupport_weilTest_subset h h + +theorem primeSide_autocorr_eq_zero' {g : ℝ → ℂ} (hg : IsWeilTest g) {L : ℝ} + (hsupp : tsupport g ⊆ Set.Icc (-L) L) (hL : 2 * L ≤ Real.log 2) : + primeSide (autocorr g) = 0 := by + have hf : Continuous (autocorr g) := (RvMBridge5.isWeilTest_autocorr hg).1.continuous + have hts := tsupport_autocorr_subset' hsupp + unfold primeSide + have hz : (fun n : ℕ => ((ArithmeticFunction.vonMangoldt n / Real.sqrt n : ℝ) : ℂ) + * (autocorr g (Real.log n) + autocorr g (-Real.log n))) = fun _ => 0 := by + funext n + rcases Nat.lt_or_ge n 2 with hn | hn + · interval_cases n + · simp + · simp [ArithmeticFunction.vonMangoldt_apply_one] + · have hlog : Real.log 2 ≤ Real.log n := + Real.log_le_log (by norm_num) (by exact_mod_cast hn) + have h1 : autocorr g (Real.log n) = 0 := + eq_zero_of_tsupport_subset_Icc_right' hf hts (by linarith) + have h2 : autocorr g (-Real.log n) = 0 := + eq_zero_of_tsupport_subset_Icc_left' hf hts (by linarith) + rw [h1, h2] + simp + rw [hz, tsum_zero] + +/-- The archimedean form of the prime-free window (the literal body of +`RvMBridge31.PrimeFreeWindowArchPositivity`). -/ +theorem kwin_primeFreeWindowArch : PrimeFreeWindowArchPositivityBody := by + intro g L hg hs hL + have h := kwin_primeFreeWindow g L hg hs hL + have e : weilForm (autocorr g) = archSide (autocorr g) := by + unfold weilForm + rw [primeSide_autocorr_eq_zero' hg hs hL, sub_zero] + rwa [e] at h + +end KWin + +end diff --git a/telperion/examples/rvm_bridge/lean/lakefile.toml b/telperion/examples/rvm_bridge/lean/lakefile.toml index ccdba848d..83a5c547f 100644 --- a/telperion/examples/rvm_bridge/lean/lakefile.toml +++ b/telperion/examples/rvm_bridge/lean/lakefile.toml @@ -6,7 +6,7 @@ name = "RvMBridge" # v4.32.0 islands (mirrormere, main) nor the v4.34.0-rc1 islands (missions/rh, li_positivity). # AxiomGuardRvMBridge is in defaultTargets so bare `lake build` compiles the guard and every # module it imports before CI runs `lake env lean AxiomGuardRvMBridge.lean` (cf. #448/#451). -defaultTargets = ["E6Bridge", "E6Bridge2", "E6Bridge3", "E6Bridge4", "E6Bridge5", "RvMBridgeGauss", "E6Bridge6", "E6Bridge7", "E6Bridge8", "E6Bridge9", "E6Bridge10", "E6Bridge11", "E6Bridge12", "E6Bridge13", "E6Bridge14", "E6Bridge15", "E6Bridge16", "E6Bridge18", "RvMBridgeXi", "E6Bridge17", "E6Bridge20", "E6Bridge21", "E6Bridge22", "E6Bridge19", "E6Bridge23", "E6Bridge25", "E6Bridge26", "E6Bridge24", "E6Bridge27", "E6Bridge28", "E6Bridge29", "E6Bridge30", "ZhuEnvelope", "ZhuSymbol", "ZhuLegendre", "ZhuParity", "ZhuSplit", "ZhuOrtho", "ZhuTail", "ZhuInstance", "W2cAssembly", "DogfoodComplexReImSplit", "DogfoodZeroSumMajorant", "AxiomGuardRvMBridge"] +defaultTargets = ["E6Bridge", "E6Bridge2", "E6Bridge3", "E6Bridge4", "E6Bridge5", "RvMBridgeGauss", "E6Bridge6", "E6Bridge7", "E6Bridge8", "E6Bridge9", "E6Bridge10", "E6Bridge11", "E6Bridge12", "E6Bridge13", "E6Bridge14", "E6Bridge15", "E6Bridge16", "E6Bridge18", "RvMBridgeXi", "E6Bridge17", "E6Bridge20", "E6Bridge21", "E6Bridge22", "E6Bridge19", "E6Bridge23", "E6Bridge25", "E6Bridge26", "E6Bridge24", "E6Bridge27", "E6Bridge28", "E6Bridge29", "E6Bridge30", "ZhuEnvelope", "ZhuSymbol", "ZhuLegendre", "ZhuParity", "ZhuSplit", "ZhuOrtho", "ZhuTail", "ZhuInstance", "W2cAssembly", "DogfoodComplexReImSplit", "DogfoodZeroSumMajorant", "KWin_Data", "KWin_Cert", "KWin_Constants", "KWin_Taylor", "KWin_Minorant", "KWin_Head", "KWin_Tail", "KWin_Split", "KWin_Window", "AxiomGuardRvMBridge"] # anthropics/zeta-23-lean redirects to anthropics/formal-math; the Lean project is the # `zeta23/` subdirectory (package name `Zeta23`). Pinned to the exact commit that the E6 probe @@ -377,6 +377,37 @@ roots = ["Probes.Dogfood_complex_re_im_split"] name = "DogfoodZeroSumMajorant" roots = ["Probes.Dogfood_zero_sum_majorant"] +# KWin (2026-09-24): the prime-free window at 2L = log 2 on the goal node's full class, certified +# with NO Arb seam: exact-rational symbol minorant + head certificate evaluated by the kernel +# (decide +kernel), projection tail, Zhu split. 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. +[[lean_lib]] +name = "KWin_Data" + +[[lean_lib]] +name = "KWin_Cert" + +[[lean_lib]] +name = "KWin_Constants" + +[[lean_lib]] +name = "KWin_Taylor" + +[[lean_lib]] +name = "KWin_Minorant" + +[[lean_lib]] +name = "KWin_Head" + +[[lean_lib]] +name = "KWin_Tail" + +[[lean_lib]] +name = "KWin_Split" + +[[lean_lib]] +name = "KWin_Window" + # The CI axiom guard, declared as a lib so `lake build` compiles it (and thus all its imports). [[lean_lib]] name = "AxiomGuardRvMBridge" From 3cd7a08773144ca39a9bfb824a9bb184061f471e Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Thu, 24 Sep 2026 01:27:32 -0400 Subject: [PATCH 2/6] mirrormere: registry fixes from independent review -- [proof] link, name MM.weil_positivity_prime_free_window, window_tenth containment now a kernel corollary (weil_positivity_window_tenth_of_prime_free) Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6 --- .../examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean | 1 + telperion/examples/rvm_bridge/lean/KWin_Bridge.lean | 9 +++++++++ .../nodes/MM_weil_positivity_prime_free_window.toml | 10 ++++++++-- 3 files changed, 18 insertions(+), 2 deletions(-) diff --git a/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean b/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean index 456d523ce..d5c127c8f 100644 --- a/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean +++ b/telperion/examples/rvm_bridge/lean/AxiomGuardRvMBridge.lean @@ -1218,3 +1218,4 @@ import KWin_Bridge #print axioms kwin_primeFreeWindowPositivity #print axioms kwin_primeFreeWindowArchPositivity #print axioms weil_positivity_prime_free_window +#print axioms weil_positivity_window_tenth_of_prime_free diff --git a/telperion/examples/rvm_bridge/lean/KWin_Bridge.lean b/telperion/examples/rvm_bridge/lean/KWin_Bridge.lean index 4052727fc..4610845ce 100644 --- a/telperion/examples/rvm_bridge/lean/KWin_Bridge.lean +++ b/telperion/examples/rvm_bridge/lean/KWin_Bridge.lean @@ -20,3 +20,12 @@ theorem weil_positivity_prime_free_window (g : ℝ → ℂ) (hg : WeilExplicit.I (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 diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml index 8b062024b..ade801e5f 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml @@ -1,8 +1,14 @@ created = "2026-09-24" depends_on = ["MM_zeta_comb_membership_iff_rh"] kind = "lemma" -name = "MM_weil_positivity_prime_free_window" +name = "MM.weil_positivity_prime_free_window" statement_module = "Statements.MM_weil_positivity_prime_free_window" status = "draft" -title = "THE FULL PRIME-FREE WINDOW ON THE GOAL NODE'S OWN TEST CLASS, KERNEL-NATIVE (rvm_bridge island, KWin_*, 2026-09-24): for every Weil test g with tsupport g in [-L, L] and 2L <= log 2, Re weilForm (autocorr g) >= 0 -- hypothesis-free, no Arb seam (exact-rational digamma minorant + exact LDL^T head certificates, WindowFloor(log2/2, 9/10000)). Pole terms KEPT: per PR #604 the 1.3e-3 margin is zero content (first 200 zero pairs), so this is NOT Connes-Consani (pole-free class). Contains MM_weil_positivity_window_tenth. Finite window; conjecture1_proved = False" +title = "THE FULL PRIME-FREE WINDOW ON THE GOAL NODE'S OWN TEST CLASS, KERNEL-NATIVE (rvm_bridge island, KWin_*, 2026-09-24): for every Weil test g with tsupport g in [-L, L] and 2L <= log 2, Re weilForm (autocorr g) >= 0 -- hypothesis-free, no Arb seam (exact-rational digamma minorant + exact LDL^T head certificates, WindowFloor(log2/2, 9/10000)). Pole terms KEPT: per PR #604 the 1.3e-3 margin is zero content (first 200 zero pairs), so this is NOT Connes-Consani (pole-free class). Implies the L <= 1/10 statement of MM_weil_positivity_window_tenth, kernel-checked as weil_positivity_window_tenth_of_prime_free (KWin_Bridge). Finite window; conjecture1_proved = False" updated = "2026-09-24" + +[proof] +artifact = "../../examples/rvm_bridge/lean/KWin_Bridge.lean" +artifact_kind = "lean_module" +closure_clean = false +via = "direct" From b4191a0fc2a71af81fa11df7dfcc2bc94fd5524a Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Thu, 24 Sep 2026 07:56:23 -0400 Subject: [PATCH 3/6] mirrormere: regenerate MM_weil_positivity_prime_free_window statement WITH imports (Mathlib + Statements.MMDefs) via the mission CLI Fixes mission-statements-compile (mirrormere): the earlier file copied the import-less shape of MM_weil_positivity_window_tenth, which is not imported by Statements.lean and so was never compiled. Elaborates locally against MMDefs. Name, [proof] link and title restored. Still DRAFT. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6 --- .../Statements/MM_weil_positivity_prime_free_window.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/telperion/missions/mirrormere/lean/Statements/MM_weil_positivity_prime_free_window.lean b/telperion/missions/mirrormere/lean/Statements/MM_weil_positivity_prime_free_window.lean index 9408e9578..18c388c6e 100644 --- a/telperion/missions/mirrormere/lean/Statements/MM_weil_positivity_prime_free_window.lean +++ b/telperion/missions/mirrormere/lean/Statements/MM_weil_positivity_prime_free_window.lean @@ -1,4 +1,7 @@ --- DO NOT EDIT BY HAND — generated by telperion mission; node MM_weil_positivity_prime_free_window; sha256 cc5250ec86844ac2 +-- DO NOT EDIT BY HAND — generated by telperion mission; node MM_weil_positivity_prime_free_window; sha256 8d7b627527e792e5 +import Mathlib +import Statements.MMDefs + 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 := by sorry From a772f5bcb041cbbe73f336c4b0335fc679a1628b Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Thu, 24 Sep 2026 16:35:27 -0400 Subject: [PATCH 4/6] mirrormere: grant MM.weil_positivity_prime_free_window under #607 provenance (honest labels) + rvm_bridge judge bundle merge main; read-back written in the author's session, recorded independence = "unverified" (display label says self-attested); granted via `mission grant` ([grant] digests, gate 2026-09-23.1; owner ruling 2026-09-24); rvm_bridge judge bundle regenerated (--check OK). conjecture1_proved = False. Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01LMeoWeTz2Q3iSeLfqxfYo6 --- .../missions/judge/rvm_bridge/MANIFEST.json | 11 ++++++++++ ...sitivity_prime_free_window.comparator.json | 13 ++++++++++++ .../judge/rvm_bridge/MissionChallenges.lean | 1 + .../MM_weil_positivity_prime_free_window.lean | 17 ++++++++++++++++ .../MM_weil_positivity_prime_free_window.toml | 20 +++++++++++++++++-- 5 files changed, 60 insertions(+), 2 deletions(-) create mode 100644 telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json create mode 100644 telperion/missions/judge/rvm_bridge/MissionChallenges/MM_weil_positivity_prime_free_window.lean diff --git a/telperion/missions/judge/rvm_bridge/MANIFEST.json b/telperion/missions/judge/rvm_bridge/MANIFEST.json index 8848578f7..d55b93d6b 100644 --- a/telperion/missions/judge/rvm_bridge/MANIFEST.json +++ b/telperion/missions/judge/rvm_bridge/MANIFEST.json @@ -247,6 +247,17 @@ "artifact_sha256": "1b95410ca70ab08f1e2b73ebaea43f97c3becf19b3549f1e496d106e58735294", "statement_sha256": "b7ffdf97336950e8a168abd1ffa647f13e63cd4cd3ea8b4daaea6ca31f206ed3" }, + { + "slug": "MM_weil_positivity_prime_free_window", + "campaign": "mirrormere", + "theorem": "weil_positivity_prime_free_window", + "solution_module": "KWin_Bridge", + "challenge_module": "MissionChallenges.MM_weil_positivity_prime_free_window", + "bridge_theorem": "MissionJudge.MM_weil_positivity_prime_free_window", + "config": "MM_weil_positivity_prime_free_window.comparator.json", + "artifact_sha256": "2c4bc212327c00f147b41373496121cf3d54b9471eff6bb820088bbd54acd74f", + "statement_sha256": "d4ff7d84406ce351f9b9ae81c66a2658ee01b814164581460b452aceb16dabdb" + }, { "slug": "MM_zeta_comb_membership_iff_rh", "campaign": "mirrormere", diff --git a/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json b/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json new file mode 100644 index 000000000..4e52a8457 --- /dev/null +++ b/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "MissionChallenges.MM_weil_positivity_prime_free_window", + "solution_module": "MissionChallenges.MM_weil_positivity_prime_free_window", + "theorem_names": [ + "MissionJudge.MM_weil_positivity_prime_free_window" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": true +} diff --git a/telperion/missions/judge/rvm_bridge/MissionChallenges.lean b/telperion/missions/judge/rvm_bridge/MissionChallenges.lean index 87317aaa9..319d06788 100644 --- a/telperion/missions/judge/rvm_bridge/MissionChallenges.lean +++ b/telperion/missions/judge/rvm_bridge/MissionChallenges.lean @@ -20,6 +20,7 @@ import MissionChallenges.MM_theta_heat_monotone import MissionChallenges.MM_wall_map import MissionChallenges.MM_weil_positivity_implies_rh import MissionChallenges.MM_weil_positivity_implies_rh_of_gaussian +import MissionChallenges.MM_weil_positivity_prime_free_window import MissionChallenges.MM_zeta_comb_membership_iff_rh import MissionChallenges.MM_zeta_ordinates_not_uniformly_discrete import MissionChallenges.RH_bl_closed_form_five_nonneg diff --git a/telperion/missions/judge/rvm_bridge/MissionChallenges/MM_weil_positivity_prime_free_window.lean b/telperion/missions/judge/rvm_bridge/MissionChallenges/MM_weil_positivity_prime_free_window.lean new file mode 100644 index 000000000..c297f2f5d --- /dev/null +++ b/telperion/missions/judge/rvm_bridge/MissionChallenges/MM_weil_positivity_prime_free_window.lean @@ -0,0 +1,17 @@ +/- DO NOT EDIT BY HAND -- generated by telperion.missions.judge. + Comparator CHALLENGE for registry node mirrormere/MM_weil_positivity_prime_free_window. + The TYPE below is the registered statement, missions/mirrormere/lean/Statements/ + MM_weil_positivity_prime_free_window.lean (header sha256 8d7b627527e792e5), binders and conclusion verbatim; the + PROOF is the artifact constant `weil_positivity_prime_free_window` from KWin_Bridge. Both kernels + accept this module only if the artifact proves exactly the registered proposition. + The AxiomGuard imports load the whole island, so a vocabulary constant shadowed by + the artifact is a duplicate declaration here, not a silent substitution. The + `namespace` and the `open` lines inside it are the artifact's own at its + declaration, so every name in the statement resolves exactly as it does there. -/ +import KWin_Bridge +import AxiomGuardRvMBridge + +theorem MissionJudge.MM_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 := + weil_positivity_prime_free_window diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml index ade801e5f..2a07c6180 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml @@ -3,12 +3,28 @@ depends_on = ["MM_zeta_comb_membership_iff_rh"] kind = "lemma" name = "MM.weil_positivity_prime_free_window" statement_module = "Statements.MM_weil_positivity_prime_free_window" -status = "draft" +status = "proved" title = "THE FULL PRIME-FREE WINDOW ON THE GOAL NODE'S OWN TEST CLASS, KERNEL-NATIVE (rvm_bridge island, KWin_*, 2026-09-24): for every Weil test g with tsupport g in [-L, L] and 2L <= log 2, Re weilForm (autocorr g) >= 0 -- hypothesis-free, no Arb seam (exact-rational digamma minorant + exact LDL^T head certificates, WindowFloor(log2/2, 9/10000)). Pole terms KEPT: per PR #604 the 1.3e-3 margin is zero content (first 200 zero pairs), so this is NOT Connes-Consani (pole-free class). Implies the L <= 1/10 statement of MM_weil_positivity_window_tenth, kernel-checked as weil_positivity_window_tenth_of_prime_free (KWin_Bridge). Finite window; conjecture1_proved = False" updated = "2026-09-24" +[grant] +artifact_sha256 = "2c4bc212327c00f147b41373496121cf3d54b9471eff6bb820088bbd54acd74f" +date = "2026-09-24" +gate_version = "2026-09-23.1" +identity = "dr.murphy.is.in@arda-dao.com" +session = "ef083c48-579d-4bec-a689-c30fdccec2a1" +statement_sha256 = "d4ff7d84406ce351f9b9ae81c66a2658ee01b814164581460b452aceb16dabdb" + [proof] artifact = "../../examples/rvm_bridge/lean/KWin_Bridge.lean" artifact_kind = "lean_module" -closure_clean = false +closure_clean = true via = "direct" + +[readback] +auditor = "author session (self-attested; not independent)" +auditor_identity = "dr.murphy.is.in@arda-dao.com" +auditor_session = "ef083c48-579d-4bec-a689-c30fdccec2a1" +date = "2026-09-24" +independence = "unverified" +text = "Formal statement, read in the author's own session (so this read-back is NOT independent; the Comparator judge is the independent check that the artifact proves exactly this type). For every g : R -> C that is C-infinity with compact support (IsWeilTest), and every real L with 2L <= log 2 and tsupport g inside [-L, L], the real part of weilForm(autocorr g) is >= 0. weilForm f = archSide f - primeSide f with archSide = H_f(0) + H_f(1) - f(0) log pi + (1/2pi) int h_f(r) Re psi(1/4 + ir/2) dr (both pole terms kept) and primeSide = sum_n Lambda(n)/sqrt n (f(log n) + f(-log n)); autocorr g u = int g(v) conj g(v-u) dv. Since autocorr g is supported in [-2L, 2L] within [-log 2, log 2] and vanishes at the endpoints (the overlap is a single point), every prime term is zero, so the claim is positivity of the archimedean Weil functional on autocorrelations: the prime-free window. Not vacuous: the class contains nonzero bump functions for every L > 0, and the conclusion is a genuine inequality on them. It does not imply RH: it covers only support width 2L <= log 2; Weil's criterion needs all L. Pole terms are included, so this is not the pole-free Connes-Consani class." From 2d33e58d6b66205f919718064ac50364346b3407 Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Fri, 25 Sep 2026 13:51:37 -0400 Subject: [PATCH 5/6] missions: heavy_certificates on the KWin node (judge runs Lean-kernel-only) `MM_weil_positivity_prime_free_window` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The KWin window certificates need ~16-19 GB per decide, which exhausted the 16 GB runner and killed the whole shard after five nodes (run 36076883673); with the flag, the shard's single heavy node is judged by the Lean kernel alone and the other twelve keep both kernels. Merged main in for the machinery this depends on: #632 (the flag, the swap step for shards containing a heavy node, the dispatch filter, and `comparator-record --lean-kernel-only`) and #625 (`ulimit -s unlimited`). Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (53 challenges) and the node's config row now reads `lean-kernel-only`. `mission verify` is OK on all four campaigns. The record itself follows once the restricted shard dispatch passes, as `comparator-record --lean-kernel-only`, which stores `second_kernel = "none: heavy_certificates"` so provenance-report prints "Lean kernel only" rather than staying silent. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU --- telperion/missions/judge/rvm_bridge/MANIFEST.json | 1 + .../MM_weil_positivity_prime_free_window.comparator.json | 2 +- .../mirrormere/nodes/MM_weil_positivity_prime_free_window.toml | 1 + 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/telperion/missions/judge/rvm_bridge/MANIFEST.json b/telperion/missions/judge/rvm_bridge/MANIFEST.json index 95065a353..6b52563f2 100644 --- a/telperion/missions/judge/rvm_bridge/MANIFEST.json +++ b/telperion/missions/judge/rvm_bridge/MANIFEST.json @@ -277,6 +277,7 @@ "challenge_module": "MissionChallenges.MM_weil_positivity_prime_free_window", "bridge_theorem": "MissionJudge.MM_weil_positivity_prime_free_window", "config": "MM_weil_positivity_prime_free_window.comparator.json", + "nanoda": false, "artifact_sha256": "2c4bc212327c00f147b41373496121cf3d54b9471eff6bb820088bbd54acd74f", "statement_sha256": "d4ff7d84406ce351f9b9ae81c66a2658ee01b814164581460b452aceb16dabdb" }, diff --git a/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json b/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json index 4e52a8457..1cf8ae9fe 100644 --- a/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json +++ b/telperion/missions/judge/rvm_bridge/MM_weil_positivity_prime_free_window.comparator.json @@ -9,5 +9,5 @@ "Quot.sound", "Classical.choice" ], - "enable_nanoda": true + "enable_nanoda": false } diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml index 2a07c6180..18a0342ea 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml @@ -1,5 +1,6 @@ created = "2026-09-24" depends_on = ["MM_zeta_comb_membership_iff_rh"] +heavy_certificates = true kind = "lemma" name = "MM.weil_positivity_prime_free_window" statement_module = "Statements.MM_weil_positivity_prime_free_window" From 0a8f24d20e6030573f4b2040591572a16ff060f5 Mon Sep 17 00:00:00 2001 From: "Dr. Murphy" Date: Fri, 25 Sep 2026 16:18:40 -0400 Subject: [PATCH 6/6] missions: record the Lean-kernel-only Comparator pass on the KWin node `judge rvm_bridge 2/4` of run 36169770951 passed 13/13. The log line for this node is exactly COMPARATOR PASS island=rvm_bridge node=MM_weil_positivity_prime_free_window theorem=weil_positivity_prime_free_window run=36169770951 kernel=lean-kernel-only and the other twelve nodes of the shard passed with `kernel=nanoda`, so the heavy-certificate flag turned the second kernel off for this node only. The swap step ran ("extra swap enabled: /mnt/arda-judge.swap") and the shard finished instead of killing the runner after five nodes as it did on run 36076883673. `comparator-record --lean-kernel-only` stores `second_kernel = "none: heavy_certificates"`, and `provenance-report` now prints MM_weil_positivity_prime_free_window comparator=36169770951 Lean kernel only (heavy_certificates: nanoda not run) so the weaker check is stated, never silent. The recorded artifact sha256 (2c4bc212...) equals the one in `[grant]`, i.e. the judge checked the same artifact the grant pinned. `theorem` is recorded as the bare island theorem name, matching what the PASS line prints and the existing record on RH_dbn_debruijn_real_zeros from the same judge flow, so a verifier can grep the shard log for exactly this string. Note the Comparator config asserts the bridge theorem `MissionJudge.MM_weil_positivity_prime_free_window`, and the anduril records use module-qualified names; that inconsistency is worth normalising separately rather than inventing a third convention here. `mission verify` OK on all four campaigns; `judge --island rvm_bridge --check` matches the registry (53 challenges). No status change, no Lean source change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU --- .../nodes/MM_weil_positivity_prime_free_window.toml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml index 18a0342ea..84241aeff 100644 --- a/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml +++ b/telperion/missions/mirrormere/nodes/MM_weil_positivity_prime_free_window.toml @@ -6,7 +6,15 @@ name = "MM.weil_positivity_prime_free_window" statement_module = "Statements.MM_weil_positivity_prime_free_window" status = "proved" title = "THE FULL PRIME-FREE WINDOW ON THE GOAL NODE'S OWN TEST CLASS, KERNEL-NATIVE (rvm_bridge island, KWin_*, 2026-09-24): for every Weil test g with tsupport g in [-L, L] and 2L <= log 2, Re weilForm (autocorr g) >= 0 -- hypothesis-free, no Arb seam (exact-rational digamma minorant + exact LDL^T head certificates, WindowFloor(log2/2, 9/10000)). Pole terms KEPT: per PR #604 the 1.3e-3 margin is zero content (first 200 zero pairs), so this is NOT Connes-Consani (pole-free class). Implies the L <= 1/10 statement of MM_weil_positivity_window_tenth, kernel-checked as weil_positivity_window_tenth_of_prime_free (KWin_Bridge). Finite window; conjecture1_proved = False" -updated = "2026-09-24" +updated = "2026-09-25" + +[comparator] +artifact_sha256 = "2c4bc212327c00f147b41373496121cf3d54b9471eff6bb820088bbd54acd74f" +date = "2026-09-25" +run_id = "36169770951" +run_url = "https://github.com/DrMurphyIsIn/Arda/actions/runs/36169770951" +second_kernel = "none: heavy_certificates" +theorem = "weil_positivity_prime_free_window" [grant] artifact_sha256 = "2c4bc212327c00f147b41373496121cf3d54b9471eff6bb820088bbd54acd74f"