`defectSampledFamily_unbounded`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DefectSampledTrace
domain: NumberTheory
line: 449 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.DefectSampledTrace on GitHub at line 449.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.