AnnularMesh
plain-language theorem explainer
An annular mesh of N concentric rings packages a family of ring samples each carrying identical integer winding m together with the uniform charge constraint. Researchers on the RS topological cost-covering bridge cite this structure when deriving Jensen coercivity bounds of order m² log N. The declaration is a pure structure definition that assembles the rings, charge, and uniformity predicate with no lemmas or computation.
Claim. An annular mesh of $N$ concentric rings consists of a family of samples $r_n$ ($n=0,…,N-1$), where each $r_n$ is an annular ring sample on ring $n+1$ with $8n$ phase increments summing to $-2π m$, an integer charge $m$, and the predicate that every ring has winding number exactly $m$.
background
The module sets up the annular J-cost framework in which phiCost u is defined as cosh((log φ)·u)−1, equivalently J(φ^u). AnnularRingSample(n) is the structure holding 8n real increments whose sum equals −2π times the winding integer. Upstream cost is the J-cost derived from multiplicative recognizers and from recognition events; winding extracts net torsion from eight-tick clock words.
proof idea
The declaration is a structure definition. It introduces the rings field as a dependent function from Fin N into AnnularRingSample, the charge field as an integer, and the uniform_charge field as the predicate that every ring sample carries exactly that charge. No tactics or lemmas are invoked.
why it matters
AnnularMesh is the central input type for annularCost (the sum of ring costs), annularExcess, and the coercivity theorem annular_coercivity that establishes Θ(m² log N) divergence for nonzero charge. It realizes the annular sampling layer of the Recognition Science framework, supporting the topological cost-covering bridge, Jensen ring bounds, and the trace-based carrier-budget interface. The remaining open question is the concrete construction of an AnnularTrace family for a holomorphic carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.