chosenDefectPhaseFamily
plain-language theorem explainer
chosenDefectPhaseFamily selects one concrete phase family for any DefectSensor whose charge is nonzero. Workers on the Axiom 2 annular-coercivity bound cite it when they need a realized DefectPhaseFamily that already carries the regular-factor perturbation witness. Selection is performed by a one-line Classical.choose applied to the strengthened existence package defect_phase_family_with_perturbation_exists.
Claim. Let $s$ be a DefectSensor (a hypothetical pole of order $m$ of $ζ^{-1}$ at a point with real part in the critical strip) with $m ≠ 0$. Then chosenDefectPhaseFamily($s$, $m ≠ 0$) denotes a chosen element of DefectPhaseFamily attached to $s$ and equipped with the perturbation witness required for the annular-excess argument.
background
The module DefectSampledTrace constructs realized annular meshes that sample the phase of $ζ^{-1}$ near a hypothetical defect, after Axiom 1 has been removed. The remaining bottleneck is Axiom 2: one must bound the cost of the canonical sampled family rather than quantify over all AnnularMesh objects of the correct charge. DefectSensor is the structure recording the multiplicity (charge) and real part of such a hypothetical zero. DefectPhaseFamily is the type of phase-sampled families that can be turned into DefectSampledFamily objects via toSampledFamily.
proof idea
The definition is a one-line wrapper that applies Classical.choose to the existential theorem defect_phase_family_with_perturbation_exists, thereby obtaining both the family and the witness that downstream lemmas (chosenDefectPhasePerturbationWitness, canonicalDefectSampledFamily_ringPerturbationControl) require.
why it matters
It supplies the concrete family that canonicalDefectSampledFamily and canonicalDefectSampledFamily_ringPerturbationControl consume; the latter is the quantitative target for the Axiom 2 attack on annular coercivity. The construction sits inside the refined Axiom 2 bridge that replaces the earlier universal quantification over all meshes. It touches the open question whether the regular factor $g(z)$ in the local factorization $ζ^{-1} = (z-ρ)^{-m} g(z)$ yields a bounded excess above the topological floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.