chosenDefectPhaseFamily
plain-language theorem explainer
Selects one concrete phase family attached to a hypothetical zeta defect sensor whose charge is nonzero. Analysts refining the Axiom 2 bound on realized annular cost cite it when building the canonical sampled family. The definition is obtained by a direct invocation of the axiom of choice on the strengthened existence result that also supplies the regular-factor perturbation witness.
Claim. Let $S$ be a defect sensor with nonzero charge $m$. The chosen phase family attached to $S$ is the object selected by the axiom of choice from the existence theorem that guarantees a phase family together with its regular-factor perturbation witness.
background
A defect sensor records the multiplicity $m$ of a hypothetical zero of the zeta function (equivalently the order of the pole of $1/ζ$) together with the real part of its location inside the critical strip. The Defect Sampled Trace module realizes annular meshes by sampling the phase of $ζ^{-1}$ near such a defect; the goal is to replace an overly strong universal quantification over all admissible meshes with a statement about one canonical sampled family. Upstream the eight-tick phase construction supplies the discrete angles $kπ/4$ for $k=0,…,7$, while the existence result for a defect phase family with perturbation witness supplies both the family and the witness required for the subsequent annular-excess control.
proof idea
One-line wrapper that invokes the axiom of choice on the existence theorem supplying a defect phase family equipped with its regular-factor perturbation witness.
why it matters
It supplies the concrete object that canonicalDefectSampledFamily converts into the realized sampled family, which is the precise target of the ring-perturbation-control bound needed to close the refined Axiom 2 argument. The construction sits inside the eight-tick phase-sampling layer and feeds directly into the quantitative attack on annular coercivity for nonzero-charge defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.