RingRegularErrorBound
plain-language theorem explainer
RingRegularErrorBound packages per-ring regular perturbation errors for any realized defect-sampled annular family. For each depth N and ring index n it supplies an error term such that ring cost sits at most topological floor plus that error, while the sum of all errors remains bounded by a constant independent of N. Researchers closing the refined Axiom 2 for the zeta defect cite it to obtain uniform annular excess control. The structure is instantiated directly from ring perturbation control data.
Claim. Let $F$ be a realized sampled family of annular meshes attached to a defect sensor. Then a ring-regular-error bound for $F$ consists of a map $e(N,n)$ such that the cost of the $n$-th ring in the mesh at depth $N$ satisfies ringCost((mesh $N$).rings $n$) ≤ topologicalFloor($n+1$, (mesh $N$).charge) + $e(N,n)$, together with the existence of $K$ for which ∑_n $e(N,n)$ ≤ $K$ for all $N$.
background
DefectSampledFamily collects a defect sensor together with a sequence of realized annular meshes at depths N, each carrying the sensor charge. The construction samples the phase of ζ^{-1} near a hypothetical defect and replaces arbitrary synthetic meshes with this concrete family. The topological floor is the charge-sector minimum cost; the regular error isolates the contribution of the non-singular factor in the local meromorphic factorization. The module context is the refined Axiom 2: any uniform upper bound on the cost of this realized family would contradict annular coercivity.
proof idea
The declaration is a structure definition whose three fields directly encode the error map, the ring-wise inequality, and the uniform total-error bound. It is produced by the one-line wrapper ringRegularErrorBound_of_ringPerturbationControl, which extracts the error function realizedRingPerturbationError from a RingPerturbationControl instance and assembles the three properties.
why it matters
The structure supplies the quantitative regular-error control required to bound annular excess for any realized sampled family. It is invoked in annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError and in realizedDefectAnnularExcessBounded_of_ringRegularErrorBound, and supplies the canonical instance for nonzero-charge sensors. In the Recognition framework it closes the refined Axiom 2 by converting ring-level perturbation data into a uniform bound on excess, linking directly to the meromorphic factorization and the phase-sampling construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.