mkSampledMesh
plain-language theorem explainer
The construction assembles a mesh of N concentric rings from a zero-winding certificate by placing each ring at half the certificate radius using uniform zero phase increments. Researchers bridging continuous contour integrals to discrete annular cost models cite this when building zero-charge sampled traces. The definition proceeds by direct invocation of the individual ring constructor at each level together with a reflexivity proof for the charge condition.
Claim. Let $C$ be a zero-winding certificate with radius $R > 0$. For natural number $N$, the sampled mesh of depth $N$ is the structure whose rings component sends each index $n = 0, ..., N-1$ to the sampled ring of level $n+1$ at radius $R/2$, together with the uniform zero-winding condition on every ring.
background
SampledTrace bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework. A sampled mesh of depth N consists of N concentric sampled rings, each carrying zero winding, as captured by the structure whose rings field maps Fin N indices to SampledRing objects of level n.val + 1 and whose charge_zero field asserts that every such ring has winding zero. ZeroWindingCert supplies the upstream interface: a center, positive radius R, and matching ComplexCarrierCert guaranteeing zero winding around every interior circle. The sibling ring constructor builds each individual ring from the certificate at a chosen level and radius strictly less than R, using uniform zero increments because the net phase change is zero.
proof idea
The definition is a direct structure constructor. It populates the rings field by mapping each Fin N index n to the ring constructor applied at level n.val + 1 with radius equal to the certificate radius divided by 2, supplying the level positivity via Nat.succ_pos and the radius bounds via linarith. The charge_zero field is instantiated as the constant function returning reflexivity, since each ring produced by the zero-winding ring constructor already satisfies winding zero.
why it matters
This definition supplies the concrete zero-charge mesh consumed by sampledTraceToAnnularTrace to produce an AnnularTrace from any zero-winding certificate, completing the module's bridge from cert to the annular cost framework. It directly enables the charge-zero theorem and the excess-zero result for annular traces listed in the module documentation. Within the Recognition framework it realizes the discrete sampling step that connects contour certificates to the cost-covering bridge, using the canonical schedule of 8n equispaced points per ring n.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.