chosenDefectPhaseFamily_sensor
plain-language theorem explainer
The theorem states that the phase family chosen for a nonzero-charge defect sensor recovers that sensor exactly. Researchers refining the Axiom 2 annular-cost bound cite this identity when assembling the canonical sampled family from phase sampling near a hypothetical zeta defect. The proof is a one-line term that extracts the sensor component from the specification of the existence theorem for defect phase families with perturbation witnesses.
Claim. Let $S$ be a defect sensor with nonzero charge. Let $F$ be the chosen defect phase family attached to $S$. Then the sensor component of $F$ equals $S$.
background
DefectSensor is the structure that records the charge (multiplicity of the zero of zeta, hence order of the pole of zeta inverse) together with the real part of a hypothetical defect location inside the critical strip. chosenDefectPhaseFamily selects one concrete DefectPhaseFamily via Classical.choose applied to the strengthened existence result defect_phase_family_with_perturbation_exists, which also supplies a perturbation witness for later annular-excess arguments. The module DefectSampledTrace builds realized annular meshes by sampling the phase of zeta inverse near such defects, replacing an earlier universal quantification over all meshes of given charge with a concrete sampled family; the eight-tick phases supply the discrete sampling angles.
proof idea
The proof is a one-line term that applies Classical.choose_spec to defect_phase_family_with_perturbation_exists and projects the first conjunct of the resulting pair, which records that the chosen family carries the requested sensor.
why it matters
The identity is invoked directly by canonicalDefectSampledFamily_sensor to propagate sensor attachment to the full sampled family and is used inside the construction of canonicalDefectSampledFamily_ringPerturbationControl, the quantitative target for the refined Axiom 2 attack. It therefore closes one link in the chain that converts the local factorization of zeta inverse into a bounded-excess statement for the realized family. The surrounding layer addresses the remaining bottleneck after Axiom 1 elimination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.