RingPerturbationControl
plain-language theorem explainer
RingPerturbationControl equips a DefectSampledFamily with a smallness condition on each ring increment relative to the pure winding term and a uniform bound on summed realized perturbation errors across all refinement depths N. Analysts working on the zeta defect and Axiom 2 would cite it to close the gap between phiCost reduction and bounded annular excess. The declaration is a structure definition whose two fields directly encode the unit-scale regime and the total error control.
Claim. For a defect sampled family $fam$, the structure consists of two fields: (i) smallness, requiring that for every $N$, every $n$ in Fin $N$, and every $j$ in Fin $(8(n+1))$, $|log(φ) · ((fam.mesh N).rings n).increments j - (-2π · charge / (8(n+1)))| ≤ 1$; (ii) total boundedness, requiring existence of a real $K$ such that for every $N$ the sum over $n$ in Fin $N$ of realizedRingPerturbationError($fam$, $N$, $n$) is at most $K$.
background
The module DefectSampledTrace constructs realized annular meshes for a hypothetical zeta defect after Axiom 1 is eliminated. The remaining task is to bound the cost of the canonical sampled family rather than all possible meshes of given charge. DefectSampledFamily is the structure carrying a defect sensor, a mesh function from N to AnnularMesh N, and the charge specification that each mesh inherits the sensor charge. RingPerturbationControl supplies the quantitative perturbation data needed once the pure winding increment is subtracted, leaving the error term controlled by log(φ) scaling.
proof idea
This is a structure definition. The small field states the absolute deviation of each sampled increment from the pure winding term stays inside the unit interval after multiplication by log(φ). The total_bounded field asserts a single K that majorizes the sum of realizedRingPerturbationError over all rings at every depth N.
why it matters
The structure is the direct input to ringRegularErrorBound_of_ringPerturbationControl, which produces the RingRegularErrorBound package required for bounded annular excess. It is also instantiated in canonicalDefectSampledFamily_ringPerturbationControl, the quantitative target for the Axiom 2 attack, and in phaseFamily_ringPerturbationControl. The definition therefore supplies the remaining analytic input after the perturbative phiCost reduction and before the eight-tick octave and D=3 geometry are applied to close the defect trace.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.