defect_phase_family_exists
plain-language theorem explainer
For a DefectSensor with nonzero charge, a DefectPhaseFamily exists whose sensor component matches exactly. Analysts formalizing the argument principle for the zeta function cite this to obtain honest phase samples on annular meshes around hypothetical zeros. The proof is a one-line extraction that projects the family out of the perturbation-aware existence theorem.
Claim. Let $s$ be a defect sensor with charge nonzero. Then there exists a defect phase family $d$ such that the sensor component of $d$ equals $s$.
background
The Meromorphic Circle Order module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. A meromorphic function with order $n$ at a point admits the local factorization into a power term carrying phase charge $-n$ and a holomorphic nonvanishing regular factor with zero charge. The DefectPhaseFamily structure packages a DefectSensor, a positive witness radius, and a level-indexed family of ContinuousPhaseData whose charge equals the sensor charge uniformly at every level. Upstream results include the eight-tick phase definition and ledger factorization structures that calibrate J-cost on the phi-ladder.
proof idea
The proof is a one-line wrapper that invokes defect_phase_family_with_perturbation_exists on the given sensor and nonzero-charge hypothesis, then projects out the family and the sensor equality while discarding the perturbation witness.
why it matters
This existence result supplies the phase family required by argument_principle_honest to build annular meshes from actual phase samples of zeta inverse rather than uniform meshes. It supports the reduction of the Riemann hypothesis formalization to a single axiom by guaranteeing phase charge matching for nonzero defect sensors. In the Recognition framework it connects meromorphic order at zeros to the defect sensor charge, consistent with the eight-tick octave and phi-forcing derived structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.