ringCost
plain-language theorem explainer
ringCost sums phiCost over the 8n angular increments of an AnnularRingSample. Workers on the RS annular coercivity theorems cite it to accumulate ring-level J-cost before summing to total annularCost. The definition is a direct summation that passes convexity and lower bounds from phiCost straight through.
Claim. Let $s$ be an annular ring sample on ring $n$ with increments $Δ_j$ obeying the winding constraint $∑ Δ_j = -2π m$. Its ring cost equals $∑_j φ$-cost$(Δ_j)$, where $φ$-cost $u := cosh((log φ) u) - 1$.
background
The Annular J-Cost Framework defines phiCost u as cosh((log φ)·u) − 1, identical to J(φ^u). AnnularRingSample n packages 8n real increments together with an integer winding m whose constraint forces the sum of increments to equal −2π m. This machinery supports the topological cost-covering bridge. Upstream results supply the convexity of phiCost and the structure of J-cost minimization from PhysicsComplexityStructure.
proof idea
The definition is a one-line wrapper that applies summation to phiCost on each increment of the sample.
why it matters
ringCost supplies the per-ring term for annularCost and enters annular_coercivity to produce the Θ(m² log N) lower bound. It realizes the ring-level J-cost in the annular sampling layer of Recognition Science, directly supporting Jensen ring bounds and topological floor comparisons. The construction leaves open the explicit trace family for holomorphic carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.