theorem
proved
realizedDefectCostBounded_of_charge_zero_and_excessBounded
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.DefectSampledTrace on GitHub at line 270.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
isolates -
K -
K -
has -
of -
cost -
cost -
is -
of -
is -
of -
is -
of -
is -
total -
annularExcess -
annularTopologicalFloor -
annularTopologicalFloor_zero -
and -
DefectSampledFamily -
RealizedDefectAnnularCostBounded -
RealizedDefectAnnularExcessBounded -
that -
total
used by
formal source
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