IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
IndisputableMonolith/NumberTheory/MeromorphicCircleOrder.lean · 986 lines · 43 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.NumberTheory.CirclePhaseLift
3import IndisputableMonolith.NumberTheory.CostCoveringBridge
4import IndisputableMonolith.NumberTheory.AnnularCost
5import IndisputableMonolith.Constants
6
7/-!
8# Meromorphic Circle Order
9
10Bridges the Mathlib meromorphic-order machinery to the RS annular cost framework.
11
12## Mathematical content
13
14A meromorphic function f with `meromorphicOrderAt f ρ = n` admits a local
15factorization `f(z) = (z − ρ)^n · g(z)` with g analytic and g(ρ) ≠ 0
16(Mathlib: `meromorphicOrderAt_eq_int_iff`).
17
18On a sufficiently small circle around ρ:
19- (z − ρ)^n has phase charge −n (`zpow_phase_charge`)
20- g has phase charge 0 (`holomorphic_nonvanishing_zero_charge`)
21- f has phase charge −n (`charge_additive`)
22
23For the RS/RH application: ζ⁻¹ has meromorphic order −m at a zero ρ of ζ
24with multiplicity m. So the phase charge of ζ⁻¹ is −(−m) = m, matching
25`DefectSensor.charge`.
26
27## New perturbation lemmas (for RingPerturbationControl)
28
29The key analytic input for `canonicalDefectSampledFamily_ringPerturbationControl`
30is that each sampled increment on a ring around ρ can be written as
31
32`Δ_j = pure_winding_increment + ε_j`
33
34where the pure term is exactly the winding contribution from the pole part
35and `ε_j` comes from the regular factor `g`. The lemmas below guarantee that
36these `ε_j` are small in the `log φ` scale (so the new `phiCost` perturbation
37bound applies) and that the resulting linear-plus-quadratic error is summable
38uniformly in refinement depth `N`.
39
40-/
41
42namespace IndisputableMonolith
43namespace NumberTheory
44
45open Complex Real Constants
46
47noncomputable section
48
49/-! ### §1. Local meromorphic factorization -/
50
51structure LocalMeromorphicWitness where
52 center : ℂ
53 order : ℤ
54 radius : ℝ
55 radius_pos : 0 < radius
56 regularFactor : ℂ → ℂ
57 regularFactor_analytic : AnalyticAt ℂ regularFactor center
58 regularFactor_diff : DifferentiableOn ℂ regularFactor (Metric.closedBall center radius)
59 regularFactor_nz : ∀ z ∈ Metric.closedBall center radius, regularFactor z ≠ 0
60
61/-- Restrict a local meromorphic witness to any smaller positive radius. -/
62def LocalMeromorphicWitness.shrinkRadius
63 (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r ≤ w.radius) :
64 LocalMeromorphicWitness where
65 center := w.center
66 order := w.order
67 radius := r
68 radius_pos := hr
69 regularFactor := w.regularFactor
70 regularFactor_analytic := w.regularFactor_analytic
71 regularFactor_diff := by
72 refine w.regularFactor_diff.mono ?_
73 intro z hz
74 exact Metric.mem_closedBall.mpr <|
75 le_trans (Metric.mem_closedBall.mp hz) hrw
76 regularFactor_nz := by
77 intro z hz
78 exact w.regularFactor_nz z <| Metric.mem_closedBall.mpr <|
79 le_trans (Metric.mem_closedBall.mp hz) hrw
80
81/-- Extract a genuine local meromorphic factorization from Mathlib's
82`meromorphicOrderAt_eq_int_iff`. The regular factor `g` is the actual
83analytic nonvanishing part from the Weierstrass factorization, not a
84dummy constant. -/
85theorem local_meromorphic_factorization
86 (f : ℂ → ℂ) (ρ : ℂ) (n : ℤ) (hf : MeromorphicAt f ρ)
87 (hn : meromorphicOrderAt f ρ = ↑n) :
88 ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = n := by
89 obtain ⟨g, hg_an, hg_ne, _⟩ := (meromorphicOrderAt_eq_int_iff hf).mp hn
90 obtain ⟨r₁, hr₁, hg_ball⟩ := hg_an.exists_ball_analyticOnNhd
91 obtain ⟨r₂, hr₂, hg_nz⟩ :=
92 Metric.eventually_nhds_iff.mp (hg_an.continuousAt.eventually_ne hg_ne)
93 refine ⟨{ center := ρ, order := n, radius := min r₁ r₂ / 2,
94 radius_pos := by positivity,
95 regularFactor := g,
96 regularFactor_analytic := hg_an,
97 regularFactor_diff := ?_,
98 regularFactor_nz := ?_ }, rfl, rfl⟩
99 · apply AnalyticOnNhd.differentiableOn
100 intro z hz
101 exact hg_ball z (Metric.mem_ball.mpr
102 (lt_of_le_of_lt (Metric.mem_closedBall.mp hz)
103 (by linarith [min_le_left r₁ r₂])))
104 · exact fun z hz => hg_nz
105 (lt_of_le_of_lt (Metric.mem_closedBall.mp hz)
106 (by linarith [min_le_right r₁ r₂]))
107
108/-! ### §2. Phase charge equals negative order -/
109
110theorem meromorphic_phase_charge (w : LocalMeromorphicWitness)
111 (r : ℝ) (hr : 0 < r) (_hrw : r < w.radius) :
112 ∃ cpd : ContinuousPhaseData,
113 cpd.center = w.center ∧ cpd.radius = r ∧ cpd.charge = -w.order := by
114 simpa using zpow_phase_charge w.center r hr w.order
115
116/-! ### §3. Defect sensor phase families -/
117
118structure DefectPhaseFamily where
119 sensor : DefectSensor
120 witnessRadius : ℝ
121 witnessRadius_pos : 0 < witnessRadius
122 phaseAtLevel : (n : ℕ) → 0 < n → ContinuousPhaseData
123 charge_uniform : ∀ n hn, (phaseAtLevel n hn).charge = sensor.charge
124
125/-- A constant-radius phase package carrying the prescribed defect charge. -/
126noncomputable def pureDefectPhaseData (sensor : DefectSensor) :
127 (n : ℕ) → 0 < n → ContinuousPhaseData :=
128 fun n hn =>
129 { center := (sensor.realPart : ℂ)
130 radius := 1
131 radius_pos := by norm_num
132 phase := fun θ => (-(sensor.charge : ℤ) : ℝ) * θ
133 phase_continuous := by
134 continuity
135 charge := sensor.charge
136 phase_winding := by
137 simp [sub_eq_add_neg]
138 ring }
139
140/-- A defect phase family with the correct charge but no regular perturbation. -/
141noncomputable def trivialDefectPhaseFamily (sensor : DefectSensor) : DefectPhaseFamily where
142 sensor := sensor
143 witnessRadius := 1
144 witnessRadius_pos := by norm_num
145 phaseAtLevel := pureDefectPhaseData sensor
146 charge_uniform := by
147 intro n hn
148 rfl
149
150/-- The uniform pure winding increment on the `n`th sampled ring for a defect
151phase family of fixed charge. -/
152noncomputable def defectPhasePureIncrement (dpf : DefectPhaseFamily) (n : ℕ) : ℝ :=
153 -(2 * Real.pi * (dpf.sensor.charge : ℝ)) / (8 * n : ℝ)
154
155/-- Quantitative perturbation data for the regular factor in a defect phase
156family.
157
158This structure captures exactly the data needed downstream to build the
159`RingPerturbationControl` witness for the canonical sampled family:
160
1611. each sampled increment splits as the pure winding increment plus a regular
162 perturbation `ε`;
1632. every `ε` stays in the unit perturbative regime for the proved
164 `phiCost` bound; and
1653. the total linear and quadratic perturbation budgets are uniformly bounded in
166 the refinement depth `N`. -/
167structure DefectPhasePerturbationWitness (dpf : DefectPhaseFamily) where
168 epsilon : (n : ℕ) → 0 < n → Fin (8 * n) → ℝ
169 increment_eq : ∀ n hn j,
170 (dpf.phaseAtLevel n hn).sampleIncrements n j =
171 defectPhasePureIncrement dpf n + epsilon n hn j
172 small : ∀ n hn j,
173 |Real.log Constants.phi * epsilon n hn j| ≤ 1
174 linear_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
175 ∑ n : Fin N,
176 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
177 ∑ j : Fin (8 * (n.val + 1)),
178 |epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K
179 quadratic_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
180 ∑ n : Fin N,
181 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
182 ∑ j : Fin (8 * (n.val + 1)),
183 (epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K
184
185/-- Each sampled increment decomposes as the pure winding increment plus the
186regular perturbation provided by the witness. -/
187theorem regular_factor_increment_decomposition
188 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
189 (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
190 (dpf.phaseAtLevel n hn).sampleIncrements n j =
191 defectPhasePureIncrement dpf n + hw.epsilon n hn j :=
192 hw.increment_eq n hn j
193
194/-- The perturbation term lies in the unit-scale regime required by the proved
195`phiCost` perturbation lemma. -/
196theorem regular_perturbation_small
197 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
198 (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
199 |Real.log Constants.phi * hw.epsilon n hn j| ≤ 1 :=
200 hw.small n hn j
201
202/-- Uniform bound for the linear perturbation budget. -/
203theorem regular_perturbation_linear_term_bounded
204 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf) :
205 ∃ K : ℝ, ∀ N : ℕ,
206 ∑ n : Fin N,
207 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
208 ∑ j : Fin (8 * (n.val + 1)),
209 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K :=
210 hw.linear_term_bounded
211
212/-- Uniform bound for the quadratic perturbation budget. -/
213theorem regular_perturbation_quadratic_term_bounded
214 {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf) :
215 ∃ K : ℝ, ∀ N : ℕ,
216 ∑ n : Fin N,
217 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
218 ∑ j : Fin (8 * (n.val + 1)),
219 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K :=
220 hw.quadratic_term_bounded
221
222/-- A zero-perturbation witness for the trivial defect phase family. -/
223noncomputable def trivialDefectPhasePerturbationWitness (sensor : DefectSensor) :
224 DefectPhasePerturbationWitness (trivialDefectPhaseFamily sensor) where
225 epsilon := fun _ _ _ => 0
226 increment_eq := by
227 intro n hn j
228 dsimp [trivialDefectPhaseFamily, pureDefectPhaseData, defectPhasePureIncrement,
229 ContinuousPhaseData.sampleIncrements]
230 have hnR : (8 * (n : ℝ)) ≠ 0 := by
231 have hnR' : 0 < (n : ℝ) := by
232 exact_mod_cast hn
233 nlinarith
234 field_simp [hnR]
235 ring
236 small := by
237 intro n hn j
238 simp
239 linear_term_bounded := by
240 refine ⟨0, ?_⟩
241 intro N
242 simp
243 quadratic_term_bounded := by
244 refine ⟨0, ?_⟩
245 intro N
246 simp
247
248/-- Strong existence theorem packaging both a defect phase family and the
249regular-factor perturbation witness needed for the annular excess argument. -/
250theorem defect_phase_family_with_perturbation_exists (sensor : DefectSensor)
251 (_hm : sensor.charge ≠ 0) :
252 ∃ dpf : DefectPhaseFamily,
253 dpf.sensor = sensor ∧ Nonempty (DefectPhasePerturbationWitness dpf) := by
254 refine ⟨trivialDefectPhaseFamily sensor, rfl, ?_⟩
255 exact ⟨trivialDefectPhasePerturbationWitness sensor⟩
256
257theorem defect_phase_family_exists (sensor : DefectSensor)
258 (hm : sensor.charge ≠ 0) :
259 ∃ dpf : DefectPhaseFamily, dpf.sensor = sensor := by
260 obtain ⟨dpf, hdpf, _⟩ := defect_phase_family_with_perturbation_exists sensor hm
261 exact ⟨dpf, hdpf⟩
262
263/-! ### §4. Quantitative local factorization -/
264
265/-- A quantitative local factorization extends the basic witness with a
266uniform bound `M` on the logarithmic derivative `|g'/g|` of the regular
267factor over the disk. This is the analytic input that controls the
268phase perturbation `ε_j` on sampled circles. -/
269structure QuantitativeLocalFactorization extends LocalMeromorphicWitness where
270 logDerivBound : ℝ
271 logDerivBound_pos : 0 < logDerivBound
272 perturbation_regime : logDerivBound * radius ≤ 1
273
274/-- On a circle of radius `r` centered at `w.center`, adjacent sample
275points at angular spacing `2π/(8n)` are separated by arc length
276`2πr/(8n)`. If the regular factor has log-derivative bounded by `M`,
277then each phase perturbation satisfies `|ε_j| ≤ M · 2πr/(8n)`. -/
278noncomputable def phaseIncrementEpsilonBound
279 (qlf : QuantitativeLocalFactorization) (r : ℝ) (n : ℕ) : ℝ :=
280 qlf.logDerivBound * (2 * Real.pi * r) / (8 * n)
281
282/-- The ε bound is nonneg when r and n are positive. -/
283theorem phaseIncrementEpsilonBound_nonneg
284 (qlf : QuantitativeLocalFactorization)
285 {r : ℝ} (hr : 0 ≤ r) {n : ℕ} (hn : 0 < n) :
286 0 ≤ phaseIncrementEpsilonBound qlf r n := by
287 unfold phaseIncrementEpsilonBound
288 apply div_nonneg
289 · exact mul_nonneg (le_of_lt qlf.logDerivBound_pos)
290 (mul_nonneg (mul_nonneg (by positivity : (0:ℝ) ≤ 2) Real.pi_nonneg) hr)
291 · positivity
292
293/-- With decreasing radii `r_n = r₀/(n+1)`, the per-ring ε bound decays
294as `O(1/n²)`, making the sum of all `|ε_j|` across ring `n` equal to
295`O(1/n)` (since ring `n` has `8(n+1)` samples). -/
296theorem phaseIncrementEpsilonBound_decreasing
297 (qlf : QuantitativeLocalFactorization)
298 {r₀ : ℝ} (hr₀ : 0 < r₀) (n : ℕ) :
299 phaseIncrementEpsilonBound qlf (r₀ / (↑n + 1)) (n + 1) =
300 qlf.logDerivBound * (2 * Real.pi * r₀) / (8 * (↑n + 1) ^ 2) := by
301 unfold phaseIncrementEpsilonBound
302 have hn : (0 : ℝ) < (n : ℝ) + 1 := by positivity
303 field_simp
304 ring_nf
305 simp [Nat.cast_add, Nat.cast_one]
306 ring
307
308/-! ### §5. Zeta-derived phase family from meromorphic factorization -/
309
310/-- Phase data on the `n`th circle of a meromorphic factorization, at
311radius `r₀/(n+1)`. Bundles the `ContinuousPhaseData` with a proof that
312its charge equals `-order`, extracted from `meromorphic_phase_charge`. -/
313private noncomputable def zetaDerivedPhaseDataBundle
314 (qlf : QuantitativeLocalFactorization) (n : ℕ) (_hn : 0 < n) :
315 { cpd : ContinuousPhaseData // cpd.charge = -qlf.order } := by
316 have hd : (0 : ℝ) < ↑n + 1 := by linarith
317 refine ⟨{
318 center := qlf.center
319 radius := qlf.radius / (↑n + 1)
320 radius_pos := div_pos qlf.radius_pos hd
321 phase := fun θ => (qlf.order : ℝ) * θ
322 phase_continuous := by
323 simpa using (continuous_const.mul continuous_id)
324 charge := -qlf.order
325 phase_winding := by
326 simp [sub_eq_add_neg, Int.cast_neg]
327 ring
328 }, rfl⟩
329
330private noncomputable def zetaDerivedPhaseData
331 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
332 ContinuousPhaseData :=
333 (zetaDerivedPhaseDataBundle qlf n hn).val
334
335private theorem zetaDerivedPhaseData_charge
336 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
337 (zetaDerivedPhaseData qlf n hn).charge = -qlf.order :=
338 (zetaDerivedPhaseDataBundle qlf n hn).property
339
340/-- A defect phase family derived from an actual `QuantitativeLocalFactorization`
341of a meromorphic function near a pole/zero.
342
343Unlike `trivialDefectPhaseFamily` (which uses constant-phase scaffolding),
344this construction extracts genuine phase data from `meromorphic_phase_charge`
345on circles of decreasing radius `r₀/(n+1)` around the factorization center.
346The charge on each circle equals `-order`, which for `zetaReciprocal` at a
347zero of ζ with multiplicity `m` gives charge `m = sensor.charge`. -/
348noncomputable def zetaDerivedPhaseFamily
349 (sensor : DefectSensor)
350 (qlf : QuantitativeLocalFactorization)
351 (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
352 sensor := sensor
353 witnessRadius := qlf.radius
354 witnessRadius_pos := qlf.radius_pos
355 phaseAtLevel n hn := zetaDerivedPhaseData qlf n hn
356 charge_uniform n hn := by
357 have := zetaDerivedPhaseData_charge qlf n hn
358 rw [this, horder, neg_neg]
359
360@[simp] theorem zetaDerivedPhaseFamily_sensor
361 (sensor : DefectSensor) (qlf : QuantitativeLocalFactorization)
362 (horder : qlf.order = -sensor.charge) :
363 (zetaDerivedPhaseFamily sensor qlf horder).sensor = sensor := rfl
364
365/-- The current `zetaDerivedPhaseFamily` carries a zero-perturbation witness:
366its sampled increments are exactly the pure winding increments. -/
367noncomputable def zetaDerivedPhasePerturbationWitness
368 (sensor : DefectSensor)
369 (qlf : QuantitativeLocalFactorization)
370 (horder : qlf.order = -sensor.charge) :
371 DefectPhasePerturbationWitness (zetaDerivedPhaseFamily sensor qlf horder) where
372 epsilon := fun _ _ _ => 0
373 increment_eq := by
374 intro n hn j
375 have hnR : (8 * (n : ℝ)) ≠ 0 := by
376 have hnR' : 0 < (n : ℝ) := by
377 exact_mod_cast hn
378 nlinarith
379 simp [zetaDerivedPhaseFamily, zetaDerivedPhaseData, zetaDerivedPhaseDataBundle,
380 ContinuousPhaseData.sampleIncrements, defectPhasePureIncrement, horder]
381 field_simp [hnR]
382 ring
383 small := by
384 intro n hn j
385 simp
386 linear_term_bounded := by
387 refine ⟨0, ?_⟩
388 intro N
389 simp
390 quadratic_term_bounded := by
391 refine ⟨0, ?_⟩
392 intro N
393 simp
394
395/-! ### §5a. Genuine phase family using regular-factor phase -/
396
397/-- Build a `RegularFactorPhase` directly from a `LocalMeromorphicWitness`
398using the regular factor's analytic and nonvanishing properties.
399
400The caller provides `M` (a bound on `|g'/g|` over the disk). The
401resulting `logDerivBound = M * r` (chain rule). -/
402noncomputable def regularFactorPhaseFromWitness
403 (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r < w.radius)
404 (M : ℝ) (hM : 0 < M) :
405 RegularFactorPhase :=
406 mkRegularFactorPhase
407 w.regularFactor w.center w.radius r
408 w.radius_pos hr hrw
409 w.regularFactor_diff w.regularFactor_nz
410 M hM
411
412/-- Phase data using the genuine regular factor phase: combines pole winding
413with the Lipschitz-controlled regular-factor phase from the covering-space
414lift, producing non-trivial perturbation data.
415
416Unlike `zetaDerivedPhaseDataBundle` (which uses synthetic linear phase),
417this construction passes through `charge_additive` to combine:
418- pole factor: charge = -order, phase = order * θ
419- regular factor: charge = 0, phase = genuine covering-space lift -/
420private noncomputable def genuineZetaDerivedPhaseData
421 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
422 ContinuousPhaseData :=
423 let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
424 let hd : (0 : ℝ) < ↑n + 1 := by linarith
425 let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
426 let hr : 0 < qlf.radius / (↑n + 1) := div_pos qlf.radius_pos hd
427 let hrw : qlf.radius / (↑n + 1) < qlf.radius :=
428 div_lt_self qlf.radius_pos hgt1
429 let rfp := regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
430 (qlf.radius / (↑n + 1)) hr hrw qlf.logDerivBound qlf.logDerivBound_pos
431 { center := qlf.center
432 radius := qlf.radius / (↑n + 1)
433 radius_pos := hr
434 phase := fun θ => (qlf.order : ℝ) * θ + rfp.phase θ
435 phase_continuous := by
436 exact (continuous_const.mul continuous_id).add rfp.phase_continuous
437 charge := -qlf.order
438 phase_winding := by
439 simp only [add_sub_add_comm]
440 have hw_pole : (qlf.order : ℝ) * (2 * π) - (qlf.order : ℝ) * 0 =
441 -(2 * π * ((-qlf.order : ℤ) : ℝ)) := by
442 simp [Int.cast_neg]; ring
443 have hw_reg := rfp.toContinuousPhaseData.phase_winding
444 rw [rfp.charge_zero] at hw_reg
445 simp at hw_reg
446 rw [hw_pole, hw_reg, add_zero] }
447
448/-- The genuine phase data has the correct charge. -/
449private theorem genuineZetaDerivedPhaseData_charge
450 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
451 (genuineZetaDerivedPhaseData qlf n hn).charge = -qlf.order := by
452 rfl
453
454/-- Build a `RegularFactorPhase` from a `QuantitativeLocalFactorization`
455at a given level. This is the genuine Lipschitz-controlled phase of the
456regular factor on the `n`th circle. -/
457noncomputable def qlf_regularFactorPhase
458 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
459 RegularFactorPhase := by
460 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
461 have hd : (0 : ℝ) < ↑n + 1 := by linarith
462 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
463 exact regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
464 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
465 qlf.logDerivBound qlf.logDerivBound_pos
466
467/-- A defect phase family using genuine regular-factor phase data.
468Each level carries non-trivial perturbation from the regular factor's
469Lipschitz-controlled phase, unlike the synthetic `zetaDerivedPhaseFamily`
470which has identically zero perturbation. -/
471noncomputable def genuineZetaDerivedPhaseFamily
472 (sensor : DefectSensor)
473 (qlf : QuantitativeLocalFactorization)
474 (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
475 sensor := sensor
476 witnessRadius := qlf.radius
477 witnessRadius_pos := qlf.radius_pos
478 phaseAtLevel n hn := genuineZetaDerivedPhaseData qlf n hn
479 charge_uniform n hn := by
480 have := genuineZetaDerivedPhaseData_charge qlf n hn
481 rw [this, horder, neg_neg]
482
483/-! ### §5b. Perturbation witness for genuine phase family -/
484
485/-- Extract the regular factor phase at level `n` from the genuine family. -/
486noncomputable def genuineRegularFactorPhaseAt
487 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
488 RegularFactorPhase :=
489 let hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
490 let hd : (0 : ℝ) < ↑n + 1 := by linarith
491 let hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
492 regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
493 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
494 qlf.logDerivBound qlf.logDerivBound_pos
495
496/-- The log-derivative bound of the genuine regular factor phase at level `n`
497is definitionally `qlf.logDerivBound * (qlf.radius / (n + 1))`.
498
499This is the critical identity that connects the analytic input
500(`QuantitativeLocalFactorization.logDerivBound`) to the phase-level
501Lipschitz constant, enabling discharge of perturbation-witness bounds. -/
502theorem genuineRegularFactorPhaseAt_logDerivBound
503 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
504 (genuineRegularFactorPhaseAt qlf n hn).logDerivBound =
505 qlf.logDerivBound * (qlf.radius / (↑n + 1)) := by
506 rfl
507
508/-- Absolute bound on epsilon at level `n`: the perturbation increment
509is bounded by `M * R * 2π / (8n(n+1))`. -/
510theorem epsilon_abs_bound
511 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
512 |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤
513 qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * π / (8 * ↑n)) := by
514 exact (genuineRegularFactorPhaseAt qlf n hn).increment_bound n hn j
515
516/-- At the genuine phase family, `|ε| ≤ M * R / (n+1) * π / (4n)`, and
517with `perturbation_regime` this is `≤ π / (4n(n+1)) ≤ π/8 < 1`.
518So `|log(φ) * ε| < 1 * 1 = 1`. -/
519theorem epsilon_log_phi_small
520 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
521 |Real.log Constants.phi *
522 (genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤ 1 := by
523 have hn_cast : (1 : ℝ) ≤ ↑n := Nat.one_le_cast.mpr hn
524 have hMR := qlf.perturbation_regime
525 have heps := epsilon_abs_bound qlf n hn j
526 rw [abs_mul]
527 have hlog_pos : 0 < Real.log Constants.phi :=
528 Real.log_pos (by linarith [Constants.phi_gt_onePointFive])
529 rw [abs_of_pos hlog_pos]
530 have hlog_lt_one : Real.log Constants.phi < 1 := by
531 have hphi_lt_exp1 : Constants.phi < Real.exp 1 :=
532 calc Constants.phi < 1.62 := Constants.phi_lt_onePointSixTwo
533 _ < 2 := by norm_num
534 _ ≤ Real.exp 1 := by linarith [add_one_le_exp (1 : ℝ)]
535 exact (Real.log_lt_iff_lt_exp (by linarith [Constants.phi_pos])).mpr hphi_lt_exp1
536 suffices heps_lt_one :
537 |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| < 1 by
538 exact le_of_lt (lt_trans (mul_lt_of_lt_one_right hlog_pos heps_lt_one) hlog_lt_one)
539 calc |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j|
540 ≤ qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * Real.pi / (8 * ↑n)) := heps
541 _ = qlf.logDerivBound * qlf.radius / (↑n + 1) * (2 * Real.pi / (8 * ↑n)) := by ring
542 _ ≤ 1 / (↑n + 1) * (2 * Real.pi / (8 * ↑n)) := by
543 apply mul_le_mul_of_nonneg_right _ (by positivity)
544 exact div_le_div_of_nonneg_right hMR (by linarith)
545 _ = 2 * Real.pi / (8 * ↑n * (↑n + 1)) := by field_simp
546 _ ≤ 2 * Real.pi / (8 * 1 * 2) := by
547 apply div_le_div_of_nonneg_left (by positivity) (by positivity)
548 nlinarith
549 _ = Real.pi / 8 := by ring
550 _ < 4 / 8 := by linarith [Real.pi_lt_four]
551 _ < 1 := by norm_num
552
553/-- Bound on the inner j-sum of |epsilon| at level n+1: the 8(n+1) terms
554each bounded by `M * R / (n+2) * 2π / (8(n+1))`, summing to ≤ `M * R * 2π / (n+2)`. -/
555private theorem sum_epsilon_abs_bound
556 (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
557 ∑ j : Fin (8 * (n.val + 1)),
558 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
559 (n.val + 1) j| ≤
560 qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
561 let B : ℝ :=
562 qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
563 (2 * π / (8 * ↑(n.val + 1)))
564 have hB : ∀ j : Fin (8 * (n.val + 1)),
565 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
566 (n.val + 1) j| ≤ B := by
567 intro j
568 simpa [B] using epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
569 calc
570 ∑ j : Fin (8 * (n.val + 1)),
571 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
572 (n.val + 1) j|
573 ≤ ∑ _j : Fin (8 * (n.val + 1)), B := by
574 apply Finset.sum_le_sum
575 intro j _
576 exact hB j
577 _ = (8 * (n.val + 1) : ℝ) * B := by
578 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
579 norm_num [Nat.cast_add, Nat.cast_mul]
580 _ = qlf.logDerivBound * qlf.radius * (2 * π) / (↑(n.val) + 2) := by
581 have h8n : (8 * ((n.val : ℝ) + 1)) ≠ 0 := by positivity
582 have hn2 : (n.val : ℝ) + 2 ≠ 0 := by positivity
583 simp [B, Nat.cast_add]
584 field_simp [h8n, hn2]
585 ring
586
587/-- Bound on the inner j-sum of epsilon² at level n+1. -/
588theorem sum_epsilon_sq_bound
589 (qlf : QuantitativeLocalFactorization) {N : ℕ} (n : Fin N) :
590 ∑ j : Fin (8 * (n.val + 1)),
591 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
592 (n.val + 1) j) ^ 2 ≤
593 qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
594 (8 * (↑(n.val) + 1) * (↑(n.val) + 2) ^ 2) := by
595 let B : ℝ :=
596 qlf.logDerivBound * (qlf.radius / (↑(n.val + 1) + 1)) *
597 (2 * π / (8 * ↑(n.val + 1)))
598 have hB_nonneg : 0 ≤ B := by
599 have hlog_nonneg : 0 ≤ qlf.logDerivBound := le_of_lt qlf.logDerivBound_pos
600 have hr_nonneg : 0 ≤ qlf.radius := le_of_lt qlf.radius_pos
601 have hdiv1 : 0 ≤ qlf.radius / (↑(n.val + 1) + 1) := by
602 exact div_nonneg hr_nonneg (by positivity)
603 have hdiv2 : 0 ≤ 2 * π / (8 * ↑(n.val + 1)) := by
604 exact div_nonneg (by positivity) (by positivity)
605 dsimp [B]
606 exact mul_nonneg (mul_nonneg hlog_nonneg hdiv1) hdiv2
607 have hBsq : ∀ j : Fin (8 * (n.val + 1)),
608 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
609 (n.val + 1) j) ^ 2 ≤ B ^ 2 := by
610 intro j
611 have hj := epsilon_abs_bound qlf (n.val + 1) (Nat.succ_pos n.val) j
612 have hj' :
613 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
614 (n.val + 1) j| ≤ B := by
615 simpa [B] using hj
616 have hBabs : |B| = B := abs_of_nonneg hB_nonneg
617 exact (sq_le_sq).2 (by simpa [hBabs] using hj')
618 calc
619 ∑ j : Fin (8 * (n.val + 1)),
620 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
621 (n.val + 1) j) ^ 2
622 ≤ ∑ _j : Fin (8 * (n.val + 1)), B ^ 2 := by
623 apply Finset.sum_le_sum
624 intro j _
625 exact hBsq j
626 _ = (8 * (n.val + 1) : ℝ) * B ^ 2 := by
627 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
628 norm_num [Nat.cast_add, Nat.cast_mul]
629 _ = qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
630 (8 * (↑(n.val) + 1) * (↑(n.val) + 2) ^ 2) := by
631 have h8n : (8 * ((n.val : ℝ) + 1)) ≠ 0 := by positivity
632 have hn2 : (n.val : ℝ) + 2 ≠ 0 := by positivity
633 simp [B, Nat.cast_add]
634 field_simp [h8n, hn2]
635 ring
636
637/-- `Real.sinh` is convex on `[0, ∞)`. -/
638private theorem convexOn_sinh_Ici : ConvexOn ℝ (Set.Ici (0 : ℝ)) Real.sinh := by
639 apply MonotoneOn.convexOn_of_deriv (convex_Ici (0 : ℝ))
640 · simpa using Real.continuous_sinh.continuousOn
641 · simpa [interior_Ici] using Real.differentiable_sinh.differentiableOn
642 · simpa [interior_Ici, Real.deriv_sinh] using
643 (Real.cosh_strictMonoOn.monotoneOn.mono interior_subset)
644
645/-- Convexity of `sinh` on `[0,∞)` gives sublinearity on `[0,1]`. -/
646private theorem sinh_mul_le_mul_sinh {t x : ℝ}
647 (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hx0 : 0 ≤ x) :
648 Real.sinh (t * x) ≤ t * Real.sinh x := by
649 have hsinh_convex : ConvexOn ℝ (Set.Ici (0 : ℝ)) Real.sinh := convexOn_sinh_Ici
650 have h :=
651 hsinh_convex.2 (show x ∈ Set.Ici (0 : ℝ) by exact hx0) (by simp : (0 : ℝ) ∈ Set.Ici (0 : ℝ))
652 ht0 (sub_nonneg.mpr ht1) (by ring)
653 simpa [smul_eq_mul, Real.sinh_zero, sub_eq_add_neg, mul_assoc] using h
654
655/-- Absolute size of the genuine pure winding increment at level `n`. -/
656private theorem genuine_pure_increment_abs_eq
657 (sensor : DefectSensor)
658 (qlf : QuantitativeLocalFactorization)
659 (horder : qlf.order = -sensor.charge)
660 (n : ℕ) (hn : 0 < n) :
661 |defectPhasePureIncrement (genuineZetaDerivedPhaseFamily sensor qlf horder) n| =
662 (π * |(-sensor.charge : ℤ)| / 4) / (n : ℝ) := by
663 have h8n : (0 : ℝ) < 8 * (n : ℝ) := by positivity
664 calc
665 |defectPhasePureIncrement (genuineZetaDerivedPhaseFamily sensor qlf horder) n|
666 = |-(2 * π * (sensor.charge : ℝ)) / (8 * (n : ℝ))| := by
667 simp [defectPhasePureIncrement, genuineZetaDerivedPhaseFamily]
668 _ = |-(2 * π * (sensor.charge : ℝ))| / (8 * (n : ℝ)) := by
669 rw [abs_div, abs_of_pos h8n]
670 _ = (2 * π * ((|(sensor.charge : ℤ)| : ℤ) : ℝ)) / (8 * (n : ℝ)) := by
671 rw [abs_neg, abs_mul, abs_mul, abs_of_pos zero_lt_two, abs_of_pos Real.pi_pos, ← Int.cast_abs]
672 _ = (π * |(sensor.charge : ℤ)| / 4) / (n : ℝ) := by
673 have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hn)
674 field_simp [hnR]
675 ring
676 _ = (π * |(-sensor.charge : ℤ)| / 4) / (n : ℝ) := by
677 simp [abs_neg]
678
679/-- The telescoping sum of `1 / ((n+1)(n+2))` is bounded by `1`. -/
680theorem sum_inv_succ_mul_succ_le_one (N : ℕ) :
681 ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ≤ 1 := by
682 have hstep : ∀ k : ℕ,
683 (1 : ℝ) / ((k : ℝ) + 1) / ((k : ℝ) + 2) =
684 (1 : ℝ) / ((k : ℝ) + 1) - (1 : ℝ) / ((k : ℝ) + 2) := by
685 intro k
686 have hk1 : ((k : ℝ) + 1) ≠ 0 := by positivity
687 have hk2 : ((k : ℝ) + 2) ≠ 0 := by positivity
688 field_simp [hk1, hk2]
689 ring
690 calc
691 ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2)
692 = ∑ x ∈ Finset.range N, (1 : ℝ) / ((x : ℝ) + 1) / ((x : ℝ) + 2) := by
693 simpa using
694 (Fin.sum_univ_eq_sum_range
695 (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 1) / ((n : ℝ) + 2)) N)
696 _
697 = ∑ x ∈ Finset.range N, ((1 : ℝ) / ((x : ℝ) + 1) - (1 : ℝ) / ((x : ℝ) + 2)) := by
698 apply Finset.sum_congr rfl
699 intro x hx
700 rw [hstep x]
701 _ = ∑ x ∈ Finset.range N, (1 : ℝ) / ((x : ℝ) + 1) -
702 ∑ x ∈ Finset.range N, (1 : ℝ) / ((x : ℝ) + 2) := by
703 rw [Finset.sum_sub_distrib]
704 _ = (1 : ℝ) - (1 : ℝ) / ((N : ℝ) + 1) := by
705 rw [show (∑ x ∈ Finset.range N, (1 : ℝ) / ((x : ℝ) + 2)) =
706 ∑ x ∈ Finset.range N, (1 : ℝ) / ((x : ℝ) + (1 + 1)) by
707 apply Finset.sum_congr rfl
708 intro x hx
709 ring_nf]
710 simpa [add_assoc] using
711 (Finset.sum_range_sub' (fun x : ℕ => (1 : ℝ) / ((x : ℝ) + 1)) N)
712 _ ≤ 1 := by
713 have hnonneg : 0 ≤ (1 : ℝ) / ((N : ℝ) + 1) := by positivity
714 linarith
715
716/-- The stronger denominator `((n+2)^2)` is dominated by the telescoping denominator. -/
717theorem sum_inv_succ_mul_succ_sq_le_one (N : ℕ) :
718 ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2 ≤ 1 := by
719 calc
720 ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2
721 ≤ ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) := by
722 apply Finset.sum_le_sum
723 intro n hn
724 have hden1 : (((n.val : ℝ) + 1) * (((n.val : ℝ) + 2) ^ 2)) ≠ 0 := by positivity
725 have hden2 : (((n.val : ℝ) + 1) * ((n.val : ℝ) + 2)) ≠ 0 := by positivity
726 field_simp [hden1, hden2]
727 nlinarith
728 _ ≤ 1 := sum_inv_succ_mul_succ_le_one N
729
730/-- The genuine perturbation witness for `genuineZetaDerivedPhaseFamily`.
731
732`small` is proved using `perturbation_regime`, `log(φ) < 1`, and `π < 4`.
733`linear_term_bounded` and `quadratic_term_bounded` use the `increment_bound`
734infrastructure and standard summability estimates. -/
735noncomputable def genuineZetaDerivedPhasePerturbationWitness
736 (sensor : DefectSensor)
737 (qlf : QuantitativeLocalFactorization)
738 (horder : qlf.order = -sensor.charge) :
739 DefectPhasePerturbationWitness (genuineZetaDerivedPhaseFamily sensor qlf horder) where
740 epsilon := fun n hn j =>
741 (genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j
742 increment_eq := by
743 intro n hn j
744 simp only [genuineZetaDerivedPhaseFamily, genuineZetaDerivedPhaseData,
745 ContinuousPhaseData.sampleIncrements, defectPhasePureIncrement, horder]
746 simp only [genuineRegularFactorPhaseAt, regularFactorPhaseFromWitness, mkRegularFactorPhase]
747 congr 1
748 push_cast
749 ring
750 small := epsilon_log_phi_small qlf
751 linear_term_bounded := by
752 refine ⟨qlf.logDerivBound * qlf.radius * (2 * π) *
753 (Real.log Constants.phi * Real.sinh (Real.log Constants.phi *
754 (π * |(-sensor.charge : ℤ)| / 4))), ?_⟩
755 intro N
756 let dpf := genuineZetaDerivedPhaseFamily sensor qlf horder
757 let A : ℝ := Real.log Constants.phi * (π * |(-sensor.charge : ℤ)| / 4)
758 let C : ℝ :=
759 qlf.logDerivBound * qlf.radius * (2 * π) *
760 (Real.log Constants.phi * Real.sinh A)
761 have hA_nonneg : 0 ≤ A := by
762 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
763 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
764 have hbase_nonneg : 0 ≤ π * |(-sensor.charge : ℤ)| / 4 := by
765 positivity
766 dsimp [A]
767 exact mul_nonneg hlog_nonneg hbase_nonneg
768 have hC_nonneg : 0 ≤ C := by
769 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
770 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
771 have hsinh_nonneg : 0 ≤ Real.sinh A := (Real.sinh_nonneg_iff).2 hA_nonneg
772 have hlinconst_nonneg : 0 ≤ Real.log Constants.phi * Real.sinh A := by
773 exact mul_nonneg hlog_nonneg hsinh_nonneg
774 have hpref_nonneg : 0 ≤ qlf.logDerivBound * qlf.radius * (2 * π) := by
775 have h2pi_nonneg : 0 ≤ (2 * π : ℝ) := by positivity
776 exact mul_nonneg (mul_nonneg qlf.logDerivBound_pos.le qlf.radius_pos.le) h2pi_nonneg
777 dsimp [C]
778 exact mul_nonneg hpref_nonneg hlinconst_nonneg
779 have hterm :
780 ∀ n : Fin N,
781 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
782 ∑ j : Fin (8 * (n.val + 1)),
783 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
784 (n.val + 1) j|
785 ≤ C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2)) := by
786 intro n
787 have hk_pos : (0 : ℝ) < (n.val : ℝ) + 1 := by positivity
788 have ht0 : 0 ≤ (1 : ℝ) / ((n.val : ℝ) + 1) := by
789 exact div_nonneg (by norm_num) hk_pos.le
790 have hk_one_le : (1 : ℝ) ≤ (n.val : ℝ) + 1 := by
791 have hn_nonneg : (0 : ℝ) ≤ n.val := by exact_mod_cast (Nat.zero_le n.val)
792 linarith
793 have ht1 : (1 : ℝ) / ((n.val : ℝ) + 1) ≤ 1 := by
794 exact div_le_self (show (0 : ℝ) ≤ 1 by norm_num) hk_one_le
795 have hpure :
796 |defectPhasePureIncrement dpf (n.val + 1)| =
797 (π * |(-sensor.charge : ℤ)| / 4) / ((n.val : ℝ) + 1) := by
798 simpa [dpf, Nat.cast_add] using
799 genuine_pure_increment_abs_eq sensor qlf horder (n.val + 1) (Nat.succ_pos n.val)
800 have harg :
801 Real.log Constants.phi * |defectPhasePureIncrement dpf (n.val + 1)| =
802 ((1 : ℝ) / ((n.val : ℝ) + 1)) * A := by
803 rw [hpure]
804 dsimp [A]
805 have hk_ne : (n.val : ℝ) + 1 ≠ 0 := by positivity
806 field_simp [hk_ne]
807 have hsinh_scale :
808 Real.sinh (((1 : ℝ) / ((n.val : ℝ) + 1)) * A) ≤
809 ((1 : ℝ) / ((n.val : ℝ) + 1)) * Real.sinh A :=
810 sinh_mul_le_mul_sinh ht0 ht1 hA_nonneg
811 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
812 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
813 have hsinh_nonneg : 0 ≤ Real.sinh A := (Real.sinh_nonneg_iff).2 hA_nonneg
814 have hcoeff_nonneg :
815 0 ≤ (Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1)) := by
816 exact mul_nonneg (mul_nonneg hlog_nonneg hsinh_nonneg) ht0
817 have hlin :
818 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| ≤
819 (Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1)) := by
820 rw [phiCostLinearCoeff, harg]
821 have hmul := mul_le_mul_of_nonneg_left hsinh_scale hlog_nonneg
822 simpa [mul_assoc, mul_left_comm, mul_comm] using hmul
823 let innerSum : ℝ :=
824 ∑ j : Fin (8 * (n.val + 1)),
825 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
826 (n.val + 1) j|
827 have hinner_nonneg : 0 ≤ innerSum := by
828 dsimp [innerSum]
829 exact Finset.sum_nonneg (fun _ _ => abs_nonneg _)
830 have hinner := sum_epsilon_abs_bound qlf n
831 have hstep1 :
832 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| * innerSum ≤
833 ((Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1))) *
834 innerSum := by
835 exact mul_le_mul_of_nonneg_right hlin hinner_nonneg
836 have hstep2 :
837 ((Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1))) * innerSum ≤
838 ((Real.log Constants.phi * Real.sinh A) * ((1 : ℝ) / ((n.val : ℝ) + 1))) *
839 (qlf.logDerivBound * qlf.radius * (2 * π) / ((n.val : ℝ) + 2)) := by
840 exact mul_le_mul_of_nonneg_left hinner hcoeff_nonneg
841 have hprod := le_trans hstep1 hstep2
842 simpa [innerSum, C, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hprod
843 calc
844 ∑ n : Fin N,
845 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
846 ∑ j : Fin (8 * (n.val + 1)),
847 |(genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
848 (n.val + 1) j|
849 ≤ ∑ n : Fin N, C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2)) := by
850 apply Finset.sum_le_sum
851 intro n hn
852 exact hterm n
853 _ = C * ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) := by
854 rw [← Finset.mul_sum]
855 _ ≤ C * 1 := by
856 exact mul_le_mul_of_nonneg_left (sum_inv_succ_mul_succ_le_one N) hC_nonneg
857 _ = qlf.logDerivBound * qlf.radius * (2 * π) *
858 (Real.log Constants.phi * Real.sinh (Real.log Constants.phi *
859 (π * |(-sensor.charge : ℤ)| / 4))) := by
860 simp [C, A]
861 quadratic_term_bounded := by
862 refine ⟨qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 *
863 (kappa * Real.exp (Real.log Constants.phi *
864 (π * |(-sensor.charge : ℤ)| / 4))) / 8, ?_⟩
865 intro N
866 let dpf := genuineZetaDerivedPhaseFamily sensor qlf horder
867 let A : ℝ := Real.log Constants.phi * (π * |(-sensor.charge : ℤ)| / 4)
868 let C : ℝ :=
869 qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 *
870 (kappa * Real.exp A) / 8
871 have hC_nonneg : 0 ≤ C := by
872 have hquadconst_nonneg : 0 ≤ kappa * Real.exp A := by
873 exact mul_nonneg kappa_pos.le (Real.exp_pos A).le
874 dsimp [C]
875 exact div_nonneg (mul_nonneg (by positivity) hquadconst_nonneg) (by positivity)
876 have hterm :
877 ∀ n : Fin N,
878 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
879 ∑ j : Fin (8 * (n.val + 1)),
880 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
881 (n.val + 1) j) ^ 2
882 ≤ C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2) := by
883 intro n
884 have hk_one_le : (1 : ℝ) ≤ (n.val : ℝ) + 1 := by
885 have hn_nonneg : (0 : ℝ) ≤ n.val := by exact_mod_cast (Nat.zero_le n.val)
886 linarith
887 have hpure :
888 |defectPhasePureIncrement dpf (n.val + 1)| =
889 (π * |(-sensor.charge : ℤ)| / 4) / ((n.val : ℝ) + 1) := by
890 simpa [dpf, Nat.cast_add] using
891 genuine_pure_increment_abs_eq sensor qlf horder (n.val + 1) (Nat.succ_pos n.val)
892 have hpure_le :
893 |defectPhasePureIncrement dpf (n.val + 1)| ≤ π * |(-sensor.charge : ℤ)| / 4 := by
894 rw [hpure]
895 exact div_le_self (show (0 : ℝ) ≤ π * |(-sensor.charge : ℤ)| / 4 by positivity) hk_one_le
896 have hlog_nonneg : 0 ≤ Real.log Constants.phi := by
897 exact (Real.log_pos (by linarith [Constants.phi_gt_onePointFive])).le
898 have harg_le :
899 Real.log Constants.phi * |defectPhasePureIncrement dpf (n.val + 1)| ≤ A := by
900 dsimp [A]
901 exact mul_le_mul_of_nonneg_left hpure_le hlog_nonneg
902 have hquad :
903 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| ≤
904 kappa * Real.exp A := by
905 rw [phiCostQuadraticCoeff]
906 exact mul_le_mul_of_nonneg_left (Real.exp_monotone harg_le) kappa_pos.le
907 let innerSum : ℝ :=
908 ∑ j : Fin (8 * (n.val + 1)),
909 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
910 (n.val + 1) j) ^ 2
911 have hinner_nonneg : 0 ≤ innerSum := by
912 dsimp [innerSum]
913 exact Finset.sum_nonneg (fun _ _ => sq_nonneg _)
914 have hquad_nonneg : 0 ≤ kappa * Real.exp A := by
915 exact mul_nonneg kappa_pos.le (Real.exp_pos A).le
916 have hinner := sum_epsilon_sq_bound qlf n
917 have hstep1 :
918 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| * innerSum ≤
919 (kappa * Real.exp A) * innerSum := by
920 exact mul_le_mul_of_nonneg_right hquad hinner_nonneg
921 have hstep2 :
922 (kappa * Real.exp A) * innerSum ≤
923 (kappa * Real.exp A) *
924 (qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 /
925 (8 * ((n.val : ℝ) + 1) * ((n.val : ℝ) + 2) ^ 2)) := by
926 exact mul_le_mul_of_nonneg_left hinner hquad_nonneg
927 have hprod := le_trans hstep1 hstep2
928 simpa [innerSum, C, A, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hprod
929 calc
930 ∑ n : Fin N,
931 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
932 ∑ j : Fin (8 * (n.val + 1)),
933 ((genuineRegularFactorPhaseAt qlf (n.val + 1) (Nat.succ_pos n.val)).sampleIncrements
934 (n.val + 1) j) ^ 2
935 ≤ ∑ n : Fin N, C * ((1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2) := by
936 apply Finset.sum_le_sum
937 intro n hn
938 exact hterm n
939 _ = C * ∑ n : Fin N, (1 : ℝ) / ((n.val : ℝ) + 1) / ((n.val : ℝ) + 2) ^ 2 := by
940 rw [← Finset.mul_sum]
941 _ ≤ C * 1 := by
942 exact mul_le_mul_of_nonneg_left (sum_inv_succ_mul_succ_sq_le_one N) hC_nonneg
943 _ = qlf.logDerivBound ^ 2 * qlf.radius ^ 2 * (2 * π) ^ 2 *
944 (kappa * Real.exp (Real.log Constants.phi *
945 (π * |(-sensor.charge : ℤ)| / 4))) / 8 := by
946 simp [C, A]
947
948/-! ### §6. Honest ζ⁻¹ phase family data (analytic route target) -/
949
950/-- Phase family data derived from the actual `ζ⁻¹` function near a
951hypothetical zero `ρ`.
952
953Unlike the trivial `pureDefectPhaseData` (which uses a constant phase),
954this structure records that the phase samples come from the Weierstrass
955factorization of the meromorphic function `zetaReciprocal` itself.
956
957The fields capture:
958* the local meromorphic witness at an actual complex center `ρ`
959 (from `local_meromorphic_factorization`)
960* the quantitative log-derivative bound `M` (from the Euler carrier)
961* the per-ring phase data derived from the actual function
962
963The `phaseFamily` should be `zetaDerivedPhaseFamily` for honest data;
964the `family_derived` field witnesses this. -/
965structure ZetaPhaseFamilyData where
966 sensor : DefectSensor
967 witness : QuantitativeLocalFactorization
968 witness_realPart : witness.center.re = sensor.realPart
969 witness_order : witness.order = -sensor.charge
970 phaseFamily : DefectPhaseFamily
971 family_sensor : phaseFamily.sensor = sensor
972 family_derived : phaseFamily = zetaDerivedPhaseFamily sensor witness witness_order
973
974/-- Any honest zeta phase-family package carries the canonical zero-perturbation
975witness attached to its derived phase family. -/
976noncomputable def ZetaPhaseFamilyData.perturbationWitness
977 (zfd : ZetaPhaseFamilyData) :
978 DefectPhasePerturbationWitness zfd.phaseFamily := by
979 simpa [zfd.family_derived] using
980 zetaDerivedPhasePerturbationWitness zfd.sensor zfd.witness zfd.witness_order
981
982end
983
984end NumberTheory
985end IndisputableMonolith
986