theorem
proved
eulerSampledFloorCovered_iff_charge_zero
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.EulerInstantiation on GitHub at line 979.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
annularTopologicalFloor_zero -
carrierBudgetScale_nonneg -
DefectSensor -
DefectTopologicalFloorCovered -
not_DefectTopologicalFloorCovered -
eulerSampledPackage
used by
formal source
976 carrier := eulerSampledBudgetedCarrier σ₀ hσ
977
978/-- The sampled package's floor coverage is equivalent to charge = 0. -/
979theorem eulerSampledFloorCovered_iff_charge_zero (σ₀ : ℝ) (hσ : 1/2 < σ₀)
980 (sensor : DefectSensor) :
981 DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor ↔
982 sensor.charge = 0 := by
983 constructor
984 · intro hcover
985 by_contra hm
986 exact not_DefectTopologicalFloorCovered (eulerSampledPackage σ₀ hσ) sensor hm hcover
987 · intro hzero
988 intro N
989 rw [hzero, annularTopologicalFloor_zero]
990 exact carrierBudgetScale_nonneg _
991
992end NumberTheory
993end IndisputableMonolith