IndisputableMonolith.NumberTheory.AnnularCost
IndisputableMonolith/NumberTheory/AnnularCost.lean · 656 lines · 43 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Cost
4import IndisputableMonolith.Cost.Convexity
5
6/-!
7# Annular J-Cost Framework
8
9The φ-weighted cost function and annular sampling machinery for the
10RS topological cost-covering bridge.
11
12## Core objects
13
14* `phiCost u` := cosh((log φ)·u) − 1 = J(φ^u)
15* `AnnularSample` := phase increments on concentric rings
16* Jensen-based coercivity: nonzero winding forces Θ(m² log N) cost
17* Carrier budget: holomorphic nonvanishing ⟹ O(R²) annular cost
18
19## Lean certification status
20
21The annular layer is now formalized constructively:
22
23- `phiCost` properties
24- Jensen ring bound
25- ring and annular coercivity
26- harmonic divergence
27- annular topological floor and excess decomposition
28- trace-based carrier-budget interface
29
30What remains conditional is the construction of a concrete trace family for the
31specific analytic carrier together with the matching excess bound.
32-/
33
34namespace IndisputableMonolith
35namespace NumberTheory
36
37open Real Constants Cost
38
39/-! ### §1. The φ-weighted cost function -/
40
41/-- The φ-cost in log-coordinates: f(u) = cosh((log φ)·u) − 1.
42 This equals J(φ^u) by the cosh representation of J. -/
43noncomputable def phiCost (u : ℝ) : ℝ := Real.cosh (Real.log phi * u) - 1
44
45/-- phiCost(0) = 0: zero phase increment has zero cost. -/
46theorem phiCost_zero : phiCost 0 = 0 := by
47 simp [phiCost, Real.cosh_zero]
48
49/-- phiCost is symmetric: f(u) = f(−u). -/
50theorem phiCost_symm (u : ℝ) : phiCost u = phiCost (-u) := by
51 simp [phiCost, Real.cosh_neg, mul_neg]
52
53/-- phiCost is nonneg: f(u) ≥ 0 for all u. -/
54theorem phiCost_nonneg (u : ℝ) : 0 ≤ phiCost u := by
55 unfold phiCost
56 linarith [Real.one_le_cosh (Real.log phi * u)]
57
58/-- The stiffness constant κ = (log φ)². -/
59noncomputable def kappa : ℝ := (Real.log phi) ^ 2
60
61theorem kappa_pos : 0 < kappa := by
62 unfold kappa
63 have hlog_pos : 0 < Real.log phi := Real.log_pos one_lt_phi
64 nlinarith
65
66/-- Quadratic lower bound: f(u) ≥ κ·u²/2.
67 Follows from cosh(t) ≥ 1 + t²/2. -/
68theorem phiCost_quadratic_lb (u : ℝ) :
69 kappa * u ^ 2 / 2 ≤ phiCost u := by
70 unfold kappa phiCost
71 let t : ℝ := Real.log phi * u
72 have ht : Real.log phi * u = t := rfl
73 have hmain_nonneg : 0 ≤ t ^ 2 / 2 := by positivity
74 by_cases htnonneg : 0 ≤ t
75 · have hs : t / 2 ≤ Real.sinh (t / 2) :=
76 (Real.self_le_sinh_iff).2 (by linarith)
77 have hs_sq : (t / 2) ^ 2 ≤ Real.sinh (t / 2) ^ 2 := by
78 nlinarith [hs, sq_nonneg (Real.sinh (t / 2))]
79 have hformula : Real.cosh t - 1 = 2 * Real.sinh (t / 2) ^ 2 := by
80 rw [show t = 2 * (t / 2) by ring, Real.cosh_two_mul, Real.cosh_sq]
81 ring
82 have hbound : t ^ 2 / 2 ≤ Real.cosh t - 1 := by
83 rw [hformula]
84 nlinarith
85 simpa [t, mul_assoc, mul_left_comm, mul_comm, pow_two] using hbound
86 · have hformula_neg : Real.cosh t - 1 = Real.cosh (-t) - 1 := by
87 simp [Real.cosh_neg]
88 have hsq_neg : t ^ 2 / 2 = (-t) ^ 2 / 2 := by ring
89 have hpos_case :
90 (-t) ^ 2 / 2 ≤ Real.cosh (-t) - 1 := by
91 have hs : (-t) / 2 ≤ Real.sinh ((-t) / 2) :=
92 (Real.self_le_sinh_iff).2 (by linarith)
93 have hs_sq : ((-t) / 2) ^ 2 ≤ Real.sinh ((-t) / 2) ^ 2 := by
94 nlinarith [hs, sq_nonneg (Real.sinh ((-t) / 2))]
95 have hformula : Real.cosh (-t) - 1 = 2 * Real.sinh ((-t) / 2) ^ 2 := by
96 rw [show -t = 2 * ((-t) / 2) by ring, Real.cosh_two_mul, Real.cosh_sq]
97 ring
98 rw [hformula]
99 nlinarith
100 have hbound : t ^ 2 / 2 ≤ Real.cosh t - 1 := by
101 rw [hsq_neg, hformula_neg]
102 exact hpos_case
103 simpa [t, mul_assoc, mul_left_comm, mul_comm, pow_two] using hbound
104
105/-- The connection to J: phiCost(u) = Jcost(φ^u) for all u ∈ ℝ.
106 Uses the existing Jlog_as_cosh certificate. -/
107theorem phiCost_eq_Jcost (u : ℝ) :
108 phiCost u = Jcost (phi ^ u) := by
109 rw [show phiCost u = Jlog (Real.log phi * u) by
110 rw [phiCost, Jlog_as_cosh]]
111 rw [Jlog, Real.rpow_def_of_pos phi_pos]
112
113/-- `phiCost` is convex on `ℝ` (as `Jlog` composed with a linear map). -/
114private theorem phiCost_convexOn : ConvexOn ℝ (Set.univ : Set ℝ) phiCost := by
115 let g : ℝ →ₗ[ℝ] ℝ :=
116 { toFun := fun x => Real.log phi * x
117 map_add' := by intro x y; ring
118 map_smul' := by intro a x; simpa [smul_eq_mul, mul_assoc, mul_left_comm, mul_comm] }
119 have hcv : ConvexOn ℝ (Set.univ : Set ℝ) Jlog := StrictConvexOn.convexOn Jlog_strictConvexOn
120 have h :
121 ConvexOn ℝ (g ⁻¹' (Set.univ : Set ℝ)) (Jlog ∘ g) :=
122 hcv.comp_linearMap g
123 convert h using 1 <;> ext x <;> simp [g, phiCost, Function.comp, Jlog_as_cosh]
124
125/-- Linear perturbation coefficient for `phiCost` on `[-A, A]`. -/
126noncomputable def phiCostLinearCoeff (A : ℝ) : ℝ :=
127 Real.log phi * Real.sinh (Real.log phi * A)
128
129/-- Quadratic perturbation coefficient for `phiCost` on `[-A, A]`. -/
130noncomputable def phiCostQuadraticCoeff (A : ℝ) : ℝ :=
131 kappa * Real.exp (Real.log phi * A)
132
133/-- On `|x| ≤ 1`, the exponential remainder is quadratically bounded. -/
134private theorem abs_exp_sub_one_sub_id_le_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
135 |Real.exp x - 1 - x| ≤ x ^ 2 := by
136 simpa [Real.norm_eq_abs, sub_eq_add_neg] using
137 (Real.norm_exp_sub_one_sub_id_le (x := x) (by simpa [Real.norm_eq_abs] using hx))
138
139/-- On `|x| ≤ 1`, `cosh x - 1` is quadratically small. -/
140private theorem cosh_sub_one_le_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
141 Real.cosh x - 1 ≤ x ^ 2 := by
142 let A : ℝ := Real.exp x - 1 - x
143 let B : ℝ := Real.exp (-x) - 1 + x
144 have hA : |A| ≤ x ^ 2 := by
145 dsimp [A]
146 exact abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hx
147 have hB : |B| ≤ x ^ 2 := by
148 have hxneg : |-x| ≤ 1 := by simpa using hx
149 dsimp [B]
150 simpa using abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hxneg
151 have hsum : |A + B| ≤ 2 * x ^ 2 := by
152 calc
153 |A + B| ≤ |A| + |B| := abs_add_le _ _
154 _ ≤ x ^ 2 + x ^ 2 := add_le_add hA hB
155 _ = 2 * x ^ 2 := by ring
156 have hrewrite : A + B = 2 * (Real.cosh x - 1) := by
157 dsimp [A, B]
158 rw [Real.cosh_eq]
159 field_simp [two_ne_zero]
160 ring
161 have hnonneg : 0 ≤ 2 * (Real.cosh x - 1) := by
162 have hcosh : 0 ≤ Real.cosh x - 1 := by
163 linarith [Real.one_le_cosh x]
164 nlinarith
165 have hmain : 2 * (Real.cosh x - 1) ≤ 2 * x ^ 2 := by
166 have : |2 * (Real.cosh x - 1)| ≤ 2 * x ^ 2 := by
167 simpa [hrewrite] using hsum
168 simpa [abs_of_nonneg hnonneg] using this
169 nlinarith
170
171/-- On `|x| ≤ 1`, `sinh x` differs from the identity by at most quadratic size. -/
172private theorem abs_sinh_le_abs_add_sq_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
173 |Real.sinh x| ≤ |x| + x ^ 2 := by
174 let A : ℝ := Real.exp x - 1 - x
175 let B : ℝ := Real.exp (-x) - 1 + x
176 have hA : |A| ≤ x ^ 2 := by
177 dsimp [A]
178 exact abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hx
179 have hB : |B| ≤ x ^ 2 := by
180 have hxneg : |-x| ≤ 1 := by simpa using hx
181 dsimp [B]
182 simpa using abs_exp_sub_one_sub_id_le_sq_of_abs_le_one hxneg
183 have hdecomp : Real.sinh x = x + (A - B) / 2 := by
184 dsimp [A, B]
185 rw [Real.sinh_eq]
186 field_simp [two_ne_zero]
187 ring
188 have hdiv : |(A - B) / 2| ≤ (|A| + |B|) / 2 := by
189 have habs : |A - B| ≤ |A| + |B| := by
190 simpa using (abs_sub_le A 0 B)
191 have htwo : (0 : ℝ) < 2 := by norm_num
192 rw [abs_div, abs_of_pos htwo]
193 exact div_le_div_of_nonneg_right habs htwo.le
194 have hdiv' : |x| + |(A - B) / 2| ≤ |x| + (|A| + |B|) / 2 := by
195 simpa [add_comm, add_left_comm, add_assoc] using add_le_add_right hdiv |x|
196 calc
197 |Real.sinh x| = |x + (A - B) / 2| := by rw [hdecomp]
198 _ ≤ |x| + |(A - B) / 2| := abs_add_le _ _
199 _ ≤ |x| + (|A| + |B|) / 2 := hdiv'
200 _ ≤ |x| + x ^ 2 := by
201 nlinarith [hA, hB]
202
203/-- Perturbative upper bound for `phiCost`.
204
205If `u` lies in the compact interval `[-A, A]` and the perturbation `ε` is small
206enough that `|(log φ) ε| ≤ 1`, then `phiCost (u + ε)` is controlled by the base
207cost `phiCost u` plus a linear and quadratic error in `ε`. This is the basic
208ring-level estimate used to separate the topological floor from the regular-part
209error in sampled annular meshes. -/
210theorem phiCost_add_le_phiCost_add_linear_quadratic
211 {A u ε : ℝ} (hu : |u| ≤ A) (hε : |Real.log phi * ε| ≤ 1) :
212 phiCost (u + ε) ≤
213 phiCost u + phiCostLinearCoeff A * |ε| + phiCostQuadraticCoeff A * ε ^ 2 := by
214 let a : ℝ := Real.log phi
215 let x : ℝ := a * u
216 let y : ℝ := a * ε
217 have ha_pos : 0 < a := by
218 dsimp [a]
219 exact Real.log_pos one_lt_phi
220 have hxA : |x| ≤ a * A := by
221 calc
222 |x| = a * |u| := by
223 dsimp [x]
224 rw [abs_mul, abs_of_nonneg ha_pos.le]
225 _ ≤ a * A := mul_le_mul_of_nonneg_left hu ha_pos.le
226 have hsinh_x : |Real.sinh x| ≤ Real.sinh (a * A) := by
227 rw [Real.abs_sinh]
228 exact (Real.sinh_le_sinh).2 hxA
229 have hcosh_sinh_x : Real.cosh x + |Real.sinh x| ≤ Real.exp (a * A) := by
230 calc
231 Real.cosh x + |Real.sinh x| = Real.exp |x| := by
232 rw [Real.abs_sinh, ← Real.cosh_abs x, Real.cosh_add_sinh]
233 _ ≤ Real.exp (a * A) := Real.exp_le_exp.mpr hxA
234 have hy_bound : |y| ≤ 1 := by
235 simpa [y, a] using hε
236 have hcosh_y : Real.cosh y - 1 ≤ y ^ 2 :=
237 cosh_sub_one_le_sq_of_abs_le_one hy_bound
238 have hsinh_y : |Real.sinh y| ≤ |y| + y ^ 2 :=
239 abs_sinh_le_abs_add_sq_of_abs_le_one hy_bound
240 have hprod_cosh : Real.cosh x * (Real.cosh y - 1) ≤ Real.cosh x * y ^ 2 := by
241 have hcosh_nonneg : 0 ≤ Real.cosh x := by
242 linarith [Real.one_le_cosh x]
243 exact mul_le_mul_of_nonneg_left hcosh_y hcosh_nonneg
244 have hprod_sinh : Real.sinh x * Real.sinh y ≤ |Real.sinh x| * (|y| + y ^ 2) := by
245 have h1 : Real.sinh x * Real.sinh y ≤ |Real.sinh x * Real.sinh y| := le_abs_self _
246 have h2 : |Real.sinh x * Real.sinh y| ≤ |Real.sinh x| * (|y| + y ^ 2) := by
247 rw [abs_mul]
248 exact mul_le_mul_of_nonneg_left hsinh_y (abs_nonneg _)
249 exact h1.trans h2
250 have hexpand :
251 phiCost (u + ε) =
252 phiCost u + (Real.cosh x * (Real.cosh y - 1) + Real.sinh x * Real.sinh y) := by
253 dsimp [x, y, a]
254 unfold phiCost
255 rw [show Real.log phi * (u + ε) = Real.log phi * u + Real.log phi * ε by ring, Real.cosh_add]
256 ring
257 have hmain :
258 phiCost (u + ε) ≤
259 phiCost u + |Real.sinh x| * |y| + (Real.cosh x + |Real.sinh x|) * y ^ 2 := by
260 rw [hexpand]
261 calc
262 phiCost u + (Real.cosh x * (Real.cosh y - 1) + Real.sinh x * Real.sinh y)
263 ≤ phiCost u + (Real.cosh x * y ^ 2 + |Real.sinh x| * (|y| + y ^ 2)) := by
264 nlinarith [hprod_cosh, hprod_sinh]
265 _ = phiCost u + |Real.sinh x| * |y| + (Real.cosh x + |Real.sinh x|) * y ^ 2 := by
266 ring
267 have hy_abs : |y| = a * |ε| := by
268 dsimp [y]
269 rw [abs_mul, abs_of_nonneg ha_pos.le]
270 have hy_sq : y ^ 2 = a ^ 2 * ε ^ 2 := by
271 dsimp [y]
272 ring
273 have hlin :
274 |Real.sinh x| * |y| ≤ phiCostLinearCoeff A * |ε| := by
275 rw [hy_abs, phiCostLinearCoeff]
276 have :=
277 mul_le_mul_of_nonneg_right hsinh_x (mul_nonneg ha_pos.le (abs_nonneg ε))
278 simpa [mul_assoc, mul_left_comm, mul_comm] using this
279 have hquad :
280 (Real.cosh x + |Real.sinh x|) * y ^ 2 ≤ phiCostQuadraticCoeff A * ε ^ 2 := by
281 calc
282 (Real.cosh x + |Real.sinh x|) * y ^ 2 ≤ Real.exp (a * A) * y ^ 2 := by
283 exact mul_le_mul_of_nonneg_right hcosh_sinh_x (sq_nonneg y)
284 _ = Real.exp (a * A) * (a ^ 2 * ε ^ 2) := by
285 rw [hy_sq]
286 _ = phiCostQuadraticCoeff A * ε ^ 2 := by
287 dsimp [phiCostQuadraticCoeff, a, kappa]
288 ring
289 calc
290 phiCost (u + ε)
291 ≤ phiCost u + |Real.sinh x| * |y| + (Real.cosh x + |Real.sinh x|) * y ^ 2 := hmain
292 _ ≤ phiCost u + phiCostLinearCoeff A * |ε| + phiCostQuadraticCoeff A * ε ^ 2 := by
293 nlinarith [hlin, hquad]
294
295/-! ### §2. Annular sampling -/
296
297/-- An annular sample on ring n consists of 8n phase increments
298 with prescribed total winding. -/
299structure AnnularRingSample (n : ℕ) where
300 increments : Fin (8 * n) → ℝ
301 winding : ℤ
302 winding_constraint : ∑ j, increments j = -(2 * Real.pi * winding)
303
304/-- The J-cost of one ring: sum of phiCost over all angular edges. -/
305noncomputable def ringCost {n : ℕ} (s : AnnularRingSample n) : ℝ :=
306 ∑ j, phiCost (s.increments j)
307
308/-- An annular mesh of N concentric rings. -/
309structure AnnularMesh (N : ℕ) where
310 rings : (n : Fin N) → AnnularRingSample (n.val + 1)
311 charge : ℤ
312 uniform_charge : ∀ n, (rings n).winding = charge
313
314/-- Total annular cost over N rings. -/
315noncomputable def annularCost {N : ℕ} (mesh : AnnularMesh N) : ℝ :=
316 ∑ n, ringCost (mesh.rings n)
317
318/-! ### §3. Jensen coercivity -/
319
320/-- Jensen bound for phiCost on a single ring:
321 ∑ f(Δ_j) ≥ (8n) · f(∑Δ_j / (8n)).
322 Follows from strict convexity of cosh. -/
323theorem jensen_ring_bound {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
324 (8 * n : ℝ) * phiCost (-(2 * Real.pi * s.winding) / (8 * n)) ≤ ringCost s := by
325 have h8n_pos : 0 < (8 * n : ℝ) := by positivity
326 let w : Fin (8 * n) → ℝ := fun _ => 1 / (8 * n : ℝ)
327 have hw_nonneg : ∀ i ∈ (Finset.univ : Finset (Fin (8 * n))), 0 ≤ w i := by
328 intro _ _
329 dsimp [w]
330 positivity
331 have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin (8 * n))), w i = 1 := by
332 dsimp [w]
333 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
334 norm_num [Nat.cast_mul]
335 field_simp [h8n_pos.ne']
336 have hmem : ∀ i ∈ (Finset.univ : Finset (Fin (8 * n))), s.increments i ∈ (Set.univ : Set ℝ) := by
337 intro _ _
338 simp
339 have hJ :=
340 phiCost_convexOn.map_sum_le
341 (t := (Finset.univ : Finset (Fin (8 * n))))
342 (w := w) (p := s.increments) hw_nonneg hw_sum hmem
343 have h_avg :
344 ∑ i ∈ (Finset.univ : Finset (Fin (8 * n))), w i * s.increments i =
345 -(2 * Real.pi * s.winding) / (8 * n : ℝ) := by
346 dsimp [w]
347 rw [← Finset.mul_sum, s.winding_constraint]
348 field_simp [h8n_pos.ne']
349 have h_cost :
350 ∑ i ∈ (Finset.univ : Finset (Fin (8 * n))), w i * phiCost (s.increments i) =
351 ringCost s / (8 * n : ℝ) := by
352 dsimp [w]
353 unfold ringCost
354 rw [← Finset.mul_sum]
355 ring
356 have hJ' :
357 phiCost (-(2 * Real.pi * s.winding) / (8 * n : ℝ)) ≤ ringCost s / (8 * n : ℝ) := by
358 simpa [smul_eq_mul, h_avg, h_cost] using hJ
359 have hmult := mul_le_mul_of_nonneg_left hJ' h8n_pos.le
360 calc
361 (8 * n : ℝ) * phiCost (-(2 * Real.pi * s.winding) / (8 * n : ℝ))
362 ≤ (8 * n : ℝ) * (ringCost s / (8 * n : ℝ)) := hmult
363 _ = ringCost s := by
364 field_simp [h8n_pos.ne']
365
366/-- Coercivity: for charge m ≠ 0, ring n has cost ≥ π²κm²/(4n).
367 Uses the quadratic lower bound on phiCost. -/
368theorem ring_coercivity {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
369 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤ ringCost s := by
370 let u : ℝ := -(2 * Real.pi * s.winding) / (8 * n : ℝ)
371 have hphi := phiCost_quadratic_lb u
372 have hmul :=
373 mul_le_mul_of_nonneg_left hphi (by positivity : 0 ≤ (8 * n : ℝ))
374 have hleft :
375 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤
376 (8 * n : ℝ) * phiCost u := by
377 have hcalc :
378 (8 * n : ℝ) * (kappa * u ^ 2 / 2) =
379 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) := by
380 dsimp [u]
381 field_simp [show (8 * n : ℝ) ≠ 0 by positivity]
382 ring
383 rw [← hcalc]
384 exact hmul
385 exact hleft.trans (jensen_ring_bound hn s)
386
387/-- The topological floor: minimum possible cost for charge m on ring n. -/
388noncomputable def topologicalFloor (n : ℕ) (m : ℤ) : ℝ :=
389 (8 * n : ℝ) * phiCost (-(2 * Real.pi * m) / (8 * n))
390
391/-- The exact Jensen lower bound written as a named topological floor. -/
392theorem ringCost_ge_topologicalFloor {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
393 topologicalFloor n s.winding ≤ ringCost s := by
394 simpa [topologicalFloor] using jensen_ring_bound hn s
395
396/-- Ring-level perturbative upper bound above the topological floor.
397
398If each sampled increment is the uniform winding increment
399
400`-(2π m)/(8n)`
401
402plus a perturbation that is small in `log φ` coordinates, then the total ring
403cost is bounded by the topological floor plus explicit linear and quadratic
404error sums. -/
405theorem ringCost_le_topologicalFloor_add_linear_quadratic_error
406 {n : ℕ} (_hn : 0 < n) (s : AnnularRingSample n)
407 (hsmall : ∀ j : Fin (8 * n),
408 |Real.log phi *
409 (s.increments j - (-(2 * Real.pi * s.winding) / (8 * n : ℝ)))| ≤ 1) :
410 ringCost s ≤
411 topologicalFloor n s.winding +
412 phiCostLinearCoeff
413 (|(-(2 * Real.pi * s.winding) / (8 * n : ℝ))|) *
414 ∑ j : Fin (8 * n),
415 |s.increments j - (-(2 * Real.pi * s.winding) / (8 * n : ℝ))| +
416 phiCostQuadraticCoeff
417 (|(-(2 * Real.pi * s.winding) / (8 * n : ℝ))|) *
418 ∑ j : Fin (8 * n),
419 (s.increments j - (-(2 * Real.pi * s.winding) / (8 * n : ℝ))) ^ 2 := by
420 let u : ℝ := -(2 * Real.pi * s.winding) / (8 * n : ℝ)
421 have hu : |u| ≤ |u| := le_rfl
422 have hterm :
423 ∀ j : Fin (8 * n),
424 phiCost (s.increments j) ≤
425 phiCost u + phiCostLinearCoeff |u| * |s.increments j - u| +
426 phiCostQuadraticCoeff |u| * (s.increments j - u) ^ 2 := by
427 intro j
428 have hinc : u + (s.increments j - u) = s.increments j := by ring
429 have := phiCost_add_le_phiCost_add_linear_quadratic
430 (A := |u|) (u := u) (ε := s.increments j - u) hu (hsmall j)
431 simpa [hinc] using this
432 calc
433 ringCost s
434 = ∑ j : Fin (8 * n), phiCost (s.increments j) := by
435 rfl
436 _ ≤ ∑ j : Fin (8 * n),
437 (phiCost u + phiCostLinearCoeff |u| * |s.increments j - u| +
438 phiCostQuadraticCoeff |u| * (s.increments j - u) ^ 2) := by
439 apply Finset.sum_le_sum
440 intro j _
441 exact hterm j
442 _ = (∑ _j : Fin (8 * n), phiCost u) +
443 ∑ j : Fin (8 * n), phiCostLinearCoeff |u| * |s.increments j - u| +
444 ∑ j : Fin (8 * n), phiCostQuadraticCoeff |u| * (s.increments j - u) ^ 2 := by
445 rw [Finset.sum_add_distrib, Finset.sum_add_distrib]
446 _ = (8 * n : ℝ) * phiCost u +
447 phiCostLinearCoeff |u| * ∑ j : Fin (8 * n), |s.increments j - u| +
448 phiCostQuadraticCoeff |u| * ∑ j : Fin (8 * n), (s.increments j - u) ^ 2 := by
449 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul,
450 Finset.mul_sum, Finset.mul_sum]
451 norm_num [Nat.cast_mul]
452 _ = topologicalFloor n s.winding +
453 phiCostLinearCoeff
454 (|(-(2 * Real.pi * s.winding) / (8 * n : ℝ))|) *
455 ∑ j : Fin (8 * n),
456 |s.increments j - (-(2 * Real.pi * s.winding) / (8 * n : ℝ))| +
457 phiCostQuadraticCoeff
458 (|(-(2 * Real.pi * s.winding) / (8 * n : ℝ))|) *
459 ∑ j : Fin (8 * n),
460 (s.increments j - (-(2 * Real.pi * s.winding) / (8 * n : ℝ))) ^ 2 := by
461 dsimp [u, topologicalFloor]
462
463/-- The annular topological floor for a fixed charge sector over N rings. -/
464noncomputable def annularTopologicalFloor (N : ℕ) (m : ℤ) : ℝ :=
465 ∑ n : Fin N, topologicalFloor (n.val + 1) m
466
467/-- The excess cost above the topological floor for an annular mesh. -/
468noncomputable def annularExcess {N : ℕ} (mesh : AnnularMesh N) : ℝ :=
469 annularCost mesh - annularTopologicalFloor N mesh.charge
470
471/-- Annular coercivity: for charge m ≠ 0, total annular cost diverges
472 as Θ(m² log N). Specifically:
473 annularCost ≥ (π²κ/4) · m² · ∑_{n=1}^{N} 1/n. -/
474theorem annular_coercivity {N : ℕ} (hN : 0 < N) (mesh : AnnularMesh N)
475 (hm : mesh.charge ≠ 0) :
476 Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
477 ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1) ≤ annularCost mesh := by
478 have hterm : ∀ n : Fin N,
479 Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 * ((1 : ℝ) / ((n : ℝ) + 1))
480 ≤ ringCost (mesh.rings n) := by
481 intro n
482 have hn' : 0 < n.val + 1 := Nat.succ_pos _
483 have hcoer := ring_coercivity hn' (mesh.rings n)
484 rw [mesh.uniform_charge n] at hcoer
485 simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hcoer
486 calc
487 Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
488 ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1)
489 = ∑ n : Fin N, Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
490 ((1 : ℝ) / ((n : ℝ) + 1)) := by
491 rw [Finset.mul_sum]
492 _ ≤ ∑ n : Fin N, ringCost (mesh.rings n) := by
493 exact Finset.sum_le_sum (fun n _ => hterm n)
494 _ = annularCost mesh := by
495 rfl
496
497/-- The harmonic sum diverges, so nonzero charge forces unbounded cost. -/
498theorem harmonic_sum_diverges :
499 Filter.Tendsto (fun N => ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1))
500 Filter.atTop Filter.atTop := by
501 have h_log :
502 Filter.Tendsto (fun n : ℕ => Real.log ((n : ℝ) + 1)) Filter.atTop Filter.atTop := by
503 have h_add :
504 Filter.Tendsto (fun n : ℕ => (n : ℝ) + 1) Filter.atTop Filter.atTop := by
505 simpa using (tendsto_natCast_atTop_atTop.atTop_add tendsto_const_nhds)
506 exact Real.tendsto_log_atTop.comp h_add
507 have h_lower : ∀ N : ℕ, Real.log ((N : ℝ) + 1) ≤ ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1) := by
508 intro N
509 calc
510 Real.log ((N : ℝ) + 1) ≤ ∑ i ∈ Finset.range N, (1 : ℝ) / ((i : ℝ) + 1) := by
511 simpa [harmonic] using (log_add_one_le_harmonic N)
512 _ = ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1) := by
513 rw [← Fin.sum_univ_eq_sum_range]
514 exact Filter.tendsto_atTop_mono h_lower h_log
515
516/-! ### §4. Carrier traces and budgets -/
517
518/-- A regular carrier on a disk: holomorphic, nonvanishing, with
519 bounded logarithmic derivative. -/
520structure RegularCarrier where
521 logDerivBound : ℝ
522 logDerivBound_pos : 0 < logDerivBound
523 radius : ℝ
524 radius_pos : 0 < radius
525
526/-- A carrier trace is a refinement family of annular samples with fixed charge. -/
527structure AnnularTrace where
528 charge : ℤ
529 mesh : ∀ N : ℕ, AnnularMesh N
530 charge_spec : ∀ N : ℕ, (mesh N).charge = charge
531
532/-- A regular carrier equipped with an explicit excess-budget witness along a
533specific zero-charge annular trace.
534
535This is the realizable interface needed to state mesh-independent budget
536claims without quantifying over arbitrary synthetic meshes. The carrier does not
537just have a radius and a logarithmic-derivative scale; it also carries a
538specific trace family together with a uniform bound on the excess cost above the
539topological floor. -/
540structure BudgetedCarrier extends RegularCarrier where
541 trace : AnnularTrace
542 trace_charge_zero : trace.charge = 0
543 budgetConstant : ℝ
544 budgetConstant_nonneg : 0 ≤ budgetConstant
545 excess_bound : ∀ N : ℕ,
546 annularExcess (trace.mesh N) ≤ budgetConstant * logDerivBound ^ 2 * radius ^ 2
547
548/-- The scalar carrier budget appearing in the excess estimate. -/
549noncomputable def carrierBudgetScale (carrier : BudgetedCarrier) : ℝ :=
550 carrier.budgetConstant * carrier.logDerivBound ^ 2 * carrier.radius ^ 2
551
552/-- The carrier budget scale is nonnegative. -/
553theorem carrierBudgetScale_nonneg (carrier : BudgetedCarrier) :
554 0 ≤ carrierBudgetScale carrier := by
555 unfold carrierBudgetScale
556 exact mul_nonneg
557 (mul_nonneg carrier.budgetConstant_nonneg (sq_nonneg carrier.logDerivBound))
558 (sq_nonneg carrier.radius)
559
560/-- The carrier budget theorem: annular excess of the realized carrier trace
561 is bounded by `C · M² · R²`, independent of mesh refinement `N`.
562
563 For the specific carrier C(s) = det₂(I−A(s))²:
564 M = M_C(σ₀) = 2∑_p (log p)p^{−2σ₀}/(1−p^{−σ₀}) < ∞
565 for σ₀ > 1/2. -/
566theorem carrier_budget (carrier : BudgetedCarrier) :
567 ∃ K : ℝ, ∀ N : ℕ,
568 annularExcess (carrier.trace.mesh N) ≤ K * carrier.logDerivBound ^ 2 * carrier.radius ^ 2 := by
569 exact ⟨carrier.budgetConstant, carrier.excess_bound⟩
570
571/-- The topological floor is nonnegative. -/
572theorem topologicalFloor_nonneg (n : ℕ) (m : ℤ) : 0 ≤ topologicalFloor n m := by
573 unfold topologicalFloor
574 apply mul_nonneg
575 · positivity
576 · exact phiCost_nonneg _
577
578/-- Zero winding has zero topological floor on every ring. -/
579theorem topologicalFloor_zero (n : ℕ) : topologicalFloor n 0 = 0 := by
580 unfold topologicalFloor
581 simp [phiCost_zero]
582
583/-- The annular topological floor is nonnegative. -/
584theorem annularTopologicalFloor_nonneg (N : ℕ) (m : ℤ) :
585 0 ≤ annularTopologicalFloor N m := by
586 unfold annularTopologicalFloor
587 apply Finset.sum_nonneg
588 intro n _
589 exact topologicalFloor_nonneg (n.val + 1) m
590
591/-- Zero winding has zero annular topological floor on every mesh. -/
592theorem annularTopologicalFloor_zero (N : ℕ) :
593 annularTopologicalFloor N 0 = 0 := by
594 unfold annularTopologicalFloor
595 apply Finset.sum_eq_zero
596 intro n _
597 simp [topologicalFloor_zero]
598
599/-- The annular topological floor is bounded above by the total annular cost. -/
600theorem annularTopologicalFloor_le_annularCost {N : ℕ} (mesh : AnnularMesh N) :
601 annularTopologicalFloor N mesh.charge ≤ annularCost mesh := by
602 unfold annularTopologicalFloor annularCost
603 apply Finset.sum_le_sum
604 intro n _
605 have h := ringCost_ge_topologicalFloor (Nat.succ_pos n.val) (mesh.rings n)
606 rw [mesh.uniform_charge n] at h
607 simpa using h
608
609/-- Excess above the topological floor is nonnegative. -/
610theorem annularExcess_nonneg {N : ℕ} (mesh : AnnularMesh N) :
611 0 ≤ annularExcess mesh := by
612 unfold annularExcess
613 linarith [annularTopologicalFloor_le_annularCost mesh]
614
615/-- Nonzero charge forces a strictly positive topological floor on each ring. -/
616theorem topologicalFloor_pos_of_charge_ne_zero {n : ℕ} (hn : 0 < n) {m : ℤ} (hm : m ≠ 0) :
617 0 < topologicalFloor n m := by
618 unfold topologicalFloor
619 have hn' : 0 < (8 * n : ℝ) := by positivity
620 have hnum_ne : -(2 * Real.pi * (m : ℝ)) ≠ 0 := by
621 apply neg_ne_zero.mpr
622 apply mul_ne_zero
623 · norm_num [Real.pi_ne_zero]
624 · exact_mod_cast hm
625 have hu_ne : -(2 * Real.pi * (m : ℝ)) / (8 * n : ℝ) ≠ 0 := by
626 exact div_ne_zero hnum_ne (by positivity)
627 have hquad_pos : 0 < kappa * (-(2 * Real.pi * (m : ℝ)) / (8 * n : ℝ)) ^ 2 / 2 := by
628 apply div_pos
629 · exact mul_pos kappa_pos (sq_pos_iff.mpr hu_ne)
630 · norm_num
631 have hphi_lb := phiCost_quadratic_lb (-(2 * Real.pi * (m : ℝ)) / (8 * n : ℝ))
632 have hphi_pos :
633 0 < phiCost (-(2 * Real.pi * (m : ℝ)) / (8 * n : ℝ)) := by
634 exact lt_of_lt_of_le hquad_pos hphi_lb
635 exact mul_pos hn' hphi_pos
636
637/-- The one-ring topological floor is strictly positive for nonzero charge. -/
638theorem annularTopologicalFloor_one_pos_of_charge_ne_zero {m : ℤ} (hm : m ≠ 0) :
639 0 < annularTopologicalFloor 1 m := by
640 simpa [annularTopologicalFloor] using
641 topologicalFloor_pos_of_charge_ne_zero (by norm_num : 0 < 1) hm
642
643/-! ### §5. Excess bound -/
644
645/-- The excess cost: annular cost minus the topological floor.
646 For a field F(s) = (s−ρ)^{−m} G(s) with G regular:
647 excess = annularCost(F) − ∑ topologicalFloor(n, m) = O(R²). -/
648theorem excess_bounded (carrier : BudgetedCarrier) :
649 ∃ K : ℝ, ∀ N : ℕ,
650 annularExcess (carrier.trace.mesh N) ≤
651 K * carrier.logDerivBound ^ 2 * carrier.radius ^ 2 := by
652 exact carrier_budget carrier
653
654end NumberTheory
655end IndisputableMonolith
656