ringRegularErrorBound_of_ringPerturbationControl
plain-language theorem explainer
The definition constructs a RingRegularErrorBound record for any realized sampled family of annular meshes once a quantitative perturbation control on its ring increments is given. Analysts proving bounded annular excess for the canonical zeta-defect trace cite the construction. It assembles the record by substituting the realized perturbation error, recovering uniform charge, and invoking the ring-cost inequality on each sampled ring.
Claim. Let $fam$ be a realized sampled family of annular meshes attached to a defect sensor and let $hctrl$ be a quantitative perturbation control asserting that each ring increment deviates from the pure winding term by at most one unit in the scaled logarithmic measure while the summed error remains uniformly bounded. Then $fam$ admits a ring-regular-error package whose per-ring error equals the realized ring perturbation error, whose ring-cost estimate reads ringCost ≤ topologicalFloor + error, and whose total error is bounded by the same uniform constant supplied by $hctrl$.
background
In the Defect Sampled Trace module a DefectSampledFamily consists of a defect sensor together with a sequence of realized AnnularMesh objects whose charges match the sensor; the construction replaces an earlier universal quantification over arbitrary meshes by a concrete family arising from the phase of ζ^{-1}. RingPerturbationControl supplies two fields: a smallness condition |log φ · (increment - pure winding term)| ≤ 1 on every sampled ring and a uniform bound on the summed realized perturbation errors across all rings and depths. RingRegularErrorBound packages the per-ring inequality ringCost ≤ topologicalFloor + error together with a uniform bound on the summed errors; this is the exact quantitative input required to obtain bounded annular excess.
proof idea
The definition builds the RingRegularErrorBound record by setting the error field to realizedRingPerturbationError and copying the total_bounded field from the control. For the ring_estimate it recovers the uniform charge via the mesh uniform_charge lemma, derives the small-increment hypothesis directly from the control, applies the ringCost_le_topologicalFloor_add_linear_quadratic_error lemma, substitutes the charge equality, and simplifies with add_assoc.
why it matters
The definition supplies the algebraic bridge that converts a perturbation witness into the error package needed for bounded annular excess. It is invoked directly by canonicalDefectSampledFamily_ringRegularErrorBound and by phaseFamily_excess_bounded_of_perturbationWitness, which establish RealizedDefectAnnularExcessBounded. In the Recognition framework it closes the quantitative step that refutes Axiom 2 for the realized defect trace, consistent with the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.