ring_coercivity
plain-language theorem explainer
The ring_coercivity theorem supplies a quadratic lower bound on the J-cost of a single annular ring carrying nonzero winding m on a ring of size n. Researchers deriving total annular coercivity or topological floors in the Recognition Science framework cite it when summing per-ring estimates. The proof defines a scaled argument u from the winding, invokes the quadratic lower bound on phiCost, multiplies through by the positive factor 8n, and chains the result via the Jensen ring bound.
Claim. For positive integer $n$ and annular ring sample $s$ with winding number $m$, $$frac{pi^2 kappa m^2}{4n} leq text{ringCost}(s),$$ where ringCost sums phiCost over the $8n$ phase increments of $s$ and $kappa$ is the conductivity parameter drawn from the phi-ladder.
background
The annular J-cost framework defines phiCost(u) := cosh((log phi) u) - 1, equivalently J(phi^u). An AnnularRingSample(n) is a structure holding 8n real phase increments whose sum equals -2 pi times the integer winding number. kappa is the conductivity parameter kappa(k) := phi^k taken from the thermal regimes on the phi-ladder. Upstream results establish that recognition-event cost equals J-cost and that net winding on the eight-tick clock is the signed sum of directional steps.
proof idea
Define u := -(2 pi m)/(8 n). Apply phiCost_quadratic_lb to obtain the quadratic lower bound on phiCost(u). Multiply both sides by the positive quantity 8n. Verify by direct field_simp and ring that the resulting left-hand side equals the target pi^2 kappa m^2/(4n). Conclude by transitivity with jensen_ring_bound.
why it matters
The result is the immediate parent of annular_coercivity, which sums the per-ring bounds to produce the harmonic divergence Theta(m^2 log N) for total annular cost. It supplies the ring-level coercivity step inside the annular J-cost framework, linking the eight-tick octave (via the 8n increments) to the phi-ladder constants and the topological floor for nonzero charge. The module doc notes that the annular layer is now fully formalized constructively except for the concrete trace-family construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.