mkSampledRing
plain-language theorem explainer
mkSampledRing constructs a SampledRing at level n from a ZeroWindingCert by setting the center to the cert center, radius to the supplied r, all phase increments to zero, and winding to zero. Researchers assembling zero-charge annular meshes in the Recognition Science sampled-trace layer cite this constructor when building discrete approximations from contour certificates. The definition is a direct structure instantiation that discharges the winding constraint by simplification and reflexivity.
Claim. Given a zero-winding certificate $cert$, positive integer $n$, and radius $r$ with $0 < r < cert.radius$, the map $mkSampledRing(cert, n, r)$ produces a sampled ring whose center equals the certificate center, radius equals $r$, phase increments are the zero function on $8n$ points, and winding number is zero.
background
SampledRing is the structure that records a center in the complex plane, a positive radius, a function assigning phase increments to each of the $8n$ equispaced sample points on the circle, and an integer winding number whose value must satisfy the discrete contour-integral constraint that the sum of increments equals minus twice pi times the winding. The Sampled Traces module bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework by supplying canonical sampling schedules that use exactly $8n$ points per ring level. ZeroWindingCert supplies the center and radius together with the topological guarantee of zero net contour winding, which forces the uniform zero increments used here.
proof idea
The definition is a direct structure constructor for SampledRing that sets center to cert.center, radius to the input r, increments to the constant-zero function, and winding to zero; the winding_constraint is discharged by simp and winding_from_contour by reflexivity.
why it matters
This definition supplies the atomic constructor used by mkSampledMesh to assemble full sampled meshes from any ZeroWindingCert and by the theorem sampledTraceToAnnularTrace_excess_zero that proves annular excess vanishes identically. It implements the sampling schedule step that converts a zero-winding contour certificate into a discrete object compatible with the annular cost framework, consistent with the eight-tick octave sampling convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.