canonicalDefectSampledFamily_ringPerturbationControl
plain-language theorem explainer
The definition constructs an explicit RingPerturbationControl instance for the canonical defect sampled family attached to any nonzero-charge sensor. Researchers reducing Axiom 2 to zero charge in the Recognition framework cite this when they need uniform bounds on realized annular excess for phase-sampled zeta defects. The construction decomposes each increment into pure winding plus epsilon, invokes regular perturbation lemmas on the smallness and coefficient bounds, then assembles the linear-plus-quadratic error sum.
Claim. Let $S$ be a defect sensor with nonzero charge. The canonical defect sampled family $F_S$ admits a ring perturbation control: for every $N$, every ring index $n$, and increment index $j$, $|$log$phi$ times (sampled increment minus pure winding term $-(2pi$ charge$)/(8(n+1)))$| is at most 1, and there exists $K$ such that the sum over rings of the realized ring perturbation error is at most $K$ for every $N$.
background
The Defect Sampled Trace module isolates the realized annular mesh family that arises from phase sampling of a hypothetical zeta defect, after Axiom 1 has been eliminated. The target is a quantitative bound on excess cost above the topological floor for this specific family rather than for arbitrary meshes. RingPerturbationControl is the structure whose small field enforces the unit-scale perturbative regime on each increment deviation and whose total_bounded field supplies a uniform $N$-independent majorant on the summed linear-plus-quadratic error. Upstream, phiCostLinearCoeff and phiCostQuadraticCoeff supply the explicit coefficients appearing in the error expansion on the interval $[-A,A]$.
proof idea
The definition builds the two fields of RingPerturbationControl. The small field is obtained by calling regular_perturbation_small after rewriting the increment via regular_factor_increment_decomposition and simplifying the pure increment term. The total_bounded field extracts linear and quadratic bounds via regular_perturbation_linear_term_bounded and regular_perturbation_quadratic_term_bounded, then matches the realizedRingPerturbationError expression by sum_congr, ring_nf, and substitution of the pure increment formula.
why it matters
This supplies the perturbation control that canonicalDefectSampledFamily_ringRegularErrorBound consumes to produce the ring regular error bound, which in turn feeds the reduction realizedDefectCostBounded_iff_charge_zero_and_excessBounded. The module doc-comment identifies the construction as the quantitative target for the Axiom 2 attack via local factorization of zeta inverse. In the Recognition framework it closes the step that converts the phase-sampling construction into a concrete bound usable for the refined Axiom 2 statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.