defectAnnularMesh_charge
plain-language theorem explainer
The charge of the annular mesh sampled from a DefectPhaseFamily at depth N equals the charge recorded by its sensor. Analysts refining the cost bound on the canonical sampled family for Axiom 2 cite this equality to ensure the realized mesh carries the correct total charge. The proof is immediate reflexivity on the definition of defectAnnularMesh.
Claim. Let $dpf$ be a DefectPhaseFamily and $N$ a natural number. The total charge of the annular mesh obtained by sampling $dpf$ at depth $N$ equals the charge of the sensor attached to $dpf$.
background
The module constructs realized annular meshes from the phase-sampling construction for a hypothetical zeta defect, replacing quantification over all meshes of given charge with a concrete family. DefectPhaseFamily packages one such realized family attached to a single defect sensor; defectAnnularMesh extracts the mesh at a chosen depth $N$ from that family. The local setting is the refined Axiom 2 argument: any uniform upper bound on the cost of this canonical sampled family would contradict annular coercivity. Upstream, the defect functional equals $J$ on positive reals, the eight-tick phase supplies the discrete sampling angles, and the LedgerFactorization calibrates the underlying $J$-cost.
proof idea
The proof is a one-line wrapper that applies reflexivity. It follows directly from the definition of defectAnnularMesh, which sets the charge field of the constructed mesh equal to the sensor charge by construction.
why it matters
This equality is invoked by the parent declaration DefectPhaseFamily to guarantee that every mesh in the realized family carries the sensor charge. It supplies the missing link between the phase-sampling construction and the later theorem that nonzero charge forces the cost of the sampled family to diverge, thereby tightening the bridge to the refined Axiom 2. The step relies on the eight-tick octave and the defect functional from the Law of Existence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.