RealizedDefectAnnularExcessBounded
plain-language theorem explainer
Annular excess for meshes in a realized sampled family attached to a defect sensor remains bounded by some constant independent of refinement depth N. Researchers analyzing the zeta defect cost bounds after Axiom 1 elimination cite this when separating regular remainder control from total cost. The definition encodes the property directly as an existential statement over a uniform real bound on the annularExcess sequence.
Claim. For a sampled family $fam$ of annular meshes attached to one defect sensor, there exists $K ∈ ℝ$ such that for every natural number $N$, the annular excess of the mesh at depth $N$ satisfies annularExcess$(fam.mesh(N)) ≤ K$.
background
The Defect Sampled Trace module constructs realized annular meshes from the phase-sampling of $ζ^{-1}$ near a hypothetical defect. A DefectSampledFamily is the structure consisting of a defect sensor, a mesh assignment $∀ N : ℕ$, AnnularMesh $N$, and the charge specification that each mesh carries exactly the sensor charge. This replaces quantification over arbitrary AnnularMesh families with the canonical sampled family arising from the actual phase construction, addressing the refined Axiom 2 bottleneck after Axiom 1 removal.
proof idea
The declaration is the definition itself: it directly sets the Prop to the statement that annular excess is uniformly bounded, i.e., the existence of $K$ such that the inequality holds for all $N$. No lemmas are applied; downstream theorems such as realizedDefectAnnularExcessBounded_of_ringRegularErrorBound discharge the property by supplying the required $K$ from a ring-regular error bound.
why it matters
This definition supplies the target property invoked by honestPhase_routeC_bottleneck (which records that honest phase data already has bounded excess but bounded total cost requires zero charge) and by canonicalDefectSampledFamily_excess_bounded (which proves the bound for the canonical family when charge is nonzero). It supplies the quantitative control on the regular remainder after topological floor removal that the Recognition framework needs for the defect-cost story. It touches the open upgrade from bounded excess to zero charge for admissibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.