SampledMesh
plain-language theorem explainer
SampledMesh defines an N-level collection of concentric sampled rings, each required to carry zero winding. Workers constructing discrete meshes from zero-winding certificates cite it when moving from contour data to the annular cost framework. The declaration is a plain structure with two fields that directly encode the uniform zero-charge condition.
Claim. A sampled mesh of level $N$ consists of a family of sampled rings $r_n$ ($n=0$ to $N-1$), where each $r_n$ is a sampled ring of level $n+1$, together with the condition that the winding number of every ring equals zero.
background
The SampledTrace module bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing is the sibling structure: a sampled ring on level $n$ with $8n$ equispaced points whose winding number is inherited from the contour layer and constrained to satisfy the sum of phase increments equaling $-2π$ times the winding. SampledMesh assembles $N$ such rings into an annular mesh with uniform charge zero. The module doc states that the canonical schedule places ring $n$ at radius $R·n/(N+1)$ using $8n$ angular samples to match the AnnularRingSample convention.
proof idea
This is a structure definition. The two fields are introduced directly: the dependent function rings mapping each Fin N index to a SampledRing at level n.val+1, and the charge_zero predicate asserting that every such ring has winding zero. No tactics or lemmas are applied.
why it matters
SampledMesh supplies the discrete mesh object required by mkSampledMesh, which builds it from a ZeroWindingCert using fixed radius R/2, and by sampledTraceToAnnularTrace_excess_zero, which shows the annular excess vanishes because each ring saturates the topological floor at zero. It therefore completes the sampling bridge that respects the eight-tick octave convention (8n points) inside the Recognition Science cost-covering layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.