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. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.