theorem proved term proof

`not_realizedDefectAnnularCostBounded`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 462theorem not_realizedDefectAnnularCostBounded (fam : DefectSampledFamily)
 463    (hm : fam.sensor.charge ≠ 0) :
 464    ¬ RealizedDefectAnnularCostBounded fam := by

proof body

Term-mode proof.

 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

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

HonestPhaseCostBridge_of_rh in IndisputableMonolith.NumberTheory.AnalyticTrace decl_use
defect_cost_unbounded_of_shared_pair in IndisputableMonolith.NumberTheory.CarrierBudgetComparison decl_use
argument_principle_sampling in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
defect_bounded_impossible in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
DeprecatedDefectAnnularCostBounded in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use

depends on (5)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
DefectSampledFamily in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
defectSampledFamily_unbounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use
RealizedDefectAnnularCostBounded in IndisputableMonolith.NumberTheory.DefectSampledTrace decl_use