IndisputableMonolith.NumberTheory.DefectSampledTrace
IndisputableMonolith/NumberTheory/DefectSampledTrace.lean · 474 lines · 25 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.NumberTheory.AnnularCost
3import IndisputableMonolith.NumberTheory.CostCoveringBridge
4import IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
5
6/-!
7# Defect Sampled Trace
8
9Realized annular meshes attached to the phase-sampling construction for a
10hypothetical zeta defect.
11
12## Why this layer is needed
13
14After eliminating Axiom 1, the remaining bottleneck is Axiom 2. The previous
15formal statement quantified over *all* `AnnularMesh` values with the right
16charge, which is stronger than the intended analytic statement. What one really
17needs to bound is the cost of the **canonical sampled family** coming from the
18phase of `ζ⁻¹` near the hypothetical defect.
19
20This module packages that realized family:
21
22* `defectAnnularMesh` — sample one `DefectPhaseFamily` at depth `N`
23* `DefectSampledFamily` — a full refinement family of realized meshes
24* `canonicalDefectSampledFamily` — the chosen family attached to a sensor
25* `defectSampledFamily_unbounded` — nonzero charge still forces cost → ∞
26
27The last theorem is the key bridge for the refined Axiom 2: any uniform upper
28bound on the cost of the realized sampled family contradicts annular coercivity.
29-/
30
31namespace IndisputableMonolith
32namespace NumberTheory
33
34noncomputable section
35
36/-! ### §1. Sampling a phase family into annular meshes -/
37
38/-- Build an `AnnularMesh` from a `DefectPhaseFamily` by sampling each ring at
39the canonical `8n` equispaced angles. -/
40def defectAnnularMesh (dpf : DefectPhaseFamily) (N : ℕ) : AnnularMesh N where
41 rings := fun k =>
42 (dpf.phaseAtLevel (k.val + 1) (Nat.succ_pos k.val)).toAnnularRingSample
43 (k.val + 1) (Nat.succ_pos k.val)
44 charge := dpf.sensor.charge
45 uniform_charge := fun k =>
46 dpf.charge_uniform (k.val + 1) (Nat.succ_pos k.val)
47
48/-- The mesh obtained from phase sampling has the correct total charge. -/
49theorem defectAnnularMesh_charge (dpf : DefectPhaseFamily) (N : ℕ) :
50 (defectAnnularMesh dpf N).charge = dpf.sensor.charge :=
51 rfl
52
53/-! ### §2. Realized sampled families -/
54
55/-- A realized sampled family of annular meshes attached to one defect sensor.
56
57Unlike a bare `AnnularTrace`, this object is intended to arise from the actual
58phase-sampling construction for `ζ⁻¹`, not from an arbitrary synthetic mesh
59family. -/
60structure DefectSampledFamily where
61 sensor : DefectSensor
62 mesh : ∀ N : ℕ, AnnularMesh N
63 charge_spec : ∀ N : ℕ, (mesh N).charge = sensor.charge
64
65/-- Convert a `DefectPhaseFamily` to its realized sampled annular family. -/
66def DefectPhaseFamily.toSampledFamily (dpf : DefectPhaseFamily) :
67 DefectSampledFamily where
68 sensor := dpf.sensor
69 mesh := defectAnnularMesh dpf
70 charge_spec := defectAnnularMesh_charge dpf
71
72/-- Choose one phase family attached to a hypothetical defect sensor.
73
74This uses the strengthened existential package
75`defect_phase_family_with_perturbation_exists`, so the chosen family comes with
76the perturbation witness needed downstream for the annular excess argument. -/
77noncomputable def chosenDefectPhaseFamily (sensor : DefectSensor)
78 (hm : sensor.charge ≠ 0) : DefectPhaseFamily :=
79 Classical.choose (defect_phase_family_with_perturbation_exists sensor hm)
80
81/-- The chosen phase family is attached to the requested sensor. -/
82theorem chosenDefectPhaseFamily_sensor (sensor : DefectSensor)
83 (hm : sensor.charge ≠ 0) :
84 (chosenDefectPhaseFamily sensor hm).sensor = sensor :=
85 (Classical.choose_spec (defect_phase_family_with_perturbation_exists sensor hm)).1
86
87/-- The chosen phase family also carries the regular-factor perturbation witness
88needed to build the ring perturbation control package. -/
89noncomputable def chosenDefectPhasePerturbationWitness (sensor : DefectSensor)
90 (hm : sensor.charge ≠ 0) :
91 DefectPhasePerturbationWitness (chosenDefectPhaseFamily sensor hm) :=
92 Classical.choice ((Classical.choose_spec
93 (defect_phase_family_with_perturbation_exists sensor hm)).2)
94
95/-- The canonical realized sampled family attached to a hypothetical defect. -/
96noncomputable def canonicalDefectSampledFamily (sensor : DefectSensor)
97 (hm : sensor.charge ≠ 0) : DefectSampledFamily :=
98 (chosenDefectPhaseFamily sensor hm).toSampledFamily
99
100/-- The canonical sampled family remembers the requested sensor. -/
101theorem canonicalDefectSampledFamily_sensor (sensor : DefectSensor)
102 (hm : sensor.charge ≠ 0) :
103 (canonicalDefectSampledFamily sensor hm).sensor = sensor :=
104 chosenDefectPhaseFamily_sensor sensor hm
105
106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/
107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)
108 (hm : sensor.charge ≠ 0) (N : ℕ) :
109 ((canonicalDefectSampledFamily sensor hm).mesh N).charge = sensor.charge := by
110 simpa [canonicalDefectSampledFamily_sensor sensor hm] using
111 ((canonicalDefectSampledFamily sensor hm).charge_spec N)
112
113/-! ### §3. Refined bounded-cost proposition -/
114
115/-- The annular cost of a realized sampled family is bounded independently of
116mesh refinement. This is the realizable replacement for the previous
117over-strong quantification over arbitrary `AnnularMesh` values. -/
118def RealizedDefectAnnularCostBounded (fam : DefectSampledFamily) : Prop :=
119 ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K
120
121/-- The annular excess of a realized sampled family is bounded independently of
122mesh refinement. This is the quantitatively plausible part of the defect-cost
123story: after removing the topological floor, only the regular remainder should
124need analytic control. -/
125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=
126 ∃ K : ℝ, ∀ N : ℕ, annularExcess (fam.mesh N) ≤ K
127
128/-! ### §3a. Ring-level regular-part error control -/
129
130/-- A ring-level regular-part error package for a realized sampled family.
131
132For each depth `N` and ring `n`, the sampled ring cost is bounded by the
133topological floor for its charge sector plus an error term coming from the
134regular factor in the local meromorphic factorization. The total error across
135all rings is uniformly bounded in `N`.
136
137This is the exact quantitative input needed to prove bounded annular excess. -/
138structure RingRegularErrorBound (fam : DefectSampledFamily) where
139 error : ∀ N : ℕ, Fin N → ℝ
140 ring_estimate : ∀ N : ℕ, ∀ n : Fin N,
141 ringCost ((fam.mesh N).rings n) ≤
142 topologicalFloor (n.val + 1) ((fam.mesh N).charge) + error N n
143 total_error_bounded : ∃ K : ℝ, ∀ N : ℕ, ∑ n : Fin N, error N n ≤ K
144
145/-- The explicit linear-plus-quadratic perturbation error on one realized ring.
146
147This is the error term delivered by
148`ringCost_le_topologicalFloor_add_linear_quadratic_error` once the ring
149increments are written as the pure winding increment plus a regular
150perturbation. -/
151noncomputable def realizedRingPerturbationError (fam : DefectSampledFamily)
152 (N : ℕ) (n : Fin N) : ℝ :=
153 let u : ℝ := -(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)
154 phiCostLinearCoeff |u| *
155 ∑ j : Fin (8 * (n.val + 1)),
156 |((fam.mesh N).rings n).increments j - u| +
157 phiCostQuadraticCoeff |u| *
158 ∑ j : Fin (8 * (n.val + 1)),
159 (((fam.mesh N).rings n).increments j - u) ^ 2
160
161/-- Quantitative perturbation control for a realized sampled family.
162
163The `small` field says each sampled increment stays within the unit-scale
164perturbative regime of `phiCost` once expressed as
165
166`Δ_j = (pure winding increment) + ε_j`.
167
168The `total_bounded` field says the resulting linear-plus-quadratic error sums
169are uniformly bounded across refinement depth `N`. This is exactly the remaining
170analytic input needed after the perturbative `phiCost` reduction. -/
171structure RingPerturbationControl (fam : DefectSampledFamily) where
172 small : ∀ N : ℕ, ∀ n : Fin N, ∀ j : Fin (8 * (n.val + 1)),
173 |Real.log Constants.phi *
174 (((fam.mesh N).rings n).increments j -
175 (-(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)))| ≤ 1
176 total_bounded : ∃ K : ℝ, ∀ N : ℕ,
177 ∑ n : Fin N, realizedRingPerturbationError fam N n ≤ K
178
179/-- A perturbation-control package yields the ring-regular-error package needed
180for bounded annular excess. -/
181noncomputable def ringRegularErrorBound_of_ringPerturbationControl
182 (fam : DefectSampledFamily) (hctrl : RingPerturbationControl fam) :
183 RingRegularErrorBound fam := by
184 refine
185 { error := realizedRingPerturbationError fam
186 ring_estimate := ?_
187 total_error_bounded := hctrl.total_bounded }
188 intro N n
189 have hcharge : ((fam.mesh N).rings n).winding = (fam.mesh N).charge := by
190 rw [((fam.mesh N).uniform_charge n)]
191 have hsmall_ring :
192 ∀ j : Fin (8 * n.val.succ),
193 |Real.log Constants.phi *
194 (((fam.mesh N).rings n).increments j -
195 (-(2 * Real.pi * ((((fam.mesh N).rings n).winding : ℤ) : ℝ)) /
196 (8 * n.val.succ : ℝ)))| ≤ 1 := by
197 intro j
198 have hj := hctrl.small N n j
199 simpa [hcharge, Nat.succ_eq_add_one] using hj
200 have hring :=
201 ringCost_le_topologicalFloor_add_linear_quadratic_error
202 (Nat.succ_pos n.val) ((fam.mesh N).rings n) hsmall_ring
203 rw [hcharge] at hring
204 simpa [realizedRingPerturbationError, add_assoc] using hring
205
206/-- Summing the ring-level estimate yields a bound for annular excess.
207
208This is the unconditional algebraic step:
209
210`ringCost ≤ topologicalFloor + regularError`
211
212on each ring implies
213
214`annularExcess ≤ ∑ regularError`
215
216on the full annulus. -/
217theorem annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError
218 (fam : DefectSampledFamily) (hreg : RingRegularErrorBound fam) (N : ℕ) :
219 annularExcess (fam.mesh N) ≤ ∑ n : Fin N, hreg.error N n := by
220 have hsum :
221 annularCost (fam.mesh N) ≤
222 annularTopologicalFloor N ((fam.mesh N).charge) + ∑ n : Fin N, hreg.error N n := by
223 calc
224 annularCost (fam.mesh N)
225 = ∑ n : Fin N, ringCost ((fam.mesh N).rings n) := by
226 rfl
227 _ ≤ ∑ n : Fin N,
228 (topologicalFloor (n.val + 1) ((fam.mesh N).charge) + hreg.error N n) := by
229 apply Finset.sum_le_sum
230 intro n _
231 exact hreg.ring_estimate N n
232 _ = (∑ n : Fin N, topologicalFloor (n.val + 1) ((fam.mesh N).charge)) +
233 ∑ n : Fin N, hreg.error N n := by
234 rw [Finset.sum_add_distrib]
235 _ = annularTopologicalFloor N ((fam.mesh N).charge) + ∑ n : Fin N, hreg.error N n := by
236 rfl
237 unfold annularExcess
238 linarith
239
240/-- A uniform ring-level regular-part error bound implies bounded annular
241excess for the realized family. -/
242theorem realizedDefectAnnularExcessBounded_of_ringRegularErrorBound
243 (fam : DefectSampledFamily) (hreg : RingRegularErrorBound fam) :
244 RealizedDefectAnnularExcessBounded fam := by
245 obtain ⟨K, hK⟩ := hreg.total_error_bounded
246 refine ⟨K, ?_⟩
247 intro N
248 exact le_trans
249 (annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError fam hreg N)
250 (hK N)
251
252/-- A uniform total-cost bound immediately gives a uniform excess bound, since
253the topological floor is nonnegative. -/
254theorem realizedDefectAnnularExcessBounded_of_costBounded
255 (fam : DefectSampledFamily)
256 (hcost : RealizedDefectAnnularCostBounded fam) :
257 RealizedDefectAnnularExcessBounded fam := by
258 obtain ⟨K, hK⟩ := hcost
259 refine ⟨K, ?_⟩
260 intro N
261 unfold annularExcess
262 have hfloor : 0 ≤ annularTopologicalFloor N (fam.sensor.charge) :=
263 annularTopologicalFloor_nonneg N fam.sensor.charge
264 have hcostN : annularCost (fam.mesh N) ≤ K := hK N
265 rw [fam.charge_spec N]
266 linarith
267
268/-- If the sensor charge is zero, then bounded excess is equivalent to bounded
269total cost because the topological floor vanishes identically. -/
270theorem realizedDefectCostBounded_of_charge_zero_and_excessBounded
271 (fam : DefectSampledFamily)
272 (hzero : fam.sensor.charge = 0)
273 (hexcess : RealizedDefectAnnularExcessBounded fam) :
274 RealizedDefectAnnularCostBounded fam := by
275 obtain ⟨K, hK⟩ := hexcess
276 refine ⟨K, ?_⟩
277 intro N
278 have hfloor : annularTopologicalFloor N (fam.sensor.charge) = 0 := by
279 rw [hzero, annularTopologicalFloor_zero]
280 have hexN : annularExcess (fam.mesh N) ≤ K := hK N
281 unfold annularExcess at hexN
282 rw [fam.charge_spec N, hfloor] at hexN
283 simpa using hexN
284
285/-- For a realized sampled family, bounded total cost is exactly the conjunction
286of:
2871. zero charge, and
2882. bounded excess above the topological floor.
289
290This theorem isolates the remaining mathematical task cleanly: after the
291realized-family refactor, the analytically natural target is no longer a bound
292on arbitrary meshes, but a proof that the realized family has bounded excess
293and hence can only occur with zero charge. -/
294theorem realizedDefectCostBounded_iff_charge_zero_and_excessBounded
295 (fam : DefectSampledFamily) :
296 RealizedDefectAnnularCostBounded fam ↔
297 fam.sensor.charge = 0 ∧ RealizedDefectAnnularExcessBounded fam := by
298 constructor
299 · intro hcost
300 have hzero : fam.sensor.charge = 0 := by
301 by_cases hm : fam.sensor.charge = 0
302 · exact hm
303 · obtain ⟨K, hK⟩ := hcost
304 obtain ⟨N, hN⟩ := defect_cost_unbounded fam.sensor hm K
305 have hcharge : ∀ n, ((fam.mesh N).rings n).winding = fam.sensor.charge := by
306 intro n
307 rw [((fam.mesh N).uniform_charge n), fam.charge_spec N]
308 exact False.elim (not_lt_of_ge (hK N) (hN (fam.mesh N) hcharge))
309 exact ⟨hzero, realizedDefectAnnularExcessBounded_of_costBounded fam hcost⟩
310 · rintro ⟨hzero, hexcess⟩
311 exact realizedDefectCostBounded_of_charge_zero_and_excessBounded fam hzero hexcess
312
313/-- **Quantitative target for the Axiom 2 attack.**
314
315The canonical realized defect family should have bounded excess above the
316topological floor. This is the theorem that the current complex-analysis stack
317ought to prove from local factorization `ζ⁻¹ = (z-ρ)^{-m} g(z)` together with a
318log-derivative bound on the regular factor `g`.
319
320Once proved, `realizedDefectCostBounded_iff_charge_zero_and_excessBounded`
321shows that Axiom 2 reduces exactly to forcing zero charge. -/
322noncomputable def canonicalDefectSampledFamily_ringPerturbationControl
323 (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
324 RingPerturbationControl (canonicalDefectSampledFamily sensor hm) := by
325 let dpf := chosenDefectPhaseFamily sensor hm
326 let hw := chosenDefectPhasePerturbationWitness sensor hm
327 refine { small := ?_, total_bounded := ?_ }
328 · intro N n j
329 have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) j
330 have hinc :
331 (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
332 defectPhasePureIncrement dpf (n.val + 1) +
333 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
334 simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
335 defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
336 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
337 have hpure :
338 defectPhasePureIncrement dpf (n.val + 1) =
339 -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
340 (8 * (n.val + 1) : ℝ) := by
341 simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
342 chosenDefectPhaseFamily_sensor, dpf]
343 rw [hinc, hpure]
344 simpa using hsmall
345 obtain ⟨K₁, hK₁⟩ := regular_perturbation_linear_term_bounded hw
346 obtain ⟨K₂, hK₂⟩ := regular_perturbation_quadratic_term_bounded hw
347 refine ⟨K₁ + K₂, ?_⟩
348 intro N
349 have hlin := hK₁ N
350 have hquad := hK₂ N
351 have hterm :
352 ∀ n : Fin N,
353 realizedRingPerturbationError (canonicalDefectSampledFamily sensor hm) N n =
354 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
355 ∑ j : Fin (8 * (n.val + 1)),
356 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
357 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
358 ∑ j : Fin (8 * (n.val + 1)),
359 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
360 intro n
361 dsimp [realizedRingPerturbationError]
362 have hpure :
363 defectPhasePureIncrement dpf (n.val + 1) =
364 -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
365 (8 * (n.val + 1) : ℝ) := by
366 simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
367 chosenDefectPhaseFamily_sensor, dpf]
368 rw [hpure]
369 have hlinSum :
370 ∑ j : Fin (8 * (n.val + 1)),
371 |(((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
372 (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
373 (8 * (n.val + 1) : ℝ))| =
374 ∑ j : Fin (8 * (n.val + 1)),
375 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| := by
376 apply Finset.sum_congr rfl
377 intro j _
378 have hinc :
379 (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
380 defectPhasePureIncrement dpf (n.val + 1) +
381 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
382 simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
383 defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
384 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
385 rw [hinc, hpure]
386 ring_nf
387 have hquadSum :
388 ∑ j : Fin (8 * (n.val + 1)),
389 ((((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
390 (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
391 (8 * (n.val + 1) : ℝ))) ^ 2 =
392 ∑ j : Fin (8 * (n.val + 1)),
393 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
394 apply Finset.sum_congr rfl
395 intro j _
396 have hinc :
397 (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
398 defectPhasePureIncrement dpf (n.val + 1) +
399 hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
400 simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
401 defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
402 regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
403 rw [hinc, hpure]
404 ring_nf
405 rw [hlinSum, hquadSum]
406 calc
407 ∑ n : Fin N, realizedRingPerturbationError (canonicalDefectSampledFamily sensor hm) N n
408 = ∑ n : Fin N,
409 (phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
410 ∑ j : Fin (8 * (n.val + 1)),
411 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
412 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
413 ∑ j : Fin (8 * (n.val + 1)),
414 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2) := by
415 apply Finset.sum_congr rfl
416 intro n _
417 exact hterm n
418 _ = (∑ n : Fin N,
419 phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
420 ∑ j : Fin (8 * (n.val + 1)),
421 |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j|) +
422 ∑ n : Fin N,
423 phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
424 ∑ j : Fin (8 * (n.val + 1)),
425 (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
426 rw [Finset.sum_add_distrib]
427 _ ≤ K₁ + K₂ := by
428 linarith
429
430/-- The canonical perturbation-control package yields the regular-error package
431needed for bounded annular excess. -/
432noncomputable def canonicalDefectSampledFamily_ringRegularErrorBound (sensor : DefectSensor)
433 (hm : sensor.charge ≠ 0) :
434 RingRegularErrorBound (canonicalDefectSampledFamily sensor hm) := by
435 exact ringRegularErrorBound_of_ringPerturbationControl _
436 (canonicalDefectSampledFamily_ringPerturbationControl sensor hm)
437
438theorem canonicalDefectSampledFamily_excess_bounded (sensor : DefectSensor)
439 (hm : sensor.charge ≠ 0) :
440 RealizedDefectAnnularExcessBounded
441 (canonicalDefectSampledFamily sensor hm) := by
442 exact realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _
443 (canonicalDefectSampledFamily_ringRegularErrorBound sensor hm)
444
445/-- Nonzero charge forces the realized sampled family cost to exceed any bound.
446
447This is just `defect_cost_unbounded` specialized to the meshes of one realized
448family. The theorem is completely unconditional. -/
449theorem defectSampledFamily_unbounded (fam : DefectSampledFamily)
450 (hm : fam.sensor.charge ≠ 0) :
451 ∀ B : ℝ, ∃ N : ℕ, B < annularCost (fam.mesh N) := by
452 intro B
453 obtain ⟨N, hN⟩ := defect_cost_unbounded fam.sensor hm B
454 refine ⟨N, ?_⟩
455 have hcharge : ∀ n, ((fam.mesh N).rings n).winding = fam.sensor.charge := by
456 intro n
457 rw [((fam.mesh N).uniform_charge n), fam.charge_spec N]
458 exact hN (fam.mesh N) hcharge
459
460/-- A realized sampled family with nonzero charge can never have bounded annular
461cost. This is the contradiction theorem underlying the refined Axiom 2. -/
462theorem not_realizedDefectAnnularCostBounded (fam : DefectSampledFamily)
463 (hm : fam.sensor.charge ≠ 0) :
464 ¬ RealizedDefectAnnularCostBounded fam := by
465 intro hbound
466 obtain ⟨K, hK⟩ := hbound
467 obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hm K
468 exact not_lt_of_ge (hK N) hN
469
470end
471
472end NumberTheory
473end IndisputableMonolith
474