← Session 9 — Phase 4 synthesis assault + paper draft cleanup
thinking (7234 chars)
Paper sub-stage 3 done. Now the 2.9 paper-work: L1 (unconditional embedding ℋ(A_a) ↪ ℋ(A∞)) and L3/L4 (WH symbol class).
L1: injectivity of v ↦ [v] from C∞_c(−a,a) into ℋ(A∞) without RH. The claim: if [v] = 0 (i.e., Q_W(v,w) = 0 for all w, or ‖[v]‖² = 0 in the indefinite sense...), then v = 0. Careful: in the indefinite case, the completion is a quotient by the isotropic subspace. The embedding question: is C∞_c(−a,a) ∩ isotropic = {0}?
Q_W(v,v) = ⟨A∞ v, v⟩ = ∫∫ v(x) g(x−y) v̄(y) — the Weil form on the whole line restricted to support in (−a,a). The explicit formula gives: Q_W(v) = Σ over zeros + archimedean terms of |v̂|²-type quantities... The Weil form: Q_W(v) = Σ_ρ m_ρ |v̂(i(ρ̄−½))|²?-ish — for v supported in (−a,a), v̂ is entire of exponential type ≤ a (Paley–Wiener). If [v] = 0 in the quotient sense, then... The positivity structure: under RH, Q_W(v,v) = Σ_γ m_γ |v̂(γ)|² ≥ 0, and = 0 ⟺ v̂ vanishes on all γ's — a nonzero PW function CAN vanish on all γ's if a is large enough (PW_a contains functions vanishing on any discrete set of density < a/π·... — Beurling–Malliavin!). So the embedding has a kernel when a is large?! Hmm — under RH: [v]=0 ⟺ v̂|_Γ = 0; PW functions vanishing on Γ exist iff the uniform density of Γ < 2a/2π·... The zeros have density ~ log T — infinite density — a PW function of type a vanishing on all of Γ: Γ has infinite upper density ⟹ only v̂ ≡ 0 possible (a PW function is determined by values on any set of positive... actually an entire function of exponential type vanishing on a set of positive relative density on ℝ is identically zero — yes: Cartwright/Paley–Wiener: zeros of exp-type functions have finite density ≤ type/π). Γ has density log T → ∞ per unit — infinite — so v̂|_Γ = 0 ⟹ v̂ ≡ 0 ⟹ v = 0 ✓. So under RH the embedding is injective — consistent with Suzuki's §7.6 (which used [14]'s isomorphism).
Without RH: Q_W(v,v) = Σ_ρ m_ρ |v̂(i(ρ̄−½))|²·... — the sum over ALL zeros including complex ones: [v] = 0 (isotropic) means Q_W(v,v) = 0 — but that's a sum of |·|² over zeros with COMPLEX shifts — terms |v̂(i(ρ̄−½))|² with ρ̄... the isotropic condition is about the sesquilinear form: v ∈ isotropic ⟺ Q_W(v,w) = 0 ∀w ⟺ Σ_ρ m_ρ v̂(...) conj(ŵ(...)) = 0 ∀w — by density of {ŵ} this should give v̂ vanishing on the full zero multiset (with the complex shifts) — again v̂ ≡ 0 by the same density argument (the zero set including off-line ones still has infinite density). So L1 should be PROVABLE: the key input is that a nonzero exp-type function cannot vanish on a set of infinite uniform density. The subtlety: the isotropic condition gives v̂ vanishing on Γ only if the test functions ŵ are dense/rich enough to separate — the span of ŵ values at the points... Let me formalize: Q_W(v,w) = Σ_ρ m_ρ v̂(ζ_ρ) conj(ŵ(ζ_ρ)) where ζ_ρ = i(ρ̄ − ½)... whatever the exact pairing, if for FIXED v this vanishes for ALL w ∈ C∞_c(ℝ), then since {conj(ŵ(ζ_ρ))} can be chosen arbitrarily (ŵ at finitely many points arbitrary by interpolation — entire functions of exp type can take arbitrary values at finitely many points), we get v̂(ζ_ρ) = 0 for each ρ (test with ŵ peaked at each finite subset). Then v̂ vanishes on {ζ_ρ} = infinite-density set ⟹ v̂ ≡ 0. This works for v ∈ C∞_c(−a,a) — PW type a — vanishing on infinite-density set ⟹ 0. ✓ So L1 is provable with standard pieces. The a-independence: infinite density kills any type.
Wait — actually the subtlety: v isotropic in the completion means [v] = 0, i.e., v is in the kernel of the quotient map: Q_W(v,w) = 0 ∀w ∈ C∞_c(ℝ). Yes that's the condition. And the argument above shows v = 0. But hold on — does Q_W(v,w) = Σ_ρ m_ρ v̂(ζ_ρ)conj(ŵ(ζ_ρ)) hold unconditionally (the Weil explicit formula for the form)? The Weil form has the explicit formula: Q_W(v) = Σ_ρ ... + archimedean + prime terms. The zero-side representation of the FORM (not just under RH): Bombieri's result — Q_W(v) = Σ_ρ m_ρ |v̂(i(ρ̄−1/2))|² holds under... hmm, actually the form's zero-side representation: Q_W(v) = Σ_ρ m_ρ v̂(i(ρ̄−½))·conj... — is this valid without RH? The Weil explicit formula gives Q_W(v) as a sum over primes + archimedean; the zero-side form requires the functional equation/positivity... For the Guinand–Weil explicit formula: Q_W(v) = Σ_ρ m_ρ |M v(ρ)|² exactly when... hmm, Bombieri [Bom00]: the form's negative index counts off-line pairs — implying a representation with ± signs: Q_W(v) = Σ_ρ ±|v̂|² — with signs from... Actually for the embedding argument I only need: Q_W(v,w) = 0 ∀w ⟹ v = 0 on C∞_c(−a,a). Use the PRIME side instead: Q_W(v,w) has the prime-sum representation; the Fourier side: Q_W(v,w) = ∫∫ v(x)g(x−y)w̄(y) — the convolution form. [v]=0 ⟺ g∗v̄... ⟺ the distribution g∗v is... hmm: Q_W(v,w) = ⟨g∗v, w⟩ = 0 ∀w ⟺ g∗v = 0 as a distribution... wait for w ∈ C∞_c(ℝ): ⟨g∗v, w̄⟩ = 0 ∀w ⟺ g∗v ≡ 0 as a distribution. Then FT: ĝ·v̂ = 0 as analytic functionals... ĝ = z⁻²ξ′/ξ: ĝ·v̂ ≡ 0: v̂ entire (PW), ĝ meromorphic with poles at zeros — the product being zero: v̂ must vanish at... where ĝ ≠ 0... ĝ·v̂ ≡ 0 with v̂ entire and ĝ nonzero meromorphic ⟹ v̂ ≡ 0 (identity theorem: ĝ·v̂ is meromorphic, zero as a distribution ⟹ zero function ⟹ v̂ zero wherever ĝ finite nonzero...). This is cleaner! [v] = 0 ⟹ g∗v = 0 ⟹ ĝv̂ = 0 ⟹ v̂ = 0 ⟹ v = 0. The FT step needs the tempered-distribution care (g grows exponentially — g∗v for compactly supported v is fine: g is locally integrable — the convolution is a locally integrable function; its FT in the tempered sense... g is NOT tempered (exponential growth) — but g∗v for compactly v grows like e^{|x|/2} — the FT of such is an analytic functional (Paley–Wiener–Schwartz). The product identity ĝv̂ = 0 holds in that sense (this is D-026's flagged bookkeeping). So L1: injectivity holds, proof via convolution + analytic-functional FT — standard modulo the flagged bookkeeping. GOOD — L1 is essentially writable now. I'll upgrade D-041's L1 status with this argument sketch.
L3/L4 (WH symbol class): ĝ = z⁻²ξ′/ξ meromorphic with poles on ℝ (under RH). Gohberg–Feldman theory applies to symbols in specific classes (e.g., Wiener algebra, piecewise continuous, etc.). A meromorphic symbol with real poles is NOT in those classes directly — the standard trick: the equation's solvability via the factorization of the symbol as a meromorphic function... The finite-interval asymptotics for symbols with real poles — this is genuinely nonstandard (poles on the contour). Krein's 1958/62 work covers rational symbols; ξ′/ξ is not rational but is in the Nevanlinna class... Honestly L3/L4 need library work with the GF book — beyond session scope to do rigorously. I'll document the argument shapes and mark them as "assembly pending (library)".
Actually, let me time-box: write the L1 upgrade into D-041 (edit the lemma table + add the proof sketch), note L3/L4 remain library assembly. Then domain sweep (§4A.5) — the last queued item. Actually the domain sweep is significant work too (list walls, ask which untouched field has machinery shaped like each wall, web-research top candidates). Given the session length, let me do L1 now and then run the domain sweep as a focused sub-stage, then wrap the session with a full report to the user (it's been a marathon).
Paper sub-stages done. Now the 2.9 paper-work: L1 has a clean proof route (convolution kernel + analytic-functional FT), which I'll write into D-041; L3/L4 remain library assembly.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\derivations\\D-041-krein-frame-deficiency-convergence.md",
"old_string": "| L1 | \u210b(A_a) \u21aa \u210b(A\u221e) unconditionally | OPEN (published proof via [14] uses RH); expected true; bounded isotropy suffices |",
"new_string": "| L1 | \u210b(A_a) \u21aa \u210b(A\u221e) unconditionally | PROOF SKETCH COMPLETE (2026-08-19, below) \u2014 modulo the D-026-flagged tempered-FT bookkeeping |\n| L1\u2032 | (argument) [v] = 0 \u27fa g\u2217v = 0 as a distribution (Q_W(v,w) = \u27e8g\u2217v, w\u27e9 \u2200w \u2208 C\u221e_c(\u211d)); then \u011d\u00b7v\u0302 = 0 as analytic functionals (g\u2217v grows \u2264 e^{\\|x\\|/2}, Paley\u2013Wiener\u2013Schwartz); \u011d = z\u207b\u00b2\u03be\u2032/\u03be nonzero meromorphic \u27f9 v\u0302 \u2261 0 (identity theorem) \u27f9 v = 0. No RH input. | write-up = Phase-5 item |"
}
result 2026-08-19 19:55:33Z → 2026-08-26 06:04:11Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"oldString": " have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)",
"newString": " have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)",
"originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1]\n simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n (hT : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n rcases Nat.eq_zero_or_pos n with hn | hn\n \u00b7 subst hn\n simp only [kFun, pow_zero, sub_self, norm_zero]\n positivity\n \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n field_simp [ht2.ne']\n ring\n rw [h1]\n have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n linarith\n have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 hQpos hQle n\n _ = Real.exp 5 := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n field_simp [hn0]\n have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns3]\n have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns2]\n have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n rw [norm_div, hnormA, hnormB,\n \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n push_cast\n ring\n unfold kFun\n rw [hs1]\n calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n rw [norm_pow, hnorm, norm_one]\n _ \u2264 Real.exp (5 / 2) + 1 := by\n have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n Real.sqrt_nonneg _\n have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n pow_nonneg hx0 n\n have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n rw [e]\n exact hQn\n have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n rw [Real.sqrt_sq hx]\n rw [h8]\n calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n have h3re : ((3 : \u2102).re) = 3 := rfl\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hn =>\n rcases eq_or_ne n 1 with rfl | hn1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hn2 : 2 \u2264 n := by omega\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt n :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n rw [show (3 : \u211d) = 2 + 1 by norm_num,\n Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n field_simp [show (n : \u211d) \u2260 0 by positivity]\n have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n calc dirichletC3\n = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n _ \u2264 \u2211' n : \u2115, (1 / 2) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n (hsum2.mul_left (1 / 2))\n _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC3 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum3\n _ = dirichletC3 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hm =>\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt m :=\n Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n rw [h\u039b]\n rcases eq_or_ne m 1 with rfl | hm1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n \u00b7 have hm2 : 2 \u2264 m := by omega\n have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n field_simp [show (m : \u211d) \u2260 0 by positivity]\n ring_nf\n rw [e]\n have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n (hsum2.mul_left _)\n _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hle := norm_one_add_one_div_le hs0\n have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n ring\n have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n rw [hre, hns]\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n (by positivity) hU2).mpr (by linarith [h1])\n have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n rw [\u2190 Real.exp_nat_mul]\n have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n rw [mul_div_assoc, \u2190 div_le_div_iff_of_pos_right h\u03c30]\n exact (div_le_div_iff_of_pos_right hU2).mpr hnU\n calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 362,
"oldLines": 7,
"newStart": 362,
"newLines": 7,
"lines": [
" ring_nf",
" rw [e]",
" have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by",
"- rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]",
"+ rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]",
" apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)",
" exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)",
" (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Paper sub-stage 3 done. Now the 2.9 paper-work: L1 (unconditional embedding ℋ(A_a) ↪ ℋ(A∞)) and L3/L4 (WH symbol class).\n\nL1: injectivity of v ↦ [v] from C∞_c(−a,a) into ℋ(A∞) without RH. The claim: if [v] = 0 (i.e., Q_W(v,w) = 0 for all w, or ‖[v]‖² = 0 in the indefinite sense...), then v = 0. Careful: in the indefinite case, the completion is a quotient by the isotropic subspace. The embedding question: is C∞_c(−a,a) ∩ isotropic = {0}?\n\nQ_W(v,v) = ⟨A∞ v, v⟩ = ∫∫ v(x) g(x−y) v̄(y) — the Weil form on the whole line restricted to support in (−a,a). The explicit formula gives: Q_W(v) = Σ over zeros + archimedean terms of |v̂|²-type quantities... The Weil form: Q_W(v) = Σ_ρ m_ρ |v̂(i(ρ̄−½))|²?-ish — for v supported in (−a,a), v̂ is entire of exponential type ≤ a (Paley–Wiener). If [v] = 0 in the quotient sense, then... The positivity structure: under RH, Q_W(v,v) = Σ_γ m_γ |v̂(γ)|² ≥ 0, and = 0 ⟺ v̂ vanishes on all γ's — a nonzero PW function CAN vanish on all γ's if a is large enough (PW_a contains functions vanishing on any discrete set of density < a/π·... — Beurling–Malliavin!). So the embedding has a kernel when a is large?! Hmm — under RH: [v]=0 ⟺ v̂|_Γ = 0; PW functions vanishing on Γ exist iff the uniform density of Γ < 2a/2π·... The zeros have density ~ log T — infinite density — a PW function of type a vanishing on all of Γ: Γ has infinite upper density ⟹ only v̂ ≡ 0 possible (a PW function is determined by values on any set of positive... actually an entire function of exponential type vanishing on a set of positive relative density on ℝ is identically zero — yes: Cartwright/Paley–Wiener: zeros of exp-type functions have finite density ≤ type/π). Γ has density log T → ∞ per unit — infinite — so v̂|_Γ = 0 ⟹ v̂ ≡ 0 ⟹ v = 0 ✓. So under RH the embedding is injective — consistent with Suzuki's §7.6 (which used [14]'s isomorphism).\n\nWithout RH: Q_W(v,v) = Σ_ρ m_ρ |v̂(i(ρ̄−½))|²·... — the sum over ALL zeros including complex ones: [v] = 0 (isotropic) means Q_W(v,v) = 0 — but that's a sum of |·|² over zeros with COMPLEX shifts — terms |v̂(i(ρ̄−½))|² with ρ̄... the isotropic condition is about the sesquilinear form: v ∈ isotropic ⟺ Q_W(v,w) = 0 ∀w ⟺ Σ_ρ m_ρ v̂(...) conj(ŵ(...)) = 0 ∀w — by density of {ŵ} this should give v̂ vanishing on the full zero multiset (with the complex shifts) — again v̂ ≡ 0 by the same density argument (the zero set including off-line ones still has infinite density). So L1 should be PROVABLE: the key input is that a nonzero exp-type function cannot vanish on a set of infinite uniform density. The subtlety: the isotropic condition gives v̂ vanishing on Γ only if the test functions ŵ are dense/rich enough to separate — the span of ŵ values at the points... Let me formalize: Q_W(v,w) = Σ_ρ m_ρ v̂(ζ_ρ) conj(ŵ(ζ_ρ)) where ζ_ρ = i(ρ̄ − ½)... whatever the exact pairing, if for FIXED v this vanishes for ALL w ∈ C∞_c(ℝ), then since {conj(ŵ(ζ_ρ))} can be chosen arbitrarily (ŵ at finitely many points arbitrary by interpolation — entire functions of exp type can take arbitrary values at finitely many points), we get v̂(ζ_ρ) = 0 for each ρ (test with ŵ peaked at each finite subset). Then v̂ vanishes on {ζ_ρ} = infinite-density set ⟹ v̂ ≡ 0. This works for v ∈ C∞_c(−a,a) — PW type a — vanishing on infinite-density set ⟹ 0. ✓ So L1 is provable with standard pieces. The a-independence: infinite density kills any type. \n\nWait — actually the subtlety: v isotropic in the completion means [v] = 0, i.e., v is in the kernel of the quotient map: Q_W(v,w) = 0 ∀w ∈ C∞_c(ℝ). Yes that's the condition. And the argument above shows v = 0. But hold on — does Q_W(v,w) = Σ_ρ m_ρ v̂(ζ_ρ)conj(ŵ(ζ_ρ)) hold unconditionally (the Weil explicit formula for the form)? The Weil form has the explicit formula: Q_W(v) = Σ_ρ ... + archimedean + prime terms. The zero-side representation of the FORM (not just under RH): Bombieri's result — Q_W(v) = Σ_ρ m_ρ |v̂(i(ρ̄−1/2))|² holds under... hmm, actually the form's zero-side representation: Q_W(v) = Σ_ρ m_ρ v̂(i(ρ̄−½))·conj... — is this valid without RH? The Weil explicit formula gives Q_W(v) as a sum over primes + archimedean; the zero-side form requires the functional equation/positivity... For the Guinand–Weil explicit formula: Q_W(v) = Σ_ρ m_ρ |M v(ρ)|² exactly when... hmm, Bombieri [Bom00]: the form's negative index counts off-line pairs — implying a representation with ± signs: Q_W(v) = Σ_ρ ±|v̂|² — with signs from... Actually for the embedding argument I only need: Q_W(v,w) = 0 ∀w ⟹ v = 0 on C∞_c(−a,a). Use the PRIME side instead: Q_W(v,w) has the prime-sum representation; the Fourier side: Q_W(v,w) = ∫∫ v(x)g(x−y)w̄(y) — the convolution form. [v]=0 ⟺ g∗v̄... ⟺ the distribution g∗v is... hmm: Q_W(v,w) = ⟨g∗v, w⟩ = 0 ∀w ⟺ g∗v = 0 as a distribution... wait for w ∈ C∞_c(ℝ): ⟨g∗v, w̄⟩ = 0 ∀w ⟺ g∗v ≡ 0 as a distribution. Then FT: ĝ·v̂ = 0 as analytic functionals... ĝ = z⁻²ξ′/ξ: ĝ·v̂ ≡ 0: v̂ entire (PW), ĝ meromorphic with poles at zeros — the product being zero: v̂ must vanish at... where ĝ ≠ 0... ĝ·v̂ ≡ 0 with v̂ entire and ĝ nonzero meromorphic ⟹ v̂ ≡ 0 (identity theorem: ĝ·v̂ is meromorphic, zero as a distribution ⟹ zero function ⟹ v̂ zero wherever ĝ finite nonzero...). This is cleaner! [v] = 0 ⟹ g∗v = 0 ⟹ ĝv̂ = 0 ⟹ v̂ = 0 ⟹ v = 0. The FT step needs the tempered-distribution care (g grows exponentially — g∗v for compactly supported v is fine: g is locally integrable — the convolution is a locally integrable function; its FT in the tempered sense... g is NOT tempered (exponential growth) — but g∗v for compactly v grows like e^{|x|/2} — the FT of such is an analytic functional (Paley–Wiener–Schwartz). The product identity ĝv̂ = 0 holds in that sense (this is D-026's flagged bookkeeping). So L1: injectivity holds, proof via convolution + analytic-functional FT — standard modulo the flagged bookkeeping. GOOD — L1 is essentially writable now. I'll upgrade D-041's L1 status with this argument sketch.\n\nL3/L4 (WH symbol class): ĝ = z⁻²ξ′/ξ meromorphic with poles on ℝ (under RH). Gohberg–Feldman theory applies to symbols in specific classes (e.g., Wiener algebra, piecewise continuous, etc.). A meromorphic symbol with real poles is NOT in those classes directly — the standard trick: the equation's solvability via the factorization of the symbol as a meromorphic function... The finite-interval asymptotics for symbols with real poles — this is genuinely nonstandard (poles on the contour). Krein's 1958/62 work covers rational symbols; ξ′/ξ is not rational but is in the Nevanlinna class... Honestly L3/L4 need library work with the GF book — beyond session scope to do rigorously. I'll document the argument shapes and mark them as \"assembly pending (library)\".\n\nActually, let me time-box: write the L1 upgrade into D-041 (edit the lemma table + add the proof sketch), note L3/L4 remain library assembly. Then domain sweep (§4A.5) — the last queued item. Actually the domain sweep is significant work too (list walls, ask which untouched field has machinery shaped like each wall, web-research top candidates). Given the session length, let me do L1 now and then run the domain sweep as a focused sub-stage, then wrap the session with a full report to the user (it's been a marathon).","signature":""},{"type":"text","text":"Paper sub-stages done. Now the 2.9 paper-work: L1 has a clean proof route (convolution kernel + analytic-functional FT), which I'll write into D-041; L3/L4 remain library assembly."},{"type":"tool_use","id":"Edit_244","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\derivations\\D-041-krein-frame-deficiency-convergence.md","old_string":"| L1 | ℋ(A_a) ↪ ℋ(A∞) unconditionally | OPEN (published proof via [14] uses RH); expected true; bounded isotropy suffices |","new_string":"| L1 | ℋ(A_a) ↪ ℋ(A∞) unconditionally | PROOF SKETCH COMPLETE (2026-08-19, below) — modulo the D-026-flagged tempered-FT bookkeeping |\n| L1′ | (argument) [v] = 0 ⟺ g∗v = 0 as a distribution (Q_W(v,w) = ⟨g∗v, w⟩ ∀w ∈ C∞_c(ℝ)); then ĝ·v̂ = 0 as analytic functionals (g∗v grows ≤ e^{\\|x\\|/2}, Paley–Wiener–Schwartz); ĝ = z⁻²ξ′/ξ nonzero meromorphic ⟹ v̂ ≡ 0 (identity theorem) ⟹ v = 0. No RH input. | write-up = Phase-5 item |"},"extra_content":null}]