canonicalDefectSampledFamily_sensor
plain-language theorem explainer
The theorem asserts that the canonical sampled family built from a nonzero-charge defect sensor recovers that sensor as its defining data. Workers on the refined Axiom 2 for annular cost bounds cite it when propagating sensor properties through realized families. The proof is a one-line wrapper that invokes the sensor property of the underlying chosen phase family.
Claim. Let $s$ be a defect sensor with nonzero charge. Then the sensor associated to the canonical sampled family constructed from $s$ equals $s$.
background
A DefectSensor is a structure recording an integer charge (multiplicity of the zero of zeta, hence order of the pole of zeta inverse), the real part of the zero location, and the assertion that the zero lies in the right half of the critical strip. The definition canonicalDefectSampledFamily converts the chosenDefectPhaseFamily for that sensor into a DefectSampledFamily of realized annular meshes. The module packages these realized families so that cost bounds can be stated for the specific canonical trace rather than for every possible mesh of matching charge.
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 identity supplies the sensor recovery step required by canonicalDefectSampledFamily_charge and by the inconsistency theorems defect_annular_cost_bounded_inconsistent and defect_bounded_impossible in EulerInstantiation. It likewise appears in the collapse-boundary argument realizedDefectCollapseBoundaryApproaching_of_nonzero_charge. The declaration therefore closes a bookkeeping obligation inside the Defect Sampled Trace module that supports the refined Axiom 2 after Axiom 1 has been eliminated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.