canonicalDefectSampledFamily_charge
plain-language theorem explainer
Every mesh in the canonical defect sampled family attached to a nonzero-charge sensor preserves that exact charge. Number theorists refining the Axiom 2 attack on zeta defects cite this to guarantee the realized family remains charge-consistent under refinement. The proof is a one-line simplification that invokes the sensor definition and the family's charge specification.
Claim. Let $s$ be a defect sensor with nonzero charge $q$. For every natural number $N$, the charge of the mesh at depth $N$ in the canonical sampled family attached to $s$ equals $q$.
background
The Defect Sampled Trace module constructs realized annular meshes for phase-sampling a hypothetical zeta defect after Axiom 1 is removed. The remaining bottleneck is Axiom 2: prior statements quantified over all AnnularMesh values with given charge, which is stronger than needed. The module therefore isolates the canonical sampled family drawn from the phase of $ζ^{-1}$ near the defect. DefectSampledFamily packages a full refinement family of realized meshes; canonicalDefectSampledFamily selects the concrete family attached to a given sensor. Upstream results supply the underlying cost structures (J-cost from ObserverForcing and MultiplicativeRecognizerL4) and ledger factorization (DAlembert.LedgerFactorization.of) used to define the meshes.
proof idea
One-line wrapper that applies simpa with the canonicalDefectSampledFamily_sensor definition, then directly invokes the charge_spec of the family at level N.
why it matters
The result guarantees charge preservation inside the canonical family, which is the input to the downstream ringPerturbationControl definition that quantifies the Axiom 2 attack via local factorization $ζ^{-1}=(z-ρ)^{-m}g(z)$. It supplies the realizable replacement for arbitrary-mesh quantification required by the refined bounded-cost proposition in this module, advancing the Recognition Science number-theory layer toward a uniform cost bound on the sampled family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.