phaseFamily_ringPerturbationControl
plain-language theorem explainer
Given a defect phase family and its perturbation witness, this definition constructs the ring perturbation control package required by annular cost estimates. Researchers bridging phase families to sampled annular excess in the Recognition Science setting would cite it to obtain the needed error bounds. The construction decomposes each ring increment into a pure defect term plus witness epsilon, then applies the regular perturbation smallness and boundedness lemmas to the linear and quadratic contributions.
Claim. Let $dpf$ be a defect phase family and $hw$ a perturbation witness for it. Then there exists a ring perturbation control for the annular mesh sampled from $dpf$, with per-ring increments small and the total realized error bounded by the linear and quadratic coefficients of the phi-cost function applied to the absolute pure increment.
background
The Honest Phase Budget Bridge module supplies quantitative analytic control beyond pure completed-xi symmetry: a perturbation witness for an actual phase family. A DefectPhaseFamily packages phase assignments at successive levels together with a sensor charge; defectAnnularMesh converts it to an AnnularMesh by sampling each ring at 8n equispaced angles. ContinuousPhaseData records a continuous phase function on a circle together with its integer winding number (charge). The coefficients phiCostLinearCoeff and phiCostQuadraticCoeff from AnnularCost bound the linear and quadratic remainders of the phi-cost function on a symmetric interval. Upstream, the eight-tick phases supply the discrete sampling angles used throughout.
proof idea
The definition refines a RingPerturbationControl record. The smallness clause invokes regular_perturbation_small after decomposing the sampled increment via regular_factor_increment_decomposition into the pure defect term (extracted by defectPhasePureIncrement) plus the witness epsilon. The total-bounded clause obtains linear and quadratic constants from regular_perturbation_linear_term_bounded and regular_perturbation_quadratic_term_bounded, then rewrites the realizedRingPerturbationError sum as the corresponding weighted sums of absolute epsilons and squared epsilons.
why it matters
The definition is applied directly by phaseFamily_excess_bounded_of_perturbationWitness to conclude RealizedDefectAnnularExcessBounded for the sampled family. It supplies the Euler/Hadamard-style quantitative control described in the module documentation, converting a perturbation witness into bounded annular excess data. In the Recognition framework this step closes the bridge from honest phase families to the annular-cost machinery, enabling the passage from phase data to excess bounds without invoking the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.