realizedDefectAnnularExcessBounded_of_ringRegularErrorBound
plain-language theorem explainer
A uniform bound on summed regular-part errors across rings in a sampled defect family implies that annular excess remains bounded under mesh refinement. Analysts closing the refined Axiom 2 for the zeta defect would cite this to convert ring estimates into global excess control. The term proof extracts the uniform error constant K from the hypothesis and chains it via le_trans to the auxiliary inequality that bounds annular excess by the sum of regular errors.
Claim. If a sampled family of annular meshes admits a ring-regular error bound (each ring cost bounded above by the topological floor of its charge sector plus an error term, with the sum of those errors bounded by some $K$ independent of depth), then the annular excess of each mesh in the family is bounded by the same $K$.
background
The Defect Sampled Trace module constructs realized annular meshes from phase sampling of the inverse zeta function near a hypothetical defect. A DefectSampledFamily consists of a fixed-charge sensor together with a sequence of AnnularMesh objects at depths $N$ whose charges match the sensor. RingRegularErrorBound packages per-ring estimates ringCost(ring) ≤ topologicalFloor(charge sector) + error(N,n) together with the uniform bound ∑ error(N,n) ≤ K for all $N$. RealizedDefectAnnularExcessBounded asserts that annularExcess(mesh N) remains ≤ some constant for all $N$ (MODULE_DOC).
proof idea
The term-mode proof obtains the pair ⟨K, hK⟩ from the total_error_bounded field of the RingRegularErrorBound hypothesis. It refines the goal to exhibit this K as the uniform bound for annular excess. For each fixed N it applies le_trans to the inequality annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError (which consumes the ring_estimate field) followed by hK N.
why it matters
This implication is invoked by canonicalDefectSampledFamily_excess_bounded to conclude bounded excess for the canonical family attached to a nonzero-charge sensor, and by phaseFamily_excess_bounded_of_perturbationWitness for families arising from perturbation witnesses. It forms the quantitative link that would refute annular coercivity if a uniform cost bound were available, directly supporting the refined Axiom 2. Within Recognition Science it contributes to controlling J-cost excess on the phi-ladder after removal of the topological floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.