canonicalDefectSampledFamily
plain-language theorem explainer
This definition supplies the canonical realized sampled family of annular meshes for a defect sensor with nonzero charge. Analysts refining the Axiom 2 inconsistency argument cite it to instantiate the concrete family whose cost must diverge. The construction is a one-line wrapper converting the chosen phase family via its toSampledFamily method.
Claim. Let $S$ be a defect sensor with nonzero charge $m$. The canonical sampled family attached to $S$ is the structure obtained by converting the chosen phase family for $S$ into its realized annular mesh family, preserving the sensor and the charge specification on every mesh.
background
A DefectSensor records the multiplicity $m$ of a hypothetical zero of the zeta function (equivalently the order of the pole of $ζ^{-1}$) together with its real part inside the critical strip. The structure DefectSampledFamily packages a sensor, a map from depth $N$ to an AnnularMesh $N$, and the requirement that every mesh carries exactly the sensor charge. The module addresses the remaining bottleneck after Axiom 1 is eliminated: any uniform upper bound on the cost of the canonical sampled family contradicts annular coercivity. Upstream, chosenDefectPhaseFamily selects one phase family using the strengthened existential package defect_phase_family_with_perturbation_exists.
proof idea
One-line wrapper that applies the toSampledFamily conversion to the result of chosenDefectPhaseFamily sensor hm.
why it matters
It supplies the concrete object required by the downstream charge and excess theorems inside the same module and by the inconsistency result defect_annular_cost_bounded_inconsistent in EulerInstantiation. The module doc states that this family is the precise object whose cost must be shown to diverge for nonzero charge, completing the refined Axiom 2 attack. It sits between the phase-family choice and the ring-perturbation control package that targets bounded excess.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.