canonicalDefectSampledFamily_ringPerturbationControl
plain-language theorem explainer
This definition equips the canonical defect-sampled family attached to a nonzero-charge sensor with a ring-perturbation control package. It certifies that every realized increment lies inside the unit-scale regime of the phi-cost function and that the total linear-plus-quadratic error sum remains bounded independently of mesh depth. Construction proceeds by factoring each increment into a pure winding term plus a small regular perturbation and invoking separate boundedness results for the linear and quadratic coefficients.
Claim. Let $S$ be a defect sensor with nonzero charge. Let $F$ be the canonical sampled family of realized annular meshes attached to the phase of $S$. Then $F$ admits a perturbation control: for all refinement depths $N$, ring indices $n$, and increment indices $j$, $|log phi · (Δ_j − (−2π · charge(F)/(8(n+1))))| ≤ 1, and there exists $K$ such that the summed realized ring perturbation errors over all rings at depth $N$ is at most $K$.
background
In the Defect Sampled Trace module the remaining obstacle after Axiom 1 is Axiom 2, which requires bounding the cost of the canonical sampled family coming from the phase of ζ⁻¹ near a hypothetical defect. The module packages this family via defectAnnularMesh and canonicalDefectSampledFamily. RingPerturbationControl is the structure that quantifies the deviation of realized increments from the pure topological winding term, using the linear and quadratic coefficients of the phi-cost function on [−A,A]. Upstream results supply the canonical arithmetic object, the universal forcing self-reference, and the non-resonant schedule, together with the explicit expressions for the linear and quadratic perturbation coefficients.
proof idea
The definition lets dpf be the chosen defect phase family and hw the chosen perturbation witness. It refines the small field by applying the regular perturbation smallness lemma to the decomposed increment pure + epsilon, after simplifying the pure term to the explicit winding formula. For the total_bounded field it obtains separate bounds on the linear and quadratic terms from the witness, then assembles the error sum by substituting the decomposition and applying sum-congruence to isolate the epsilon sums.
why it matters
This definition supplies the perturbation-control package that is fed directly into canonicalDefectSampledFamily_ringRegularErrorBound, which in turn yields the regular-error bound needed for bounded annular excess. It forms the quantitative target for the Axiom 2 attack: once the complex-analysis stack proves the required factorization and log-derivative bound on the regular factor, the present construction shows that Axiom 2 reduces exactly to forcing zero charge. The construction relies on the eight-tick octave structure implicit in the annular sampling and on the phi-cost expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.