mkSampledMesh_charge_zero
plain-language theorem explainer
mkSampledMesh_charge_zero shows that a sampled mesh built from a zero-winding certificate has zero winding on every ring. Researchers bridging continuous contour winding to discrete annular cost models cite it to confirm charge neutrality after sampling. The proof is a direct one-line projection onto the charge_zero field of the constructed mesh.
Claim. Let cert be a zero-winding certificate and let $N$ be a natural number. Then for every ring index $n$, the winding number of the $n$-th ring in the sampled mesh constructed from cert and $N$ equals zero.
background
The Sampled Traces module bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing records phase increments sampled at 8n equispaced points on a circle, with winding taken from the contour layer. SampledMesh assembles N concentric rings into an annular mesh using the schedule with radius proportional to n/(N+1) and 8n angular samples per ring n.
proof idea
The proof is a term-mode one-liner that returns the charge_zero field of the object produced by the sampled-mesh construction from the given zero-winding certificate. This field is supplied directly by the mesh definition once the certificate is supplied.
why it matters
The result supplies the zero-charge property required by the bridge theorems to AnnularTrace in the same module, including the sampledTraceToAnnularTrace_charge_zero sibling. It realizes the module's key claim that a zero-winding certificate produces a charge-neutral discrete mesh, preserving the topological neutrality built into the J-cost and eight-tick structures of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.