SampledRing
plain-language theorem explainer
SampledRing packages data for a discrete ring at level n sampled at 8n equispaced points: complex center, positive radius, real increments, and integer winding fixed to zero by the contour constraint. Researchers discretizing traces for annular cost models in Recognition Science cite this when moving from continuous winding to the mesh framework. The definition is a structure that directly encodes the zero-winding condition as a field.
Claim. A structure for level $n$ consists of center $c$ in the complex plane, radius $r>0$, increments given by a map from the $8n$ sample indices to reals, winding integer $w$, satisfying the sum of increments equals $-2$ times pi times $w$, and with $w$ required to be zero.
background
The Sampled Traces module bridges the continuous contour-winding layer to the discrete AnnularRingSample and AnnularMesh cost framework. SampledRing collects phase increments from evaluating a function at equispaced points on a circle of given radius, with the winding number taken from the contour layer. The module uses the canonical schedule of ring level n (1-indexed) at radius proportional to n, with exactly 8n angular samples to match the annular convention.
proof idea
This is a structure definition that directly packages the geometric data and the zero-winding constraint as a field. The toAnnularRingSample projection copies the increments and winding while inheriting the zero constraint. Accompanying theorems are one-line wrappers that read the winding_from_contour field.
why it matters
SampledRing is the atomic object feeding SampledMesh and the sampledTraceToAnnularTrace bridge, which establish that annular excess is zero on every mesh. It aligns with the eight-tick octave by using 8n samples and supports the zero-charge results required for the cost-covering theorems in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.