DefectSampledFamily
plain-language theorem explainer
DefectSampledFamily records a defect sensor together with a family of annular meshes whose charges are forced to match the sensor at every depth N. Researchers refining the zeta-defect argument cite the structure when they must replace quantification over arbitrary meshes by the specific family obtained from phase sampling of zeta inverse. The declaration is a plain record type whose three fields directly encode the sensor, the mesh map, and the charge-consistency condition.
Claim. Let $S$ be a defect sensor (charge $m$ and real part of a zero of $zeta$). A DefectSampledFamily consists of $S$, a map $N mapsto M_N$ where each $M_N$ is an annular mesh of $N$ rings, and equalities asserting that the charge of every $M_N$ equals $m$.
background
The Defect Sampled Trace module replaces an overly strong quantification over all AnnularMesh values by the concrete family arising from phase sampling of $zeta^{-1}$ near a hypothetical defect. A DefectSensor records the multiplicity $m$ of a zero of $zeta$ together with its real part inside the critical strip. An AnnularMesh of depth $N$ consists of $N$ concentric ring samples that all carry the same winding number (charge). DefectPhaseFamily supplies the sensor, a positive witness radius, and a phaseAtLevel map that produces ContinuousPhaseData whose charge is uniform and equal to the sensor charge.
proof idea
The declaration is a structure definition. The companion function DefectPhaseFamily.toSampledFamily constructs an instance by copying the sensor field and delegating the mesh and charge_spec fields to the lemmas defectAnnularMesh and defectAnnularMesh_charge.
why it matters
This structure supplies the central object for the refined Axiom 2. It is used to define canonicalDefectSampledFamily, to prove defectSampledFamily_unbounded (nonzero charge forces annular cost to infinity), and to reach the contradiction in not_realizedDefectAnnularCostBounded. The parent theorem defect_cost_exceeds_carrier_budget applies it to show defect cost exceeds any fixed carrier budget. It directly implements the module requirement to bound the cost of the canonical sampled family coming from the phase of $zeta^{-1}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.