SampledMesh
plain-language theorem explainer
SampledMesh assembles N concentric sampled rings, each forced to winding number zero. Researchers building discrete zero-charge traces for annular cost calculations in Recognition Science cite the structure when converting contour data to the mesh layer. The definition is a direct record whose single constraint propagates the zero-winding property from each SampledRing.
Claim. A sampled mesh of size $N$ consists of a map sending each index $n$ in the finite set of size $N$ to a sampled ring of level $n+1$ together with the requirement that every such ring has winding number zero.
background
The Sampled Traces module bridges continuous contour winding to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing stores a center, positive radius, 8n phase increments on equispaced points, and an integer winding whose value satisfies the sum of increments equaling minus twice pi times the winding, with the winding inherited from the contour layer. SampledMesh aggregates N such rings under the uniform charge-zero constraint. The module adopts the canonical schedule of 8n samples per ring n at radii scaled inside the disk, matching the AnnularRingSample convention.
proof idea
The structure is introduced by direct field declaration. The accompanying toAnnularMesh conversion is a one-line wrapper that maps each ring through toAnnularRingSample, sets charge to zero, and discharges uniform_charge by simp together with the charge_zero hypothesis.
why it matters
SampledMesh supplies the target type for mkSampledMesh, which builds the mesh from a ZeroWindingCert at fixed radius R/2, and for sampledTraceToAnnularTrace_excess_zero, which shows annular excess vanishes because uniform zero increments saturate the topological floor. It completes the sampled-to-annular bridge inside the module and aligns with the Recognition Science eight-tick sampling schedule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.