canonicalDefectSampledFamily_sensor
canonicalDefectSampledFamily_sensor asserts that the canonical sampled family for a nonzero-charge defect sensor recovers the input sensor exactly. Researchers formalizing the refined Axiom 2 for the zeta defect would invoke it to propagate sensor data through the phase-sampling construction. The proof reduces directly to the sensor property of the underlying chosen defect phase family.
claimLet $S$ be a defect sensor with nonzero charge. If $F$ is the canonical defect sampled family attached to $S$, then the sensor field of $F$ equals $S$.
background
The Defect Sampled Trace module packages realized annular meshes attached to the phase-sampling construction for a hypothetical zeta defect. After Axiom 1 is eliminated, the remaining bottleneck is Axiom 2: one must bound the cost of the canonical sampled family coming from the phase of $ζ^{-1}$ near the defect, rather than quantifying over all AnnularMesh values. A DefectSensor is the structure recording the charge (multiplicity of the zero of $ζ$), the real part of the zero location, and the requirement that the zero lies in the right half of the critical strip. The canonicalDefectSampledFamily is obtained by converting the chosenDefectPhaseFamily for that sensor into a sampled family.
proof idea
The proof is a one-line wrapper that applies chosenDefectPhaseFamily_sensor to the given sensor and nonzero-charge hypothesis.
why it matters in Recognition Science
This result supplies the sensor identity used in canonicalDefectSampledFamily_charge to recover the charge at every mesh depth. It is invoked in defect_annular_cost_bounded_inconsistent and defect_bounded_impossible to derive contradictions from any bounded-cost assumption on the canonical family, and it supports realizedDefectCollapseBoundaryApproaching_of_nonzero_charge in UnifiedRH. The theorem closes the data-propagation step required for the refined Axiom 2 and annular coercivity arguments.
scope and limits
- Does not prove that the cost of the family tends to infinity.
- Does not apply when the sensor charge is zero.
- Does not construct or locate the underlying zeta zero.
- Does not bound the real part of the zero location.
formal statement (Lean)
101theorem canonicalDefectSampledFamily_sensor (sensor : DefectSensor)
102 (hm : sensor.charge ≠ 0) :
103 (canonicalDefectSampledFamily sensor hm).sensor = sensor :=
proof body
Term-mode proof.
104 chosenDefectPhaseFamily_sensor sensor hm
105
106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/