chosenDefectPhaseFamily_sensor
The theorem states that for a defect sensor with nonzero charge the chosen phase family returns exactly that sensor. Researchers refining Axiom 2 for the zeta defect in Recognition Science cite it to confirm attachment before building the canonical sampled family. The proof is a direct one-line extraction via Classical.choose_spec on the first component of the strengthened existence theorem.
claimLet $σ$ be a defect sensor with charge $m ≠ 0$. The chosen defect phase family attached to $σ$ satisfies that its sensor component equals $σ$.
background
The Defect Sampled Trace module packages realized annular meshes for a hypothetical zeta defect after Axiom 1 is eliminated. A DefectSensor is a structure holding the charge (multiplicity of the zero of $ζ$, hence pole order of $ζ^{-1}$), the real part of the location, and confirmation that the zero lies in the right half of the critical strip. The chosenDefectPhaseFamily definition selects one such family by Classical.choose from the existence theorem defect_phase_family_with_perturbation_exists, which also carries a regular-factor perturbation witness for later annular excess arguments.
proof idea
Term-mode one-liner that invokes Classical.choose_spec on the existence theorem defect_phase_family_with_perturbation_exists and projects to its first component, which is the required sensor equality.
why it matters in Recognition Science
This attachment result is invoked by canonicalDefectSampledFamily_sensor to propagate the sensor identity to the full sampled family and by the ring perturbation control definition that targets bounded excess above the topological floor. It closes the sensor loop in the phase-sampling construction needed for the refined Axiom 2 attack, consistent with the eight-tick phase structure supplied by the upstream EightTick module.
scope and limits
- Does not prove existence of any phase family.
- Does not supply cost or excess bounds.
- Applies only to sensors with nonzero charge.
- Does not address the Riemann hypothesis.
- Does not construct explicit meshes.
Lean usage
theorem sensor_preservation (sensor : DefectSensor) (hm : sensor.charge ≠ 0) : (canonicalDefectSampledFamily sensor hm).sensor = sensor := canonicalDefectSampledFamily_sensor sensor hmformal statement (Lean)
82theorem chosenDefectPhaseFamily_sensor (sensor : DefectSensor)
83 (hm : sensor.charge ≠ 0) :
84 (chosenDefectPhaseFamily sensor hm).sensor = sensor :=
proof body
Term-mode proof.
85 (Classical.choose_spec (defect_phase_family_with_perturbation_exists sensor hm)).1
86
87/-- The chosen phase family also carries the regular-factor perturbation witness
88needed to build the ring perturbation control package. -/