canonicalDefectSampledFamily_ringRegularErrorBound
plain-language theorem explainer
The definition supplies the ring-regular-error bound package for the canonical sampled family attached to any nonzero-charge defect sensor. Workers on the refined Axiom 2 would cite it to obtain the uniform error control required before proving bounded annular excess. The proof is a one-line wrapper that feeds the perturbation-control witness into ringRegularErrorBound_of_ringPerturbationControl.
Claim. Let $s$ be a defect sensor with nonzero charge. Let $F$ be the canonical sampled family obtained from the chosen phase family of $ζ^{-1}$ near the defect. Then $F$ satisfies the ring-regular-error bound: for each depth $N$ and ring index $n$, the sampled ring cost is at most the topological floor of its charge sector plus an error term, and the sum of all error terms remains bounded independently of $N$.
background
The module constructs realized annular meshes for a hypothetical zeta defect after Axiom 1 is removed. The remaining task is to bound the cost of the canonical sampled family rather than every possible AnnularMesh. A DefectSensor records the multiplicity (charge) of a zero of $ζ$ together with its real part. RingRegularErrorBound packages the quantitative statement that each ring cost lies within a topological floor plus a regular-part error, with the total error uniformly bounded across depths. The upstream canonicalDefectSampledFamily_ringPerturbationControl supplies the perturbation-control witness that this definition converts.
proof idea
One-line wrapper that applies ringRegularErrorBound_of_ringPerturbationControl to the perturbation-control package already constructed for the canonical family.
why it matters
This definition is the immediate predecessor of canonicalDefectSampledFamily_excess_bounded, which establishes RealizedDefectAnnularExcessBounded for the canonical family. It therefore supplies the exact error package needed to close the refined Axiom 2 argument via the local meromorphic factorization of $ζ^{-1}$. The construction sits inside the complex-analysis stack that must eventually deliver the ring-perturbation control from the regular factor $g(z)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.