canonicalDefectSampledFamily_ringPerturbationControl
plain-language theorem explainer
This definition constructs a ring perturbation control package for the canonical sampled defect family attached to any nonzero-charge sensor. Researchers reducing Axiom 2 to zero charge in the Recognition framework would cite it when bounding realized annular excess. The construction extracts the chosen phase family and its witness, then applies regular perturbation smallness and linear-quadratic boundedness lemmas to verify both fields of the structure.
Claim. Let $S$ be a defect sensor with nonzero charge. The canonical sampled defect family attached to $S$ admits a ring perturbation control package: for every refinement depth $N$, every ring index $n$, and every increment index $j$, the deviation of the sampled increment from the pure winding term satisfies $|$log $phi$ times deviation$| leq 1$, and there exists $K$ such that the summed linear-plus-quadratic perturbation error over all rings up to $N$ is at most $K$ for every $N$.
background
RingPerturbationControl is the structure whose small field requires each sampled increment to lie in the unit-scale regime of phiCost once written as pure winding increment plus epsilon, while total_bounded requires the summed linear-plus-quadratic error to be uniformly bounded in refinement depth. The module DefectSampledTrace packages realized annular meshes for a hypothetical zeta defect after Axiom 1 is eliminated; the canonical sampled family is the one obtained by sampling the phase of zeta inverse near the defect via ContinuousPhaseData and DefectSensor. Upstream, phiCostLinearCoeff and phiCostQuadraticCoeff supply the explicit linear and quadratic coefficients on the interval [-A,A] that appear in the error expression.
proof idea
The definition proceeds by letting dpf be the chosen defect phase family and hw its perturbation witness. For the small field it invokes regular_perturbation_small together with the increment decomposition and the explicit pure-increment formula. For total_bounded it obtains K1 and K2 from the linear and quadratic boundedness lemmas on hw, then rewrites realizedRingPerturbationError via the pure increment and the epsilon sums to obtain the required uniform K.
why it matters
This definition supplies the perturbation control instance required by the downstream ringRegularErrorBound_of_ringPerturbationControl, which in turn feeds the reduction of Axiom 2 to forcing zero charge. The module doc-comment states that once realizedDefectCostBounded_iff_charge_zero_and_excessBounded is available, Axiom 2 reduces exactly to zero charge; the present construction closes the quantitative gap between the canonical family and the annular coercivity statement. It sits inside the T5-T8 forcing chain by controlling the defect cost on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.