DefectPhasePerturbationWitness
plain-language theorem explainer
DefectPhasePerturbationWitness equips any DefectPhaseFamily with a map epsilon that splits each sampled increment into the pure winding term plus a regular perturbation. Workers constructing RingPerturbationControl for annular excess bounds on zeta-derived families cite the structure to close the regular-factor contribution. The definition directly records the decomposition equality, the unit bound on log-phi scaled epsilon, and uniform K bounds on the summed linear and quadratic costs over refinement depth N.
Claim. Let dpf be a DefectPhaseFamily. A witness consists of a function epsilon assigning reals to each level n>0 and sample index j in Fin(8n) such that the sampled increment at that level equals defectPhasePureIncrement(dpf,n) plus epsilon(n,hn,j), with |log phi * epsilon| <=1 for all such indices, and there exist K such that the N-dependent sums of phiCostLinearCoeff(|pure increment|) times sum |epsilon| and of phiCostQuadraticCoeff times sum epsilon^2 remain bounded by K.
background
DefectPhaseFamily is the structure carrying a DefectSensor, a positive witness radius, and a family of ContinuousPhaseData (one per refinement level n) all sharing the same charge; its phaseAtLevel supplies the sampled increments that the witness perturbs. The module MeromorphicCircleOrder translates Mathlib meromorphicOrderAt into the RS annular-cost setting by separating the pole factor (pure winding) from the regular analytic factor g via local_meromorphic_factorization. Upstream, phiCostLinearCoeff(A) = log phi * sinh(log phi * A) and the quadratic counterpart from AnnularCost supply the coefficients that turn the epsilon bounds into summable excess; defectPhasePureIncrement is the pure term extracted from the same family definition.
proof idea
This is a structure definition whose four fields are exactly the data clauses required by downstream RingPerturbationControl. No tactics or lemmas are applied; the fields are stated directly.
why it matters
The structure supplies the perturbation data that phaseFamily_ringPerturbationControl turns into a RingPerturbationControl instance, which phaseFamily_excess_bounded_of_perturbationWitness and honestPhaseFamily_excess_bounded_of_perturbationWitness then convert into RealizedDefectAnnularExcessBounded. It therefore completes the analytic step between the meromorphic factorization and the bounded annular-cost claims that support the phi-ladder cost control in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.