canonicalDefectSampledFamily
plain-language theorem explainer
The definition supplies the canonical realized sampled family of annular meshes for a defect sensor with nonzero charge. Analysts refining the Axiom 2 inconsistency argument in the Recognition Science zeta-defect analysis cite this object when they need a concrete phase-sampled family rather than an arbitrary mesh. The construction is a direct one-line conversion of the chosen phase family via its toSampledFamily method.
Claim. Let $S$ be a defect sensor with nonzero charge. The canonical sampled family attached to $S$ is the family obtained by converting the chosen phase family for $S$ into a sampled family of annular meshes.
background
The DefectSampledTrace module packages realized annular meshes that arise from the phase-sampling construction for $ζ^{-1}$ near a hypothetical defect, after the elimination of Axiom 1. A DefectSensor records the charge (multiplicity of the zero of $ζ$), the real part of its location, and the requirement that the zero lies in the right half of the critical strip. DefectSampledFamily is the structure consisting of a sensor, a function assigning an AnnularMesh at each depth $N$, and the charge_spec axiom ensuring every mesh carries the sensor charge.
proof idea
One-line wrapper that applies the toSampledFamily conversion to the output of chosenDefectPhaseFamily sensor hm.
why it matters
This definition is the central object fed into the refined Axiom 2 attack. It is used by canonicalDefectSampledFamily_charge to confirm the charge, by canonicalDefectSampledFamily_excess_bounded to obtain bounded excess, and by defect_annular_cost_bounded_inconsistent in EulerInstantiation to derive a contradiction from the assumption of bounded annular cost for nonzero charge. The module documentation states that any uniform upper bound on the cost of this realized sampled family contradicts annular coercivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.