not_realizedDefectAnnularCostBounded
plain-language theorem explainer
A realized sampled family of annular meshes attached to a nonzero-charge defect sensor cannot have annular cost bounded independently of refinement level. Analysts refining Axiom 2 after the elimination of Axiom 1 cite this result to obtain contradictions from any assumed uniform cost bound. The proof is a one-line wrapper that assumes boundedness, invokes defectSampledFamily_unbounded to produce a mesh whose cost exceeds the bound, and closes via not_lt_of_ge.
Claim. Let $fam$ be a realized sampled family of annular meshes attached to one defect sensor. If the sensor charge is nonzero, then there does not exist a real $K$ such that the annular cost of the mesh at every refinement level $N$ satisfies annularCost$(fam.mesh N) ≤ K$.
background
DefectSampledFamily packages a sensor together with a sequence of realized AnnularMesh objects whose charges match the sensor at every level; it arises from the phase-sampling construction for ζ⁻¹ rather than from arbitrary synthetic meshes. RealizedDefectAnnularCostBounded asserts that the annular costs of these meshes remain below some fixed K for all N. The module replaces the earlier over-strong quantification over all AnnularMesh values with this canonical sampled family so that the refined Axiom 2 can be stated precisely. Upstream, defectSampledFamily_unbounded already shows that nonzero charge forces the cost of any such family to exceed every real bound.
proof idea
Assume RealizedDefectAnnularCostBounded fam. Extract the witnessing bound K. Apply defectSampledFamily_unbounded fam hm K to obtain an N with annularCost(fam.mesh N) > K. The final step is not_lt_of_ge (hK N) hN, which yields the contradiction.
why it matters
This supplies the direct contradiction step underlying the refined Axiom 2 in the Defect Sampled Trace construction. It is invoked by defect_bounded_impossible and by DeprecatedDefectAnnularCostBounded to convert any bounded-cost hypothesis into falsehood when charge is nonzero. The result therefore closes the analytic route after Axiom 1 has been removed and before the honest-phase bridge is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.