AnnularRingSample
plain-language theorem explainer
AnnularRingSample defines a structure holding 8n real phase increments on a ring indexed by n together with an integer winding number whose sum is fixed to equal minus two pi times the winding. Researchers formalizing J-cost coercivity and topological floors in Recognition Science cite this when assembling annular meshes or applying Jensen bounds. The definition is a direct structure declaration whose only content is the three fields and the explicit summation constraint.
Claim. An annular ring sample for natural number $n$ consists of a function assigning a real increment to each of the $8n$ angular positions together with an integer winding $m$ such that the sum of all increments equals $-2π m$.
background
The Annular J-Cost Framework equips the Recognition Science cost-covering bridge with phiCost u defined as cosh((log φ)·u) − 1, equivalently J(φ^u). Annular samples are collections of phase increments placed on concentric rings; the module certifies Jensen-based coercivity showing nonzero winding forces quadratic cost growth and supplies the carrier-budget interface. This structure is the basic object on which ringCost is defined as the sum of phiCost over the increments and on which the topological floor is later imposed.
proof idea
Structure definition introducing the three fields (increments map, winding integer, and the summation constraint) with no further computation or proof obligations.
why it matters
AnnularRingSample is the foundational type for AnnularMesh (which stacks N such rings with uniform charge) and for the downstream theorems jensen_ring_bound, ring_coercivity, ringCost_ge_topologicalFloor and ringCost_le_topologicalFloor_add_linear_quadratic_error. It supplies the annular sampling layer required by the RS topological cost-covering bridge and the phi-weighted cost machinery. The module documentation notes that the remaining open task is the concrete trace family for the analytic carrier together with its matching excess bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.