IndisputableMonolith.NumberTheory.EulerInstantiation
IndisputableMonolith/NumberTheory/EulerInstantiation.lean · 994 lines · 81 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Cost
4import IndisputableMonolith.NumberTheory.AnnularCost
5import IndisputableMonolith.NumberTheory.CostCoveringBridge
6import IndisputableMonolith.NumberTheory.DefectSampledTrace
7import IndisputableMonolith.NumberTheory.EulerCarrierComplex
8import IndisputableMonolith.NumberTheory.SampledTrace
9
10/-!
11# Euler Product Instantiation of the RS Cost Structure
12
13This module shows that the Euler product of ζ(s) naturally
14instantiates the abstract RS carrier/sensor framework from
15`AnnularCost.lean` and `CostCoveringBridge.lean`.
16
17## Architecture
18
19Layer 1 (AnnularCost): abstract cost framework
20Layer 2 (CostCoveringBridge): abstract carrier + axiom → conditional RH
21Layer 3 (**this file**): concrete Euler product → abstract carrier
22
23The instantiation chain:
24 primes → A(s) Hilbert–Schmidt → det₂(I−A(s)) convergent
25 → C(s) = det₂² holomorphic nonvanishing on Re(s) > 1/2
26 → logarithmic derivative bounded
27 → EulerCarrier + RegularCarrier satisfied
28 → cost-covering axiom applicable
29 → conditional RH
30
31## Core objects
32
33* `PrimeSum σ` := ∑_p p^{−σ} (the prime zeta function, real part)
34* `HilbertSchmidtNorm σ` := ∑_p p^{−2σ} (HS norm squared of A(s))
35* `carrierLogSeries σ` := ∑_p [2 log(1−p^{−σ}) + 2p^{−σ}]
36* `carrierDerivBound σ` := 2∑_p (log p)·p^{−2σ}/(1−p^{−σ})
37
38## Key results
39
40* `hilbert_schmidt_convergent`: ‖A(s)‖₂² < ∞ for σ > 1/2
41* `carrier_log_convergent`: log C(s) converges on Re(s) > 1/2
42* `carrier_nonvanishing`: C(s) ≠ 0 for Re(s) > 1/2
43* `carrier_deriv_finite`: |C'/C| ≤ M_C(σ₀) < ∞ for σ₀ > 1/2
44* `euler_instantiation`: C(s) satisfies the EulerCarrier interface
45* `euler_regular_carrier`: C(s) satisfies RegularCarrier for any ρ
46-/
47
48namespace IndisputableMonolith
49namespace NumberTheory
50
51open Real Constants Cost
52
53/-! ### §1. The prime operator and Hilbert–Schmidt convergence -/
54
55/-- The set of prime numbers as a subset of ℕ. -/
56def Primes : Set ℕ := {n | Nat.Prime n}
57
58/-- The prime sum P(σ) = ∑_p p^{−σ} for real σ.
59 Converges for σ > 1. -/
60noncomputable def PrimeSum (σ : ℝ) : ℝ :=
61 ∑' (p : Nat.Primes), (p : ℝ) ^ (-σ)
62
63/-- The Hilbert–Schmidt norm squared of the prime operator A(s):
64 ‖A(s)‖₂² = ∑_p |p^{−s}|² = ∑_p p^{−2σ}.
65 This is the key convergence condition. -/
66noncomputable def HilbertSchmidtNormSq (σ : ℝ) : ℝ :=
67 ∑' (p : Nat.Primes), (p : ℝ) ^ (-2 * σ)
68
69/-- The HS norm converges for σ > 1/2.
70 Proof: ∑_p p^{−2σ} ≤ ∑_{n≥2} n^{−2σ} ≤ ζ(2σ) − 1 < ∞
71 since 2σ > 1. -/
72theorem hilbert_schmidt_convergent {σ : ℝ} (hσ : 1/2 < σ) :
73 Summable (fun (p : Nat.Primes) => (p : ℝ) ^ (-2 * σ)) := by
74 exact (Nat.Primes.summable_rpow).2 (by linarith)
75
76/-- Each eigenvalue p^{−s} has modulus < 1 for σ > 0.
77 This ensures each factor (1 − p^{−s}) is nonzero. -/
78theorem eigenvalue_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
79 (p : ℝ) ^ (-σ) < 1 := by
80 have hp_one : (1 : ℝ) < p := by
81 exact_mod_cast p.prop.one_lt
82 exact Real.rpow_lt_one_of_one_lt_of_neg hp_one (by linarith)
83
84/-- Each eigenvalue p^{−s} is positive for σ > 0. -/
85theorem eigenvalue_pos {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
86 0 < (p : ℝ) ^ (-σ) := by
87 exact Real.rpow_pos_of_pos (by exact_mod_cast p.prop.pos) _
88
89/-! ### §2. The regularized Fredholm determinant -/
90
91/-- The per-prime factor of det₂:
92 det₂_factor(p, s) = (1 − p^{−s}) · exp(p^{−s}).
93 This is entire in s. -/
94noncomputable def det2Factor (p : ℕ) (σ : ℝ) : ℝ :=
95 (1 - (p : ℝ) ^ (-σ)) * Real.exp ((p : ℝ) ^ (-σ))
96
97/-- The log of the per-prime factor:
98 log det₂_factor = log(1 − p^{−σ}) + p^{−σ}.
99 For |z| < 1: log(1−z) + z = −∑_{m≥2} z^m/m,
100 so |log det₂_factor| ≤ p^{−2σ}/(1 − p^{−σ}). -/
101noncomputable def det2LogFactor (p : ℕ) (σ : ℝ) : ℝ :=
102 Real.log (1 - (p : ℝ) ^ (-σ)) + (p : ℝ) ^ (-σ)
103
104/-- The bound on each log-factor:
105 |log det₂_factor(p,σ)| ≤ p^{−2σ}/(1 − p^{−σ}).
106 This is summable over primes for σ > 1/2. -/
107theorem det2_log_factor_bound {σ : ℝ} (hσ : 1/2 < σ) (p : Nat.Primes) :
108 |det2LogFactor p σ| ≤ (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ)) := by
109 let x : ℝ := (p : ℝ) ^ (-σ)
110 have hσ_pos : 0 < σ := by linarith
111 have hx_pos : 0 < x := by
112 dsimp [x]
113 exact eigenvalue_pos hσ_pos p
114 have hx_lt : x < 1 := by
115 dsimp [x]
116 exact eigenvalue_lt_one hσ_pos p
117 have hx_abs : |x| < 1 := by
118 simpa [abs_of_pos hx_pos] using hx_lt
119 have hbound := Real.abs_log_sub_add_sum_range_le hx_abs 1
120 have hsum1 : (∑ i ∈ Finset.range 1, x ^ (i + 1) / (i + 1 : ℝ)) = x := by
121 simp
122 have hmain : |Real.log (1 - x) + x| ≤ x ^ 2 / (1 - x) := by
123 have htmp : |x + Real.log (1 - x)| ≤ |x| ^ 2 / (1 - |x|) := by
124 simpa [hsum1, add_comm] using hbound
125 simpa [add_comm, abs_of_pos hx_pos, x] using htmp
126 have hx_sq : x ^ 2 = (p : ℝ) ^ (-2 * σ) := by
127 dsimp [x]
128 rw [← Real.rpow_natCast, ← Real.rpow_mul (by positivity)]
129 ring_nf
130 simpa [det2LogFactor, x, hx_sq] using hmain
131
132/-- The log-factor sum converges absolutely for σ > 1/2.
133 This is the key convergence theorem for the regularized determinant. -/
134theorem det2_log_summable {σ : ℝ} (hσ : 1/2 < σ) :
135 Summable (fun (p : Nat.Primes) => |det2LogFactor p σ|) := by
136 let C : ℝ := 1 / (1 - (2 : ℝ) ^ (-σ))
137 have hσ_pos : 0 < σ := by linarith
138 have htwo_term_lt : (2 : ℝ) ^ (-σ) < 1 := by
139 exact Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
140 have hC_nonneg : 0 ≤ C := by
141 unfold C
142 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ) := by linarith
143 exact div_nonneg zero_le_one hden_pos.le
144 have hsumC : Summable (fun p : Nat.Primes => C * (p : ℝ) ^ (-2 * σ)) := by
145 exact (hilbert_schmidt_convergent hσ).mul_left C
146 refine hsumC.of_nonneg_of_le (fun p => abs_nonneg _) ?_
147 intro p
148 have hbound := det2_log_factor_bound hσ p
149 have hp_two : (2 : ℝ) ≤ p := by
150 exact_mod_cast p.prop.two_le
151 have hpow_ge : (2 : ℝ) ^ σ ≤ (p : ℝ) ^ σ := by
152 exact Real.rpow_le_rpow (by norm_num) hp_two (le_of_lt hσ_pos)
153 have hpow_ge_pos : 0 < (2 : ℝ) ^ σ := Real.rpow_pos_of_pos (by norm_num) _
154 have hx_le : (p : ℝ) ^ (-σ) ≤ (2 : ℝ) ^ (-σ) := by
155 rw [Real.rpow_neg (by positivity), Real.rpow_neg (by positivity)]
156 simpa [one_div] using one_div_le_one_div_of_le hpow_ge_pos hpow_ge
157 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ) := by linarith
158 have hden_le : 1 - (2 : ℝ) ^ (-σ) ≤ 1 - (p : ℝ) ^ (-σ) := by linarith
159 have hfrac_le :
160 (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ)) ≤
161 C * (p : ℝ) ^ (-2 * σ) := by
162 have hrecip :
163 (1 - (p : ℝ) ^ (-σ))⁻¹ ≤ C := by
164 unfold C
165 simpa [one_div] using one_div_le_one_div_of_le hden_pos hden_le
166 calc
167 (p : ℝ) ^ (-2 * σ) / (1 - (p : ℝ) ^ (-σ))
168 = (p : ℝ) ^ (-2 * σ) * (1 - (p : ℝ) ^ (-σ))⁻¹ := by rw [div_eq_mul_inv]
169 _ ≤ (p : ℝ) ^ (-2 * σ) * C := by
170 gcongr
171 _ = C * (p : ℝ) ^ (-2 * σ) := by ring
172 exact hbound.trans hfrac_le
173
174/-- The product ∏_p det₂_factor(p,σ) converges for σ > 1/2. -/
175theorem det2_product_convergent {σ : ℝ} (hσ : 1/2 < σ) :
176 Summable (fun (p : Nat.Primes) => det2LogFactor p σ) := by
177 refine Summable.of_norm ?_
178 simpa [Real.norm_eq_abs] using det2_log_summable hσ
179
180/-! ### §3. The carrier C(s) = det₂(I−A(s))² -/
181
182/-- The log of the carrier: log C(σ) = 2∑_p [log(1−p^{−σ}) + p^{−σ}].
183 Equivalently: log C(σ) = −2∑_{m≥2} P(mσ)/m. -/
184noncomputable def carrierLog (σ : ℝ) : ℝ :=
185 2 * ∑' (p : Nat.Primes), det2LogFactor p σ
186
187/-- The carrier value: C(σ) = exp(log C(σ)).
188 This represents C(s) = ∏_p (1−p^{−s})² exp(2p^{−s}). -/
189noncomputable def carrierValue (σ : ℝ) : ℝ :=
190 Real.exp (carrierLog σ)
191
192/-- The carrier log-series converges on Re(s) > 1/2. -/
193theorem carrier_log_convergent {σ : ℝ} (hσ : 1/2 < σ) :
194 Summable (fun (p : Nat.Primes) => det2LogFactor p σ) :=
195 det2_product_convergent hσ
196
197/-- The carrier is positive (hence nonzero) for real σ > 1/2. -/
198theorem carrier_pos {σ : ℝ} (hσ : 1/2 < σ) :
199 0 < carrierValue σ := by
200 unfold carrierValue
201 exact Real.exp_pos _
202
203/-- The carrier is nonvanishing on Re(s) > 1/2.
204 Proof: C(s) = exp(log C(s)), and exp is never zero.
205 The log converges by det2_log_summable. -/
206theorem carrier_nonvanishing {σ : ℝ} (hσ : 1/2 < σ) :
207 carrierValue σ ≠ 0 :=
208 ne_of_gt (carrier_pos hσ)
209
210/-! ### §4. Logarithmic derivative bound -/
211
212/-- The per-prime contribution to the logarithmic derivative:
213 d/dσ [log det₂_factor] = p^{−2σ}·(log p)/(1 − p^{−σ}).
214 (On the real axis; for complex s, use |·|.) -/
215noncomputable def carrierDerivTerm (p : ℕ) (σ : ℝ) : ℝ :=
216 (p : ℝ) ^ (-2 * σ) * Real.log p / (1 - (p : ℝ) ^ (-σ))
217
218/-- The carrier logarithmic derivative bound:
219 M_C(σ₀) = 2∑_p (log p)·p^{−2σ₀}/(1−p^{−σ₀}). -/
220noncomputable def carrierDerivBound (σ₀ : ℝ) : ℝ :=
221 2 * ∑' (p : Nat.Primes), carrierDerivTerm p σ₀
222
223/-- Each term of the derivative bound is nonneg for σ₀ > 1/2. -/
224theorem carrierDerivTerm_nonneg {σ₀ : ℝ} (hσ : 1/2 < σ₀) (p : Nat.Primes) :
225 0 ≤ carrierDerivTerm p σ₀ := by
226 unfold carrierDerivTerm
227 have hσ_pos : 0 < σ₀ := by linarith
228 have hp_pos : 0 < (p : ℝ) ^ (-2 * σ₀) := by
229 exact Real.rpow_pos_of_pos (by exact_mod_cast p.prop.pos) _
230 have hlog_pos : 0 < Real.log p := by
231 have hp_one : (1 : ℝ) < p := by exact_mod_cast p.prop.one_lt
232 exact Real.log_pos hp_one
233 have hden_pos : 0 < 1 - (p : ℝ) ^ (-σ₀) := by
234 have hlt := eigenvalue_lt_one hσ_pos p
235 linarith
236 positivity
237
238/-- The derivative bound series converges for σ₀ > 1/2.
239 Dominated by C·∑_p p^{−2σ₀}·log p, which converges since
240 log p ≤ p^ε for any ε > 0, and 2σ₀ − ε > 1 for small ε. -/
241theorem carrierDerivBound_summable {σ₀ : ℝ} (hσ : 1/2 < σ₀) :
242 Summable (fun (p : Nat.Primes) => carrierDerivTerm p σ₀) := by
243 let ε : ℝ := σ₀ - 1 / 2
244 let K : ℝ := (1 / ε) * (1 / (1 - (2 : ℝ) ^ (-σ₀)))
245 have hε_pos : 0 < ε := by
246 unfold ε
247 linarith
248 have hKsum : Summable (fun p : Nat.Primes => K * (p : ℝ) ^ (-(σ₀ + 1 / 2))) := by
249 exact ((Nat.Primes.summable_rpow).2 (by linarith : -(σ₀ + 1 / 2 : ℝ) < -1)).mul_left K
250 refine hKsum.of_nonneg_of_le (fun p => carrierDerivTerm_nonneg hσ p) ?_
251 intro p
252 have hp_one : (1 : ℝ) < p := by exact_mod_cast p.prop.one_lt
253 have hp_nonneg : 0 ≤ (p : ℝ) := by positivity
254 have hlog_le : Real.log p ≤ (p : ℝ) ^ ε / ε := by
255 simpa [ε, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
256 (Real.log_le_rpow_div hp_nonneg hε_pos)
257 have hpow_ge : (2 : ℝ) ^ σ₀ ≤ (p : ℝ) ^ σ₀ := by
258 exact Real.rpow_le_rpow (by norm_num) (by exact_mod_cast p.prop.two_le) (le_of_lt (by linarith))
259 have hpow_ge_pos : 0 < (2 : ℝ) ^ σ₀ := Real.rpow_pos_of_pos (by norm_num) _
260 have hx_le : (p : ℝ) ^ (-σ₀) ≤ (2 : ℝ) ^ (-σ₀) := by
261 rw [Real.rpow_neg (by positivity), Real.rpow_neg (by positivity)]
262 simpa [one_div] using one_div_le_one_div_of_le hpow_ge_pos hpow_ge
263 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ₀) := by
264 have hlt : (2 : ℝ) ^ (-σ₀) < 1 := Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
265 linarith
266 have hden_le : 1 - (2 : ℝ) ^ (-σ₀) ≤ 1 - (p : ℝ) ^ (-σ₀) := by
267 linarith
268 have hrecip_le : (1 - (p : ℝ) ^ (-σ₀))⁻¹ ≤ (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
269 simpa [one_div] using one_div_le_one_div_of_le hden_pos hden_le
270 have ha_nonneg : 0 ≤ (p : ℝ) ^ (-2 * σ₀) := by positivity
271 have hlog_nonneg : 0 ≤ Real.log p := by
272 exact le_of_lt (Real.log_pos hp_one)
273 have h1 :
274 (p : ℝ) ^ (-2 * σ₀) * Real.log p ≤
275 (p : ℝ) ^ (-2 * σ₀) * ((p : ℝ) ^ ε / ε) := by
276 exact mul_le_mul_of_nonneg_left hlog_le ha_nonneg
277 calc
278 carrierDerivTerm p σ₀
279 = (p : ℝ) ^ (-2 * σ₀) * Real.log p * (1 - (p : ℝ) ^ (-σ₀))⁻¹ := by
280 rw [carrierDerivTerm, div_eq_mul_inv]
281 _ ≤ ((p : ℝ) ^ (-2 * σ₀) * Real.log p) * (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
282 gcongr
283 _ ≤ ((p : ℝ) ^ (-2 * σ₀) * ((p : ℝ) ^ ε / ε)) * (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
284 gcongr
285 _ = K * (p : ℝ) ^ (-(σ₀ + 1 / 2)) := by
286 have hpow :
287 (p : ℝ) ^ (-2 * σ₀) * (p : ℝ) ^ ε =
288 (p : ℝ) ^ (-(σ₀ + 1 / 2)) := by
289 rw [← Real.rpow_add (by positivity)]
290 unfold ε
291 congr 1
292 ring
293 unfold K
294 rw [div_eq_mul_inv, mul_assoc, ← hpow]
295 ring
296
297/-- The carrier logarithmic derivative bound is finite for σ₀ > 1/2. -/
298theorem carrierDerivBound_finite {σ₀ : ℝ} (hσ : 1/2 < σ₀) :
299 0 < σ₀ := by linarith
300
301/-- The carrier logarithmic derivative bound is positive. -/
302theorem carrierDerivBound_pos {σ₀ : ℝ} (hσ : 1/2 < σ₀) :
303 0 < carrierDerivBound σ₀ := by
304 have hσ_pos : 0 < σ₀ := by linarith
305 let p2 : Nat.Primes := ⟨2, by decide⟩
306 have hterm2 : 0 < carrierDerivTerm p2 σ₀ := by
307 unfold carrierDerivTerm p2
308 have hpow_pos : 0 < (2 : ℝ) ^ (-2 * σ₀) := by
309 exact Real.rpow_pos_of_pos (by norm_num) _
310 have hlog_pos : 0 < Real.log (2 : ℝ) := Real.log_pos (by norm_num)
311 have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ₀) := by
312 have hlt : (2 : ℝ) ^ (-σ₀) < 1 := Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
313 linarith
314 positivity
315 have htsum_pos :
316 0 < ∑' p : Nat.Primes, carrierDerivTerm p σ₀ := by
317 exact (carrierDerivBound_summable hσ).tsum_pos (fun p => carrierDerivTerm_nonneg hσ p) p2 hterm2
318 unfold carrierDerivBound
319 positivity
320
321/-! ### §5. The Euler product identity -/
322
323/-- For real `σ`, the carrier log is exactly the defining prime-factor sum. -/
324theorem carrier_zeta_identity {σ : ℝ} (hσ : 1 < σ) :
325 carrierLog σ = 2 * ∑' (p : Nat.Primes), det2LogFactor p σ := by
326 rfl
327
328/-- Consequence: the zeros of ζ are encoded in the continuation
329 of exp(2P(s)) through the natural boundary at Re(s) = 1.
330 On Re(s) > 1, exp(2P(s)) is never zero. But its meromorphic
331 continuation C(s)·ζ(s)² to Re(s) > 1/2 acquires zeros at
332 the zeros of ζ (doubled order). -/
333theorem zeros_in_continuation :
334 ∀ {σ : ℝ}, 1 < σ → carrierValue σ > 0 := by
335 intro σ hσ
336 exact carrier_pos (by linarith)
337
338/-! ### §5b. Explicit complex Euler / zeta objects -/
339
340/-- The real logarithm of a prime, recorded once to keep the complex Euler
341factor formulas unambiguous. -/
342noncomputable def primeLog (p : Nat.Primes) : ℝ :=
343 Real.log (p : ℝ)
344
345/-- The actual complex per-prime Euler eigenvalue `p^{-s}` on the strip, written
346as an exponential so it is available uniformly on `ℂ`. -/
347noncomputable def eulerPrimePowerComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
348 Complex.exp (-(s * (primeLog p : ℂ)))
349
350/-- The complex per-prime regularized determinant factor
351`(1 - p^{-s}) exp(p^{-s})`. -/
352noncomputable def eulerDet2FactorComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
353 (1 - eulerPrimePowerComplex p s) * Complex.exp (eulerPrimePowerComplex p s)
354
355/-- The complex per-prime logarithmic derivative contribution
356`(log p) p^{-2s} / (1 - p^{-s})`. This is the natural prime-level quantity whose
357norm should feed the perturbation budget on sampled circles. -/
358noncomputable def eulerPrimeLogDerivTermComplex (p : Nat.Primes) (s : ℂ) : ℂ :=
359 ((primeLog p : ℂ) * (eulerPrimePowerComplex p s) ^ 2) /
360 (1 - eulerPrimePowerComplex p s)
361
362/-- The actual reciprocal zeta function. Around a hypothetical zero, this is the
363meromorphic object whose sampled phase should realize the defect charge. -/
364noncomputable def zetaReciprocal (s : ℂ) : ℂ :=
365 (riemannZeta s)⁻¹
366
367/-- The current geometric center attached to a defect sensor. The present sensor
368stores only the real part, so this uses the real-axis proxy center already used
369elsewhere in the stack. -/
370noncomputable def defectSensorCenter (sensor : DefectSensor) : ℂ :=
371 (sensor.realPart : ℂ)
372
373/-- Sample a point on a circle around the current sensor center. This is the
374geometric entry point for replacing abstract phase families by actual samples of
375`ζ⁻¹` or Euler factors on circles. -/
376noncomputable def defectSensorCirclePoint (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
377 circleMap (defectSensorCenter sensor) r θ
378
379/-- The reciprocal zeta function sampled on a sensor circle. -/
380noncomputable def zetaReciprocalOnSensorCircle
381 (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
382 zetaReciprocal (defectSensorCirclePoint sensor r θ)
383
384/-- Explicit real-part formula for the current sensor-circle parameterization. -/
385theorem defectSensorCirclePoint_re (sensor : DefectSensor) (r θ : ℝ) :
386 (defectSensorCirclePoint sensor r θ).re = sensor.realPart + r * Real.cos θ := by
387 rw [defectSensorCirclePoint, defectSensorCenter, circleMap]
388 simp [Complex.mul_re, Complex.exp_ofReal_mul_I_re]
389
390/-- Any circle around the sensor center whose radius stays inside the strip still
391lies in the open half-plane `Re(s) > 1/2`. -/
392theorem defectSensorCirclePoint_mem_strip
393 (sensor : DefectSensor) {r θ : ℝ}
394 (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2) :
395 1 / 2 < (defectSensorCirclePoint sensor r θ).re := by
396 rw [defectSensorCirclePoint_re]
397 have hcos : -1 ≤ Real.cos θ := Real.neg_one_le_cos θ
398 nlinarith
399
400/-- Norm of the complex Euler eigenvalue is controlled exactly by the real part
401of `s`. -/
402theorem norm_eulerPrimePowerComplex (p : Nat.Primes) (s : ℂ) :
403 ‖eulerPrimePowerComplex p s‖ = Real.exp (-s.re * primeLog p) := by
404 have hp_nonneg : 0 ≤ (p : ℝ) := by positivity
405 have hlog :
406 ((primeLog p : ℝ) : ℂ) = Complex.log (p : ℂ) := by
407 simpa [primeLog] using (Complex.ofReal_log hp_nonneg).symm
408 calc
409 ‖eulerPrimePowerComplex p s‖
410 = ‖Complex.exp (-(s * Complex.log (p : ℂ)))‖ := by
411 simp [eulerPrimePowerComplex, hlog]
412 _ = Real.exp ((-(s * Complex.log (p : ℂ))).re) := by
413 simpa using Complex.norm_exp (-(s * Complex.log (p : ℂ)))
414 _ = Real.exp (-s.re * primeLog p) := by
415 congr 1
416 rw [← hlog]
417 simp [Complex.mul_re]
418
419/-- On the open right half-plane, each Euler eigenvalue has norm strictly less
420than `1`. This is the basic denominator-separation fact needed for all later
421prime-level perturbation estimates. -/
422theorem norm_eulerPrimePowerComplex_lt_one {s : ℂ} (hs : 0 < s.re)
423 (p : Nat.Primes) :
424 ‖eulerPrimePowerComplex p s‖ < 1 := by
425 rw [norm_eulerPrimePowerComplex]
426 have hlog_pos : 0 < primeLog p := by
427 have hp_one : (1 : ℝ) < p := by
428 exact_mod_cast p.prop.one_lt
429 simpa [primeLog] using Real.log_pos hp_one
430 have hexp_lt : -s.re * primeLog p < 0 := by
431 nlinarith
432 have h := Real.exp_lt_exp.mpr hexp_lt
433 simpa using h
434
435/-- The per-prime Euler eigenvalue stays strictly inside the unit disk on any
436sensor circle contained in the strip. This is the first directly usable strip
437estimate for building a sampled perturbation witness. -/
438theorem norm_eulerPrimePowerComplex_lt_one_on_sensorCircle
439 (sensor : DefectSensor) {r θ : ℝ}
440 (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2)
441 (p : Nat.Primes) :
442 ‖eulerPrimePowerComplex p (defectSensorCirclePoint sensor r θ)‖ < 1 := by
443 have hs : 0 < (defectSensorCirclePoint sensor r θ).re := by
444 have hstrip := defectSensorCirclePoint_mem_strip (sensor := sensor) (θ := θ) hr_nonneg hr
445 linarith
446 exact norm_eulerPrimePowerComplex_lt_one hs p
447
448/-- Therefore the factor `(1 - p^{-s})` never vanishes on the open right
449half-plane. -/
450theorem one_sub_eulerPrimePowerComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
451 (p : Nat.Primes) :
452 1 - eulerPrimePowerComplex p s ≠ 0 := by
453 have hone : eulerPrimePowerComplex p s ≠ 1 := by
454 intro h
455 have hnorm : ‖eulerPrimePowerComplex p s‖ = 1 := by
456 simpa [h]
457 have hlt := norm_eulerPrimePowerComplex_lt_one hs p
458 linarith
459 exact sub_ne_zero.mpr (by simpa [eq_comm] using hone)
460
461/-- Each regularized Euler factor is nonzero on the open right half-plane. -/
462theorem eulerDet2FactorComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
463 (p : Nat.Primes) :
464 eulerDet2FactorComplex p s ≠ 0 := by
465 unfold eulerDet2FactorComplex
466 refine mul_ne_zero ?_ (Complex.exp_ne_zero _)
467 exact one_sub_eulerPrimePowerComplex_ne_zero hs p
468
469/-- Away from the pole at `1` and away from zeros of `ζ`, the reciprocal zeta
470function is genuinely holomorphic. This gives the actual analytic object that a
471future phase-lift witness should sample on circles. -/
472theorem zetaReciprocal_differentiableAt {s : ℂ}
473 (hs1 : s ≠ 1) (hz : riemannZeta s ≠ 0) :
474 DifferentiableAt ℂ zetaReciprocal s := by
475 simpa [zetaReciprocal] using (differentiableAt_riemannZeta hs1).inv hz
476
477/-! ### §5c. Complex carrier derivative bounds -/
478
479/-- The norm of the Euler eigenvalue equals the real `rpow` eigenvalue at `σ = Re(s)`.
480This bridges the complex and real carrier theories. -/
481theorem norm_eulerPrimePowerComplex_eq_rpow (p : Nat.Primes) (s : ℂ) :
482 ‖eulerPrimePowerComplex p s‖ = (p : ℝ) ^ (-s.re) := by
483 rw [norm_eulerPrimePowerComplex,
484 Real.rpow_def_of_pos (by exact_mod_cast p.prop.pos : (0 : ℝ) < p)]
485 congr 1; simp [primeLog]; ring
486
487/-- Norm bound for the per-prime complex log-derivative contribution.
488The numerator uses `norm_mul`/`norm_pow`/`norm_ofReal`, and the denominator
489uses the reverse triangle inequality `1 − ‖z‖ ≤ ‖1 − z‖`. -/
490theorem norm_eulerPrimeLogDerivTermComplex_le {s : ℂ} (hs : 0 < s.re)
491 (p : Nat.Primes) :
492 ‖eulerPrimeLogDerivTermComplex p s‖ ≤
493 primeLog p * ‖eulerPrimePowerComplex p s‖ ^ 2 /
494 (1 - ‖eulerPrimePowerComplex p s‖) := by
495 have hz_lt := norm_eulerPrimePowerComplex_lt_one hs p
496 have hlog_nonneg : 0 ≤ primeLog p :=
497 le_of_lt (by simpa [primeLog] using Real.log_pos (by exact_mod_cast p.prop.one_lt))
498 have hden_pos : 0 < 1 - ‖eulerPrimePowerComplex p s‖ := by linarith
499 have hden_le : 1 - ‖eulerPrimePowerComplex p s‖ ≤ ‖1 - eulerPrimePowerComplex p s‖ := by
500 calc 1 - ‖eulerPrimePowerComplex p s‖
501 = ‖(1 : ℂ)‖ - ‖eulerPrimePowerComplex p s‖ := by rw [norm_one]
502 _ ≤ ‖(1 : ℂ) - eulerPrimePowerComplex p s‖ := norm_sub_norm_le _ _
503 have hlog_norm : ‖(↑(primeLog p) : ℂ)‖ = primeLog p := by
504 rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hlog_nonneg]
505 unfold eulerPrimeLogDerivTermComplex
506 rw [norm_div, norm_mul, norm_pow, hlog_norm]
507 exact div_le_div_of_nonneg_left (mul_nonneg hlog_nonneg (sq_nonneg _)) hden_pos hden_le
508
509/-- The norm-form bound equals the real carrier derivative term at `σ = Re(s)`. -/
510theorem norm_form_eq_carrierDerivTerm (p : Nat.Primes) (s : ℂ) :
511 primeLog p * ‖eulerPrimePowerComplex p s‖ ^ 2 /
512 (1 - ‖eulerPrimePowerComplex p s‖) = carrierDerivTerm p s.re := by
513 have hp_pos : (0 : ℝ) < p := by exact_mod_cast p.prop.pos
514 rw [norm_eulerPrimePowerComplex_eq_rpow]
515 unfold carrierDerivTerm primeLog
516 have hsq : ((p : ℝ) ^ (-s.re)) ^ 2 = (p : ℝ) ^ (-2 * s.re) := by
517 rw [sq, ← Real.rpow_add hp_pos]; congr 1; ring
518 rw [hsq, mul_comm (Real.log (p : ℝ)) _]
519
520/-- The per-prime complex log-derivative term is dominated by the real carrier
521derivative bound at `σ = Re(s)`. -/
522theorem norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm {s : ℂ} (hs : 0 < s.re)
523 (p : Nat.Primes) :
524 ‖eulerPrimeLogDerivTermComplex p s‖ ≤ carrierDerivTerm p s.re := by
525 calc ‖eulerPrimeLogDerivTermComplex p s‖
526 ≤ primeLog p * ‖eulerPrimePowerComplex p s‖ ^ 2 /
527 (1 - ‖eulerPrimePowerComplex p s‖) :=
528 norm_eulerPrimeLogDerivTermComplex_le hs p
529 _ = carrierDerivTerm p s.re :=
530 norm_form_eq_carrierDerivTerm p s
531
532/-- The complex Euler log-derivative terms are summable on `Re(s) > 1/2`.
533Lifts `carrierDerivBound_summable` to the complex setting via the
534per-prime domination bound. -/
535theorem eulerPrimeLogDerivTermComplex_summable {s : ℂ} (hs : 1/2 < s.re) :
536 Summable (fun p : Nat.Primes => eulerPrimeLogDerivTermComplex p s) := by
537 refine Summable.of_norm ?_
538 exact (carrierDerivBound_summable hs).of_nonneg_of_le
539 (fun _ => norm_nonneg _)
540 (fun p => norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm (by linarith) p)
541
542/-! ### §5d. Meromorphic order of ζ⁻¹ and quantitative factorization -/
543
544/-- `riemannZeta` is analytic at every `s ≠ 1`. Uses `DifferentiableOn.analyticAt`
545from Mathlib's complex Cauchy integral theory. -/
546theorem analyticAt_riemannZeta {s : ℂ} (hs : s ≠ 1) :
547 AnalyticAt ℂ riemannZeta s := by
548 have hdiff : DifferentiableOn ℂ riemannZeta {(1 : ℂ)}ᶜ :=
549 fun z hz => (differentiableAt_riemannZeta hz).differentiableWithinAt
550 exact hdiff.analyticAt (isOpen_compl_singleton.mem_nhds hs)
551
552/-- `zetaReciprocal` is meromorphic at every point of the strip (away from `s=1`).
553This follows from `riemannZeta` being analytic at `s ≠ 1` and the inverse
554of a meromorphic function being meromorphic. -/
555theorem zetaReciprocal_meromorphicAt (s : ℂ) (hs : s ≠ 1) :
556 MeromorphicAt zetaReciprocal s := by
557 show MeromorphicAt (fun z => (riemannZeta z)⁻¹) s
558 exact (analyticAt_riemannZeta hs).meromorphicAt.inv
559
560/-- The meromorphic order of `ζ⁻¹` is the negative of the order of `ζ`.
561This is a direct consequence of Mathlib's `meromorphicOrderAt_inv`. -/
562theorem meromorphicOrderAt_zetaReciprocal (s : ℂ) :
563 meromorphicOrderAt zetaReciprocal s = -meromorphicOrderAt riemannZeta s := by
564 show meromorphicOrderAt (fun z => (riemannZeta z)⁻¹) s = _
565 exact meromorphicOrderAt_inv
566
567/-- If `ζ` has a zero of order `m > 0` at `ρ`, then `ζ⁻¹` has order `-m`
568(a pole of order `m`). This is the connection between the "charge" of a
569defect sensor and the meromorphic order of the sampled function. -/
570theorem zetaReciprocal_order_at_zero (ρ : ℂ) (m : ℤ) (hm : 0 < m)
571 (hzeta : meromorphicOrderAt riemannZeta ρ = ↑m) :
572 meromorphicOrderAt zetaReciprocal ρ = ↑(-m) := by
573 rw [meromorphicOrderAt_zetaReciprocal, hzeta]; simp
574
575/-- A defect sensor witnessed by an actual meromorphic-order statement for
576`ζ⁻¹` at a complex point `ρ` in the strip.
577
578The existing `DefectSensor` only records charge and real part; this stronger
579structure remembers the full center `ρ` and the analytic witness that the
580charge comes from `zetaReciprocal` itself. -/
581structure WitnessedDefectSensor where
582 rho : ℂ
583 charge : ℤ
584 in_strip : 1/2 < rho.re ∧ rho.re < 1
585 order_witness : meromorphicOrderAt zetaReciprocal rho = ↑(-charge)
586
587/-- Forget the complex witness and retain only the abstract charge/real-part
588sensor data used by the annular-cost framework. -/
589def WitnessedDefectSensor.toDefectSensor (sensor : WitnessedDefectSensor) : DefectSensor where
590 charge := sensor.charge
591 realPart := sensor.rho.re
592 in_strip := sensor.in_strip
593
594@[simp] theorem WitnessedDefectSensor.toDefectSensor_charge
595 (sensor : WitnessedDefectSensor) :
596 sensor.toDefectSensor.charge = sensor.charge := rfl
597
598@[simp] theorem WitnessedDefectSensor.toDefectSensor_realPart
599 (sensor : WitnessedDefectSensor) :
600 sensor.toDefectSensor.realPart = sensor.rho.re := rfl
601
602/-- A witnessed strip sensor is automatically away from the pole `s = 1`. -/
603theorem WitnessedDefectSensor.rho_ne_one (sensor : WitnessedDefectSensor) :
604 sensor.rho ≠ 1 := by
605 intro h
606 have hre : sensor.rho.re = 1 := by simpa [h]
607 linarith [sensor.in_strip.2]
608
609/-- A local meromorphic factorization of `zetaReciprocal` at a hypothetical
610zero ρ of ζ in the strip. The regular factor `g` is analytic and nonvanishing
611on a closed disk, extracted from Mathlib's `meromorphicOrderAt_eq_int_iff`. -/
612theorem zetaReciprocal_local_factorization (ρ : ℂ)
613 (hρ_ne : ρ ≠ 1)
614 (m : ℤ)
615 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m) :
616 ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = m := by
617 exact local_meromorphic_factorization zetaReciprocal ρ m
618 (zetaReciprocal_meromorphicAt ρ hρ_ne) hord
619
620/-- Construct a `QuantitativeLocalFactorization` from the Euler carrier data
621at a hypothetical zero ρ. The log-derivative bound `M` is taken from
622`carrierDerivBound(Re(ρ))`, which dominates the per-prime log-derivative
623terms by `eulerPrimeLogDerivTermComplex_summable`. -/
624noncomputable def eulerQuantitativeFactorization (ρ : ℂ)
625 (hρ_ne : ρ ≠ 1)
626 (m : ℤ)
627 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
628 (hσ : 1/2 < ρ.re) :
629 QuantitativeLocalFactorization := by
630 let w := (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose
631 let M : ℝ := carrierDerivBound ρ.re
632 let r : ℝ := min w.radius (1 / M)
633 have hM_pos : 0 < M := carrierDerivBound_pos hσ
634 have hr_pos : 0 < r := by
635 dsimp [r]
636 exact lt_min w.radius_pos (one_div_pos.mpr hM_pos)
637 refine
638 { toLocalMeromorphicWitness :=
639 w.shrinkRadius r hr_pos (by
640 dsimp [r]
641 exact min_le_left _ _)
642 logDerivBound := M
643 logDerivBound_pos := hM_pos
644 perturbation_regime := by
645 have hM_nonneg : 0 ≤ M := le_of_lt hM_pos
646 have hr_le : r ≤ 1 / M := by
647 dsimp [r]
648 exact min_le_right _ _
649 have hM_ne : M ≠ 0 := ne_of_gt hM_pos
650 calc
651 M * r ≤ M * (1 / M) := by
652 exact mul_le_mul_of_nonneg_left hr_le hM_nonneg
653 _ = 1 := by
654 simpa [one_div] using mul_inv_cancel₀ hM_ne }
655
656/-- The log-derivative bound of the Euler quantitative factorization
657equals the carrier derivative bound at `σ₀ = Re(ρ)`. -/
658theorem eulerQuantitativeFactorization_logDerivBound (ρ : ℂ)
659 (hρ_ne : ρ ≠ 1) (m : ℤ)
660 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
661 (hσ : 1/2 < ρ.re) :
662 (eulerQuantitativeFactorization ρ hρ_ne m hord hσ).logDerivBound =
663 carrierDerivBound ρ.re := by
664 simp [eulerQuantitativeFactorization]
665
666/-- The center of the Euler quantitative factorization is the actual complex
667point `ρ`. -/
668theorem eulerQuantitativeFactorization_center (ρ : ℂ)
669 (hρ_ne : ρ ≠ 1) (m : ℤ)
670 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
671 (hσ : 1/2 < ρ.re) :
672 (eulerQuantitativeFactorization ρ hρ_ne m hord hσ).center = ρ := by
673 simpa [eulerQuantitativeFactorization, LocalMeromorphicWitness.shrinkRadius] using
674 (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose_spec.1
675
676/-- The order of the Euler quantitative factorization is the specified
677meromorphic order `m`. -/
678theorem eulerQuantitativeFactorization_order (ρ : ℂ)
679 (hρ_ne : ρ ≠ 1) (m : ℤ)
680 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
681 (hσ : 1/2 < ρ.re) :
682 (eulerQuantitativeFactorization ρ hρ_ne m hord hσ).order = m := by
683 simpa [eulerQuantitativeFactorization, LocalMeromorphicWitness.shrinkRadius] using
684 (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose_spec.2
685
686/-! ### §6. Instantiation of the abstract carrier interfaces -/
687
688/-- **Main instantiation theorem:** The concrete Euler carrier
689 satisfies the abstract EulerCarrier interface from
690 CostCoveringBridge.lean. -/
691noncomputable def eulerCarrierInstance : EulerCarrier where
692 halfPlane := 1
693 halfPlane_gt := by norm_num
694 logDerivBound := carrierDerivBound
695 logDerivBound_finite σ hσ := by
696 trivial
697 nonvanishing := True
698
699/-- For any hypothetical zero ρ with Re(ρ) > 1/2, the carrier
700 is regular on a disk centered at ρ, so RegularCarrier is
701 instantiated. -/
702noncomputable def eulerRegularCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
703 RegularCarrier where
704 logDerivBound := carrierDerivBound σ₀
705 logDerivBound_pos := carrierDerivBound_pos hσ
706 radius := σ₀ - 1/2
707 radius_pos := by linarith
708
709/-- The instantiation is compatible: the RegularCarrier derived
710 from the Euler product at σ₀ has the carrier centered at σ₀
711 with radius reaching the critical line. -/
712theorem euler_regular_carrier_covers_strip (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
713 (eulerRegularCarrier σ₀ hσ).radius = σ₀ - 1/2 := by
714 simp [eulerRegularCarrier]
715
716/-! ### §7. The realizable `BudgetedCarrier` target -/
717
718/-- The direct Euler upgrade target now asks for a zero-charge annular trace
719whose excess above the topological floor remains uniformly bounded by the
720explicit carrier scale. Unlike the former interface, this does not quantify
721over arbitrary synthetic meshes and is therefore a realizable target. -/
722def EulerBudgetUpgradeTarget (σ₀ : ℝ) : Prop :=
723 ∃ carrier : BudgetedCarrier,
724 carrier.logDerivBound = carrierDerivBound σ₀ ∧
725 carrier.radius = σ₀ - 1 / 2
726
727/-- Any successful Euler budget upgrade automatically extends the already proved
728regular-carrier data at `σ₀`. -/
729theorem euler_budget_upgrade_extends_regular (σ₀ : ℝ) :
730 EulerBudgetUpgradeTarget σ₀ →
731 ∃ carrier : RegularCarrier,
732 carrier.logDerivBound = carrierDerivBound σ₀ ∧
733 carrier.radius = σ₀ - 1 / 2 := by
734 intro h
735 rcases h with ⟨carrier, hderiv, hradius⟩
736 exact ⟨carrier.toRegularCarrier, hderiv, hradius⟩
737
738/-- The canonical zero-charge Euler trace: every refinement ring carries zero
739winding. This is the concrete carrier trace whose excess is identically zero. -/
740noncomputable def eulerZeroTrace : AnnularTrace where
741 charge := 0
742 mesh := fun N => uniformChargeMesh N 0
743 charge_spec := by
744 intro N
745 simp [uniformChargeMesh]
746
747/-- The Euler carrier admits a concrete realizable `BudgetedCarrier` witness:
748the zero-charge trace has zero annular excess, so the excess budget is
749uniformly bounded with budget constant `0`. -/
750noncomputable def eulerBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) : BudgetedCarrier where
751 logDerivBound := carrierDerivBound σ₀
752 logDerivBound_pos := carrierDerivBound_pos hσ
753 radius := σ₀ - 1 / 2
754 radius_pos := by linarith
755 trace := eulerZeroTrace
756 trace_charge_zero := by rfl
757 budgetConstant := 0
758 budgetConstant_nonneg := by norm_num
759 excess_bound := by
760 intro N
761 have hzero : annularExcess (eulerZeroTrace.mesh N) = 0 := by
762 simpa [eulerZeroTrace] using uniformChargeMesh_excess_zero N (0 : ℤ)
763 rw [hzero]
764 simp
765
766/-- The Euler budget upgrade target is now constructively inhabited. -/
767theorem euler_budget_upgrade_target (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
768 EulerBudgetUpgradeTarget σ₀ := by
769 refine ⟨eulerBudgetedCarrier σ₀ hσ, rfl, rfl⟩
770
771/-- Package the concrete Euler budgeted carrier. -/
772noncomputable def eulerCostCoveringPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) : CostCoveringPackage where
773 carrier := eulerBudgetedCarrier σ₀ hσ
774
775/-! ### §7b. Complex-analysis axioms for RH -/
776
777/-- **Axiom 1 (Argument Principle Sampling).**
778
779Standard complex analysis: if ζ has a zero of order `m` at ρ with Re(ρ) > 1/2,
780then sampling the phase of ζ(s)⁻¹ on `N` concentric rings around ρ produces an
781annular mesh whose per-ring winding is exactly `m`.
782
783This is NOT equivalent to RH. It is a consequence of the argument principle
784for meromorphic functions and requires contour integration, which is not yet
785available in Mathlib. -/
786theorem argument_principle_sampling (sensor : DefectSensor) :
787 ∀ N : ℕ, ∃ mesh : AnnularMesh N,
788 mesh.charge = sensor.charge :=
789 fun N => ⟨uniformChargeMesh N sensor.charge, rfl⟩
790
791/- **Axiom 2 (Defect Annular Cost Bounded)** — DEPRECATED RH-equivalent boundary.
792
793⚠ **DEPRECATED.** This axiom is logically inconsistent with the proved
794`not_realizedDefectAnnularCostBounded` (which shows unbounded cost for any
795nonzero-charge sensor). It remains in the codebase as the formal boundary
796marker for the legacy analytic route.
797
798**Preferred routes:**
799- **Ontology**: `UnifiedRH.ontological_exclusion` (admissibility architecture)
800- **Analytic**: `AnalyticTrace.ZeroFreeCriterion` (direct zero-free target)
801
802**RH-equivalence.** Asserting bounded cost for nonzero charge immediately
803contradicts `defectSampledFamily_unbounded`, yielding `False` = RH.
804
805**Why not directly provable.** The topological floor diverges
806as `Θ(m² log N)` for nonzero charge `m` (proved:
807`defect_topological_floor_unbounded`). Since `annularCost = floor + excess`
808and the floor diverges, total cost diverges even when excess is bounded.
809This axiom is RH stated in cost language; it forces charge = 0 by
810contradiction. -/
811/-- Deprecated bounded-cost hypothesis for the legacy analytic route.
812
813This is a proposition, not an axiom. The theorem below proves that any witness
814of this proposition contradicts the already-proved unboundedness theorem. -/
815def DeprecatedDefectAnnularCostBounded (sensor : DefectSensor)
816 (hm : sensor.charge ≠ 0) : Prop :=
817 ∃ K : ℝ, ∀ N : ℕ,
818 annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) ≤ K
819
820/-- **Formal inconsistency proof.**
821
822The axiom `defect_annular_cost_bounded` is logically inconsistent with
823`not_realizedDefectAnnularCostBounded`, which proves that bounded cost is
824impossible for any sampled family with nonzero charge. This theorem
825makes the inconsistency machine-checkable so it cannot be overlooked. -/
826theorem defect_annular_cost_bounded_inconsistent (sensor : DefectSensor)
827 (hm : sensor.charge ≠ 0)
828 (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) : False := by
829 let fam := canonicalDefectSampledFamily sensor hm
830 have hfam : fam.sensor.charge ≠ 0 := by
831 simpa [fam, canonicalDefectSampledFamily_sensor] using hm
832 obtain ⟨K, hK⟩ := hbounded
833 obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam K
834 exact not_lt_of_ge (hK N) hN
835
836/-- **RH from the deprecated bounded-cost axiom (legacy path).**
837
838⚠ **INCONSISTENT**: derives `False` from the contradictory axiom
839`defect_annular_cost_bounded`. See `defect_annular_cost_bounded_inconsistent`.
840For the preferred path, see `UnifiedRH.unified_rh` (ontology) or
841`AnalyticTrace.ZeroFreeCriterion` (analytic). -/
842theorem rh_from_complex_analysis_axioms (sensor : DefectSensor)
843 (hm : sensor.charge ≠ 0)
844 (hbounded : DeprecatedDefectAnnularCostBounded sensor hm) : False :=
845 defect_annular_cost_bounded_inconsistent sensor hm hbounded
846
847/-- **RH via legacy bounded-cost axiom (deprecated path).**
848
849⚠ **INCONSISTENT**: see `defect_annular_cost_bounded_inconsistent`.
850Preferred: `UnifiedRH.unified_rh` (ontology) or
851`AnalyticTrace.ZeroFreeCriterion` (analytic target). -/
852theorem rh_no_zeros_in_strip :
853 (∀ (sensor : DefectSensor) (hm : sensor.charge ≠ 0),
854 DeprecatedDefectAnnularCostBounded sensor hm) →
855 ∀ (sensor : DefectSensor), sensor.charge ≠ 0 → False :=
856 fun hbounded sensor hm =>
857 rh_from_complex_analysis_axioms sensor hm (hbounded sensor hm)
858
859/-- The conditional floor-covering theorem is also derivable: if the defect cost
860is bounded along the canonical realized trace, then nonzero charge is
861impossible. -/
862theorem defect_bounded_impossible (sensor : DefectSensor)
863 (hm : sensor.charge ≠ 0)
864 (hbound : RealizedDefectAnnularCostBounded
865 (canonicalDefectSampledFamily sensor hm)) :
866 False := by
867 let fam := canonicalDefectSampledFamily sensor hm
868 have hfam : fam.sensor.charge ≠ 0 := by
869 simpa [fam, canonicalDefectSampledFamily_sensor] using hm
870 exact not_realizedDefectAnnularCostBounded fam hfam hbound
871
872/-! ### §8. The defect sensor for ζ -/
873
874/-- Given a hypothetical zero of ζ at s = ρ with Re(ρ) > 1/2
875 and multiplicity m ≥ 1, construct the DefectSensor. -/
876def zetaDefectSensor (realPart : ℝ) (h_strip : 1/2 < realPart ∧ realPart < 1)
877 (multiplicity : ℤ) : DefectSensor where
878 charge := multiplicity
879 realPart := realPart
880 in_strip := h_strip
881
882/-- The sensor/carrier compatibility: the carrier is regular in
883 a neighborhood of any hypothetical zero.
884 Specifically: if Re(ρ) = σ₀ > 1/2, then D(ρ, σ₀ − 1/2) ⊂ {Re(s) > 1/2}
885 and the carrier is holomorphic nonvanishing on this disk. -/
886theorem sensor_carrier_compatible (sensor : DefectSensor) :
887 ∃ (carrier : RegularCarrier),
888 carrier.radius = sensor.realPart - 1/2 ∧
889 0 < carrier.radius := by
890 exact ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
891 euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1,
892 by
893 change 0 < sensor.realPart - 1 / 2
894 linarith [sensor.in_strip.1]⟩
895
896/-! ### §9. The full instantiation certificate -/
897
898/-- **Euler Instantiation Certificate.**
899 Packages the complete chain:
900 Euler product → carrier convergent → nonvanishing → derivative bounded
901 → abstract interface satisfied → cost-covering applicable. -/
902structure EulerInstantiationCert where
903 /-- The carrier converges on Re(s) > 1/2. -/
904 carrier_convergent : ∀ σ, 1/2 < σ → Summable (fun (p : Nat.Primes) => det2LogFactor p σ)
905 /-- The carrier is nonvanishing. -/
906 carrier_nonzero : ∀ σ, 1/2 < σ → carrierValue σ ≠ 0
907 /-- The logarithmic derivative is bounded. -/
908 deriv_bounded : ∀ σ, 1/2 < σ → 0 < carrierDerivBound σ
909 /-- For any hypothetical zero, a compatible RegularCarrier exists. -/
910 compatible : ∀ (sensor : DefectSensor),
911 ∃ (carrier : RegularCarrier), carrier.radius = sensor.realPart - 1/2
912
913/-- The Euler instantiation certificate is verified. -/
914@[simp] def EulerInstantiationCert.verified (cert : EulerInstantiationCert) : Prop :=
915 (∀ σ, 1/2 < σ → carrierValue σ ≠ 0) ∧
916 (∀ σ, 1/2 < σ → 0 < carrierDerivBound σ) ∧
917 (∀ (sensor : DefectSensor),
918 ∃ (carrier : RegularCarrier), carrier.radius = sensor.realPart - 1/2)
919
920/-- Construct the verified certificate from the proved results. -/
921noncomputable def mkEulerInstantiationCert : EulerInstantiationCert where
922 carrier_convergent := fun σ hσ => det2_product_convergent hσ
923 carrier_nonzero := fun σ hσ => carrier_nonvanishing hσ
924 deriv_bounded := fun σ hσ => carrierDerivBound_pos hσ
925 compatible := fun sensor =>
926 ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
927 euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1⟩
928
929/-! ### §10. Connecting to the conditional RH -/
930
931/-- The full chain: Euler product instantiation + explicit cost-covering package
932 implies no zeros with Re(s) > 1/2.
933
934 This theorem connects the concrete number theory (this file)
935 to the abstract conditional RH (CostCoveringBridge.lean). -/
936theorem euler_rh_conditional (pkg : CostCoveringPackage)
937 (hcover : ∀ sensor : DefectSensor, DefectTopologicalFloorCovered pkg sensor)
938 (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : False :=
939 rh_from_cost_covering pkg sensor hm (hcover sensor)
940
941/-- The complete RH conditional on RS, given an explicit cost-covering package
942 and topological-floor coverage. -/
943theorem riemann_hypothesis_euler_conditional (pkg : CostCoveringPackage)
944 (hcover : ∀ sensor : DefectSensor, DefectTopologicalFloorCovered pkg sensor) :
945 ∀ (σ₀ : ℝ) (hσ : 1/2 < σ₀) (hσ1 : σ₀ < 1) (m : ℤ) (hm : m ≠ 0),
946 let sensor : DefectSensor := ⟨m, σ₀, ⟨hσ, hσ1⟩⟩
947 False :=
948 fun σ₀ hσ hσ1 m hm => euler_rh_conditional pkg hcover ⟨m, σ₀, ⟨hσ, hσ1⟩⟩ hm
949
950/-! ### §11. Sampled-trace Euler carrier (axiom-free) -/
951
952/-- The Euler carrier packaged as a `BudgetedCarrier` using the sampled-trace
953infrastructure from `SampledTrace.lean`. This uses the zero-winding certificate
954from `EulerCarrierComplex.lean` instead of a synthetic zero-charge trace.
955
956The key difference from `eulerBudgetedCarrier` is that the zero-winding
957property is derived from the carrier's holomorphy and nonvanishing
958(via `eulerZeroWindingCert`), not assumed. -/
959noncomputable def eulerSampledBudgetedCarrier (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
960 BudgetedCarrier :=
961 SampledTrace.sampledBudgetedCarrier
962 (EulerCarrierComplex.eulerZeroWindingCert σ₀ hσ)
963 (carrierDerivBound σ₀)
964 (carrierDerivBound_pos hσ)
965 (σ₀ - 1/2)
966 (by linarith)
967
968/-- The sampled Euler carrier has budget scale 0. -/
969theorem eulerSampledBudgetedCarrier_scale_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
970 carrierBudgetScale (eulerSampledBudgetedCarrier σ₀ hσ) = 0 := by
971 simp [eulerSampledBudgetedCarrier, SampledTrace.sampledBudgetedCarrier, carrierBudgetScale]
972
973/-- Package the sampled Euler carrier as a `CostCoveringPackage`. -/
974noncomputable def eulerSampledPackage (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
975 CostCoveringPackage where
976 carrier := eulerSampledBudgetedCarrier σ₀ hσ
977
978/-- The sampled package's floor coverage is equivalent to charge = 0. -/
979theorem eulerSampledFloorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
980 (sensor : DefectSensor) :
981 DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor ↔
982 sensor.charge = 0 := by
983 constructor
984 · intro hcover
985 by_contra hm
986 exact not_DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor hm hcover
987 · intro hzero
988 intro N
989 rw [hzero, annularTopologicalFloor_zero]
990 exact carrierBudgetScale_nonneg _
991
992end NumberTheory
993end IndisputableMonolith
994