canonicalDefectSampledFamily_charge
The theorem states that every mesh in the canonical defect sampled family attached to a nonzero-charge sensor preserves that exact charge at every refinement level N. Researchers attacking the refined Axiom 2 via realized zeta-defect families cite it to enforce charge consistency before bounding annular excess. The proof is a one-line term wrapper that substitutes the canonical sensor definition and invokes the family's charge specification.
claimLet $S$ be a defect sensor with nonzero charge $q$. Let $F$ be the canonical sampled family of realized annular meshes attached to $S$. Then for every natural number $N$, the charge of the mesh at level $N$ in $F$ equals $q$.
background
The Defect Sampled Trace module constructs realized annular meshes for a hypothetical zeta defect after Axiom 1 is eliminated. Its central objects are DefectSampledFamily, a full refinement family of realized meshes, and canonicalDefectSampledFamily, the specific family chosen from the phase of ζ^{-1} near the defect. The module documentation notes that the prior quantification over all AnnularMesh values was too strong; only the canonical sampled family needs cost bounds to bridge to annular coercivity.
proof idea
The proof is a one-line term-mode wrapper. It first unfolds the canonical family via the sensor definition, then directly applies the charge_spec property of that family at the given level N.
why it matters in Recognition Science
This charge-preservation result is a prerequisite for the downstream canonicalDefectSampledFamily_ringPerturbationControl, which targets bounded excess above the topological floor for the realized family. That control object is the quantitative target for the refined Axiom 2 attack, relying on local factorization of ζ^{-1} together with log-derivative bounds on the regular factor. It supports the module's key bridge: nonzero charge still forces cost to infinity under annular coercivity.
scope and limits
- Does not prove any upper bound on annular cost.
- Does not apply when sensor charge is zero.
- Does not quantify over arbitrary AnnularMesh objects, only the canonical sampled family.
- Does not address perturbation control or excess bounds.
formal statement (Lean)
107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)
108 (hm : sensor.charge ≠ 0) (N : ℕ) :
109 ((canonicalDefectSampledFamily sensor hm).mesh N).charge = sensor.charge := by
proof body
Term-mode proof.
110 simpa [canonicalDefectSampledFamily_sensor sensor hm] using
111 ((canonicalDefectSampledFamily sensor hm).charge_spec N)
112
113/-! ### §3. Refined bounded-cost proposition -/
114
115/-- The annular cost of a realized sampled family is bounded independently of
116mesh refinement. This is the realizable replacement for the previous
117over-strong quantification over arbitrary `AnnularMesh` values. -/