ringCost
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not verify the winding constraint.
- Does not bound the cost from above.
- Does not incorporate radial cost terms.
- Does not specialize to uniform increments.
formal statement (Lean)
305noncomputable def ringCost {n : ℕ} (s : AnnularRingSample n) : ℝ :=
proof body
Definition body.
306 ∑ j, phiCost (s.increments j)
307
308/-- An annular mesh of N concentric rings. -/
used by (12)
-
annular_coercivity -
annularCost -
jensen_ring_bound -
ring_coercivity -
ringCost_ge_topologicalFloor -
ringCost_le_topologicalFloor_add_linear_quadratic_error -
uniformRingSample_cost_eq_topologicalFloor -
annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError -
RingRegularErrorBound -
ringRegularErrorBound_of_ringPerturbationControl -
zetaDerivedPhaseFamily_excess_zero -
sampledTraceToAnnularTrace_excess_zero