`not_realizedDefectAnnularCostBounded`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DefectSampledTrace
domain: NumberTheory
line: 462 · 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 462.

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

 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.