defect_phase_family_with_perturbation_exists
plain-language theorem explainer
For any defect sensor with nonzero charge, a defect phase family attached to the sensor exists together with a nonempty collection of regular-factor perturbation witnesses. Researchers constructing the canonical sampled family and ring perturbation control in DefectSampledTrace cite this result to obtain the quantitative epsilon data for annular excess estimates. The proof is a direct term-mode instantiation of the trivial family and its zero-perturbation witness.
Claim. Let $S$ be a defect sensor with charge nonzero. Then there exists a defect phase family $D$ such that the sensor of $D$ equals $S$ and the type of defect phase perturbation witnesses for $D$ is nonempty.
background
A defect sensor records the pole order (charge) of $ζ^{-1}$ at a zero of $ζ$, together with its real part. From the upstream definition: 'A defect sensor at a point ρ: the field ζ(s)⁻¹ has a pole of order m at ρ (where m is the multiplicity of the zero of ζ).'
proof idea
The proof is a term-mode one-liner. It instantiates the trivial defect phase family for the given sensor and supplies the trivial perturbation witness, which sets all epsilon increments to zero while satisfying the increment equation and the smallness bound.
why it matters
This existence result packages the perturbation witness required downstream for RingPerturbationControl and the annular excess argument. It is invoked by chosenDefectPhaseFamily, chosenDefectPhasePerturbationWitness, and the weaker defect_phase_family_exists in DefectSampledTrace. The construction closes the local meromorphic factorization into a quantitative package compatible with the phi-ladder cost estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.