IndisputableMonolith.NumberTheory.HonestPhaseBudgetBridge
IndisputableMonolith/NumberTheory/HonestPhaseBudgetBridge.lean · 249 lines · 9 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.NumberTheory.DefectSampledTrace
3import IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
4
5/-!
6# Honest Phase Budget Bridge
7
8This module packages a concrete kind of extra analytic input beyond pure
9completed-ξ symmetry: a perturbation witness for an actual phase family.
10
11Such a witness does not by itself prove RH, but it is exactly the
12Euler/Hadamard-style quantitative control needed to turn an honest phase family
13into bounded annular excess data on the sampled side.
14-/
15
16namespace IndisputableMonolith
17namespace NumberTheory
18
19noncomputable section
20
21/-- The current `zetaDerivedPhaseFamily` sits exactly on the topological floor:
22its annular excess is identically zero on every mesh depth. -/
23theorem zetaDerivedPhaseFamily_excess_zero
24 (sensor : DefectSensor)
25 (qlf : QuantitativeLocalFactorization)
26 (horder : qlf.order = -sensor.charge)
27 (N : ℕ) :
28 annularExcess ((zetaDerivedPhaseFamily sensor qlf horder).toSampledFamily.mesh N) = 0 := by
29 let dpf := zetaDerivedPhaseFamily sensor qlf horder
30 unfold annularExcess annularCost annularTopologicalFloor
31 rw [sub_eq_zero]
32 apply Finset.sum_congr rfl
33 intro n _
34 have hconst :
35 ∀ j : Fin (8 * (n.val + 1)),
36 (((dpf.toSampledFamily).mesh N).rings n).increments j =
37 -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
38 (8 * (n.val + 1) : ℝ) := by
39 intro j
40 have hinc :
41 (((dpf.toSampledFamily).mesh N).rings n).increments j =
42 defectPhasePureIncrement dpf (n.val + 1) := by
43 simpa [dpf, zetaDerivedPhasePerturbationWitness] using
44 (zetaDerivedPhasePerturbationWitness sensor qlf horder).increment_eq
45 (n.val + 1) (Nat.succ_pos n.val) j
46 have hpure :
47 defectPhasePureIncrement dpf (n.val + 1) =
48 -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
49 (8 * (n.val + 1) : ℝ) := by
50 simp [dpf, defectPhasePureIncrement, DefectPhaseFamily.toSampledFamily,
51 defectAnnularMesh]
52 rw [hinc, hpure]
53 calc
54 ringCost (((dpf.toSampledFamily).mesh N).rings n)
55 = ∑ j : Fin (8 * (n.val + 1)),
56 phiCost (-(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
57 (8 * (n.val + 1) : ℝ)) := by
58 unfold ringCost
59 apply Finset.sum_congr rfl
60 intro j _
61 rw [hconst j]
62 _ = topologicalFloor (n.val + 1) (((dpf.toSampledFamily).mesh N).charge) := by
63 unfold topologicalFloor
64 simp [Finset.sum_const, nsmul_eq_mul]
65
66/-- A perturbation witness for any defect phase family induces the ring-level
67perturbation-control package needed by the annular-cost machinery. -/
68noncomputable def phaseFamily_ringPerturbationControl
69 (dpf : DefectPhaseFamily) (hw : DefectPhasePerturbationWitness dpf) :
70 RingPerturbationControl (dpf.toSampledFamily) := by
71 refine { small := ?_, total_bounded := ?_ }
72 · intro N n j
73 have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) j
74 have hinc :
75 (((dpf.toSampledFamily).mesh N).rings n).increments j =
76 defectPhasePureIncrement dpf (n.val + 1) +
77 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
78 simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
79 ContinuousPhaseData.toAnnularRingSample] using
80 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
81 have hpure :
82 defectPhasePureIncrement dpf (n.val + 1) =
83 -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
84 (8 * (n.val + 1) : ℝ) := by
85 simp [defectPhasePureIncrement, DefectPhaseFamily.toSampledFamily,
86 defectAnnularMesh]
87 rw [hinc, hpure]
88 simpa using hsmall
89 obtain ⟨K₁, hK₁⟩ := regular_perturbation_linear_term_bounded hw
90 obtain ⟨K₂, hK₂⟩ := regular_perturbation_quadratic_term_bounded hw
91 refine ⟨K₁ + K₂, ?_⟩
92 intro N
93 have hterm :
94 ∀ n : Fin N,
95 realizedRingPerturbationError (dpf.toSampledFamily) N n =
96 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
97 ∑ j : Fin (8 * (n.val + 1)),
98 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
99 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
100 ∑ j : Fin (8 * (n.val + 1)),
101 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
102 intro n
103 dsimp [realizedRingPerturbationError]
104 have hpure :
105 defectPhasePureIncrement dpf (n.val + 1) =
106 -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
107 (8 * (n.val + 1) : ℝ) := by
108 simp [defectPhasePureIncrement, DefectPhaseFamily.toSampledFamily,
109 defectAnnularMesh]
110 rw [hpure]
111 have hlinSum :
112 ∑ j : Fin (8 * (n.val + 1)),
113 |(((dpf.toSampledFamily).mesh N).rings n).increments j -
114 (-(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
115 (8 * (n.val + 1) : ℝ))| =
116 ∑ j : Fin (8 * (n.val + 1)),
117 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| := by
118 apply Finset.sum_congr rfl
119 intro j _
120 have hinc :
121 (((dpf.toSampledFamily).mesh N).rings n).increments j =
122 defectPhasePureIncrement dpf (n.val + 1) +
123 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
124 simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
125 ContinuousPhaseData.toAnnularRingSample] using
126 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
127 rw [hinc, hpure]
128 ring_nf
129 have hquadSum :
130 ∑ j : Fin (8 * (n.val + 1)),
131 ((((dpf.toSampledFamily).mesh N).rings n).increments j -
132 (-(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
133 (8 * (n.val + 1) : ℝ))) ^ 2 =
134 ∑ j : Fin (8 * (n.val + 1)),
135 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
136 apply Finset.sum_congr rfl
137 intro j _
138 have hinc :
139 (((dpf.toSampledFamily).mesh N).rings n).increments j =
140 defectPhasePureIncrement dpf (n.val + 1) +
141 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
142 simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
143 ContinuousPhaseData.toAnnularRingSample] using
144 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
145 rw [hinc, hpure]
146 ring_nf
147 rw [hlinSum, hquadSum]
148 calc
149 ∑ n : Fin N, realizedRingPerturbationError (dpf.toSampledFamily) N n
150 = ∑ n : Fin N,
151 (phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
152 ∑ j : Fin (8 * (n.val + 1)),
153 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
154 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
155 ∑ j : Fin (8 * (n.val + 1)),
156 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2) := by
157 apply Finset.sum_congr rfl
158 intro n _
159 exact hterm n
160 _ = (∑ n : Fin N,
161 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
162 ∑ j : Fin (8 * (n.val + 1)),
163 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j|) +
164 ∑ n : Fin N,
165 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
166 ∑ j : Fin (8 * (n.val + 1)),
167 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
168 rw [Finset.sum_add_distrib]
169 _ ≤ K₁ + K₂ := by
170 linarith [hK₁ N, hK₂ N]
171
172/-- Hence a perturbation witness gives bounded annular excess for the sampled
173family attached to that phase family. -/
174theorem phaseFamily_excess_bounded_of_perturbationWitness
175 (dpf : DefectPhaseFamily) (hw : DefectPhasePerturbationWitness dpf) :
176 RealizedDefectAnnularExcessBounded (dpf.toSampledFamily) := by
177 exact realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _
178 (ringRegularErrorBound_of_ringPerturbationControl _
179 (phaseFamily_ringPerturbationControl dpf hw))
180
181/-- Specialization to the honest zeta-derived phase package. This makes the
182missing Euler/Hadamard-style upgrade explicit: a perturbation witness for the
183honest phase family is enough to produce bounded annular excess data. -/
184theorem honestPhaseFamily_excess_bounded_of_perturbationWitness
185 (zfd : ZetaPhaseFamilyData)
186 (hw : DefectPhasePerturbationWitness zfd.phaseFamily) :
187 RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) := by
188 exact phaseFamily_excess_bounded_of_perturbationWitness zfd.phaseFamily hw
189
190/-- The current honest zeta-derived phase package already supplies its canonical
191zero-perturbation witness. -/
192noncomputable def honestPhaseFamily_perturbationWitness
193 (zfd : ZetaPhaseFamilyData) :
194 DefectPhasePerturbationWitness zfd.phaseFamily :=
195 zfd.perturbationWitness
196
197/-- The sampled family attached to honest phase data has zero annular excess on
198every mesh depth. -/
199theorem honestPhaseFamily_excess_zero
200 (zfd : ZetaPhaseFamilyData) (N : ℕ) :
201 annularExcess (zfd.phaseFamily.toSampledFamily.mesh N) = 0 := by
202 simpa [zfd.family_derived] using
203 zetaDerivedPhaseFamily_excess_zero zfd.sensor zfd.witness zfd.witness_order N
204
205/-- Therefore the sampled family attached to the current honest phase package
206has bounded annular excess. The remaining analytic gap is no longer the
207perturbation witness itself, but upgrading this excess control to the charge-zero
208conclusion required by `AnalyticTrace`. -/
209theorem honestPhaseFamily_excess_bounded
210 (zfd : ZetaPhaseFamilyData) :
211 RealizedDefectAnnularExcessBounded (zfd.phaseFamily.toSampledFamily) := by
212 refine ⟨0, ?_⟩
213 intro N
214 rw [honestPhaseFamily_excess_zero zfd N]
215
216/-- If the sampled family attached to honest phase data also has bounded total
217annular cost, then the corresponding sensor charge must vanish. This isolates
218the remaining topological/budget upgrade needed by the analytic route. -/
219theorem honestPhaseFamily_charge_zero_of_costBounded
220 (zfd : ZetaPhaseFamilyData)
221 (hcost : RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily)) :
222 zfd.sensor.charge = 0 := by
223 have hzero :=
224 (realizedDefectCostBounded_iff_charge_zero_and_excessBounded
225 (zfd.phaseFamily.toSampledFamily)).mp hcost
226 simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hzero.1
227
228/-- For the current honest phase package, bounded total cost is equivalent to
229zero charge. The perturbation/excess part is already proved; only the bounded-cost
230upgrade remains genuinely open. -/
231theorem honestPhaseFamily_cost_bounded_iff_charge_zero
232 (zfd : ZetaPhaseFamilyData) :
233 RealizedDefectAnnularCostBounded (zfd.phaseFamily.toSampledFamily) ↔
234 zfd.sensor.charge = 0 := by
235 constructor
236 · intro hcost
237 exact honestPhaseFamily_charge_zero_of_costBounded zfd hcost
238 · intro hzero
239 have hzero' : (zfd.phaseFamily.toSampledFamily).sensor.charge = 0 := by
240 simpa [DefectPhaseFamily.toSampledFamily, zfd.family_sensor] using hzero
241 exact realizedDefectCostBounded_of_charge_zero_and_excessBounded
242 (zfd.phaseFamily.toSampledFamily) hzero'
243 (honestPhaseFamily_excess_bounded zfd)
244
245end
246
247end NumberTheory
248end IndisputableMonolith
249