DefectSampledFamily
plain-language theorem explainer
DefectSampledFamily bundles a single defect sensor with a family of annular meshes indexed by refinement depth N, enforcing that every mesh carries exactly the sensor charge. Number theorists refining Axiom 2 bounds on zeta-defect costs cite the structure to replace quantification over arbitrary meshes with canonical phase-sampled ones. The definition is a direct structure constructor that delegates mesh construction and charge uniformity to defectAnnularMesh and defectAnnularMesh_charge.
Claim. A structure consisting of a defect sensor $s$ (integer charge $m$, real part in the critical strip) together with a map $Nmapsto M_N$ such that each $M_N$ is an annular mesh of $N$ concentric rings whose uniform winding number equals $m$.
background
The Defect Sampled Trace module packages realized annular meshes that arise from the phase-sampling construction for a hypothetical pole of $ζ^{-1}$. An AnnularMesh $N$ comprises $N$ rings, each an AnnularRingSample, plus an integer charge required to be identical on every ring. A DefectSensor records the multiplicity $m$ of the underlying zero together with its real part. Upstream, DefectPhaseFamily supplies continuous phase data at each level whose charge matches the sensor, together with a positive witness radius. The module doc states that this layer is required once Axiom 1 is eliminated, because the remaining bottleneck (Axiom 2) demands bounds only on the canonical sampled family rather than on every synthetic mesh of matching charge.
proof idea
The definition is a one-line wrapper. It sets the sensor field to the input DefectPhaseFamily sensor, populates the mesh field by applying defectAnnularMesh to the input, and satisfies the charge_spec field by applying defectAnnularMesh_charge to the same input.
why it matters
The structure supplies the concrete object on which the refined Axiom 2 argument operates. It is the type of the canonicalDefectSampledFamily definition and the input to defectSampledFamily_unbounded, which shows that nonzero charge forces annular cost to diverge with $N$. That divergence immediately yields not_realizedDefectAnnularCostBounded, the contradiction theorem that no uniform upper bound on realized cost can exist. The construction therefore replaces the earlier over-strong quantification over all AnnularMesh values and closes the analytic gap between synthetic meshes and the actual meromorphic factorization near a defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.