RealizedDefectAnnularCostBounded
plain-language theorem explainer
RealizedDefectAnnularCostBounded encodes the property that annular costs of meshes drawn from a DefectSampledFamily remain uniformly bounded by some fixed real K across all refinement depths N. Analysts closing the refined Axiom 2 statement for hypothetical zeta defects cite this predicate to restrict attention to phase-sampled families rather than arbitrary meshes. The definition is a direct existential quantifier over the uniform bound applied to annularCost of each mesh.
Claim. Let $fam$ be a realized sampled family of annular meshes attached to one defect sensor. Then $fam$ has bounded annular cost if there exists $K ∈ ℝ$ such that for every natural number $N$, the annular cost of the mesh at level $N$ satisfies annularCost$(fam.mesh N) ≤ K$.
background
DefectSampledFamily is the structure carrying a DefectSensor, a map from each $N ∈ ℕ$ to an AnnularMesh, and the charge_spec axiom ensuring mesh charge equals sensor charge at every level. It is obtained by converting a DefectPhaseFamily via defectAnnularMesh, so the meshes arise from actual phase sampling of $ζ^{-1}$ near a hypothetical defect rather than from synthetic constructions. The module packages this object to localize the cost bound after Axiom 1 is removed, leaving Axiom 2 as the remaining bottleneck that requires control only on the canonical sampled family.
proof idea
This declaration is a definition whose body is the direct statement ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K. No lemmas are applied; the predicate simply records the uniform bound on the sequence of annular costs for the realized family.
why it matters
The predicate is the key hypothesis in HonestPhaseCostBridge and is used to discharge charge_zero_of_honest_phase_of_costBridge once bounded cost is known. It also appears in the equivalence of honestPhase_routeC_bottleneck and in the carrier_defect_comparison_rh and defect_cost_unbounded_of_shared_pair results that separate zero-charge carriers from nonzero-charge defects. By replacing the prior quantification over all AnnularMesh with the realized sampled family, the definition supplies the quantitatively plausible part of the defect-cost story in the Recognition Science treatment of the zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.