chosenDefectPhaseFamily_sensor
plain-language theorem explainer
The theorem asserts that the phase family selected via the existence package for a nonzero-charge defect sensor is attached exactly to that sensor. Number theorists refining the Axiom 2 bound via canonical sampled families in the Recognition Science zeta-defect construction would cite it for sensor consistency. The proof is a one-line term extraction of the first conjunct from the strengthened existence theorem via Classical.choose_spec.
Claim. Let $S$ be a defect sensor (a structure recording the multiplicity and location of a hypothetical zero of the zeta function) with nonzero charge. Then the chosen defect phase family attached to $S$ satisfies that its attached sensor equals $S$.
background
The DefectSampledTrace module constructs realized annular meshes attached to phase-sampling for a hypothetical zeta defect. After Axiom 1 is eliminated, the remaining task is to bound the cost of the canonical sampled family arising from the phase of ζ^{-1} near the defect, rather than quantifying over all possible AnnularMesh values. A DefectSensor is the structure with fields charge (multiplicity of the zero), realPart, and a flag that the zero lies in the right half of the critical strip. The chosenDefectPhaseFamily definition selects one DefectPhaseFamily using the strengthened existence result defect_phase_family_with_perturbation_exists, which supplies both sensor attachment and a perturbation witness.
proof idea
The proof is a term-mode one-liner that applies Classical.choose_spec directly to the existential statement defect_phase_family_with_perturbation_exists sensor hm, then projects the first conjunct of the resulting witness.
why it matters
It is invoked by canonicalDefectSampledFamily_sensor (which propagates the identity to the full sampled family) and by canonicalDefectSampledFamily_ringPerturbationControl (the quantitative target for the Axiom 2 attack on excess above the topological floor). The result closes the sensor-attachment step required before proving that nonzero charge forces unbounded realized cost, consistent with the module's goal of refining Axiom 2 via the phase-sampling construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.