DefectSampledFamily
A structure that bundles a defect sensor with a family of annular meshes indexed by depth N, each mesh carrying exactly the sensor charge and realized from phase sampling of ζ^{-1}. Analysts refining the cost bound for hypothetical zeta defects in Recognition Science cite this to replace quantification over arbitrary meshes with a concrete sampled family. The definition is a direct structure whose fields are populated by the defectAnnularMesh constructor and its charge preservation lemma.
claimLet $s$ be a defect sensor recording the multiplicity of a zero of $ζ$. A DefectSampledFamily consists of $s$, a map $m:ℕ→$AnnularMesh such that each $m(N)$ is an annular mesh of $N$ rings, and the condition that the charge of $m(N)$ equals the charge of $s$ for every $N$.
background
The Defect Sampled Trace module packages realized annular meshes attached to the phase-sampling construction for a hypothetical zeta defect. After Axiom 1 is eliminated, Axiom 2 remains the bottleneck. Earlier statements quantified over every AnnularMesh with matching charge, but the analytic claim only requires bounding the cost of the canonical family sampled from the phase of ζ^{-1} near the defect.
proof idea
The structure is introduced by its three fields: the sensor, the mesh map, and the charge equality. The accompanying toSampledFamily constructor on DefectPhaseFamily sets the sensor directly, populates the mesh field via defectAnnularMesh, and satisfies the charge specification via defectAnnularMesh_charge. This is a one-line wrapper that applies the annular mesh sampling function and its charge lemma.
why it matters in Recognition Science
DefectSampledFamily supplies the input type for canonicalDefectSampledFamily, defectSampledFamily_unbounded, and not_realizedDefectAnnularCostBounded. The unbounded theorem shows nonzero charge forces annular cost to diverge with N, supplying the contradiction for the refined Axiom 2. It is used in carrier budget comparisons and annular excess bounds, tightening the link between the meromorphic phase construction and cost divergence in the Recognition framework.
scope and limits
- Does not assert existence of a phase family for an arbitrary sensor.
- Does not supply any upper bound on annular cost.
- Does not decompose cost into topological floor plus regular error.
- Does not address convergence of phase data under mesh refinement.
Lean usage
def useSite (dpf : DefectPhaseFamily) : DefectSampledFamily := dpf.toSampledFamilyformal statement (Lean)
60structure DefectSampledFamily where
61 sensor : DefectSensor
62 mesh : ∀ N : ℕ, AnnularMesh N
63 charge_spec : ∀ N : ℕ, (mesh N).charge = sensor.charge
64
65/-- Convert a `DefectPhaseFamily` to its realized sampled annular family. -/
66def DefectPhaseFamily.toSampledFamily (dpf : DefectPhaseFamily) :
67 DefectSampledFamily where
68 sensor := dpf.sensor
proof body
Definition body.
69 mesh := defectAnnularMesh dpf
70 charge_spec := defectAnnularMesh_charge dpf
71
72/-- Choose one phase family attached to a hypothetical defect sensor.
73
74This uses the strengthened existential package
75`defect_phase_family_with_perturbation_exists`, so the chosen family comes with
76the perturbation witness needed downstream for the annular excess argument. -/
used by (16)
-
defect_cost_exceeds_carrier_budget -
annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError -
canonicalDefectSampledFamily -
DefectPhaseFamily -
defectSampledFamily_unbounded -
not_realizedDefectAnnularCostBounded -
RealizedDefectAnnularCostBounded -
RealizedDefectAnnularExcessBounded -
realizedDefectAnnularExcessBounded_of_costBounded -
realizedDefectAnnularExcessBounded_of_ringRegularErrorBound -
realizedDefectCostBounded_iff_charge_zero_and_excessBounded -
realizedDefectCostBounded_of_charge_zero_and_excessBounded -
realizedRingPerturbationError -
RingPerturbationControl -
RingRegularErrorBound -
ringRegularErrorBound_of_ringPerturbationControl