canonicalDefectSampledFamily_sensor
plain-language theorem explainer
The theorem states that the canonical sampled family attached to a defect sensor with nonzero charge retains that sensor unchanged. Workers refining the annular cost bound for a hypothetical zeta defect cite it to keep the realized family aligned with the input charge. The proof is a one-line wrapper applying the sensor property of the chosen defect phase family.
Claim. Let $S$ be a defect sensor with nonzero charge $m$. Then the sensor of the canonical realized sampled family attached to $S$ equals $S$.
background
The Defect Sampled Trace module constructs realized annular meshes for a hypothetical zeta defect once Axiom 1 is removed. The remaining task is to bound the cost of the canonical sampled family derived from the phase of $ζ^{-1}$ near the defect. A DefectSensor records the multiplicity (charge) of a zero of $ζ$ together with its real part inside the critical strip. The canonicalDefectSampledFamily is obtained by converting the chosenDefectPhaseFamily to a sampled family. Upstream results supply realization-independent canonical objects in arithmetic and scheduling, while the module document notes that any uniform upper bound on the cost of this realized family contradicts annular coercivity.
proof idea
The proof is a one-line wrapper that applies chosenDefectPhaseFamily_sensor to the given sensor and nonzero-charge hypothesis.
why it matters
The result guarantees that the canonical family matches the requested sensor, which is required by the charge specification theorem and by the inconsistency statements defect_annular_cost_bounded_inconsistent and defect_bounded_impossible. It also feeds realizedDefectCollapseBoundaryApproaching_of_nonzero_charge. The declaration closes the refined Axiom 2 bridge that replaces a universal quantification over all meshes by a concrete realized trace, consistent with the Recognition Science program of discharging structural axioms via explicit constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.