realizedDefectCostBounded_iff_charge_zero_and_excessBounded
plain-language theorem explainer
Bounded annular cost for a realized sampled family of annular meshes holds precisely when the attached sensor charge is zero and the excess above the topological floor stays bounded. Analysts refining the zeta-defect analysis cite this to reduce Axiom 2 to a charge-zero condition once excess control is shown. The proof splits the biconditional via constructor, using case analysis plus an unbounded-cost contradiction lemma in one direction and a direct construction lemma in the other.
Claim. For a realized sampled family $fam$ of annular meshes, the total annular cost is bounded independently of refinement depth if and only if the sensor charge vanishes and the annular excess above the topological floor is bounded independently of refinement.
background
DefectSampledFamily consists of a defect sensor together with a family of annular meshes at depths $N$, where each mesh charge equals the sensor charge by construction. RealizedDefectAnnularCostBounded asserts a uniform $K$ such that annularCost of the mesh at depth $N$ is at most $K$ for all $N$. RealizedDefectAnnularExcessBounded asserts the same for annularExcess after subtracting the topological floor set by the charge sector.
proof idea
The tactic proof opens with constructor. The forward direction performs case analysis on the sensor charge; nonzero charge triggers defect_cost_unbounded to contradict the cost bound, after which realizedDefectAnnularExcessBounded_of_costBounded supplies the excess claim. The reverse direction applies realizedDefectCostBounded_of_charge_zero_and_excessBounded directly.
why it matters
The equivalence isolates the remaining task for Axiom 2 after the realized-family refactor: bounded excess plus zero charge. It feeds honestPhaseFamily_charge_zero_of_costBounded, which concludes charge zero from bounded cost on honest phase data. In the Recognition framework this separates the topological charge condition from analytic excess control, advancing the quantitative target stated in the module comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.