ring_coercivity
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when winding number is zero.
- Does not supply matching upper bounds or equality cases.
- Does not address interactions across multiple concentric rings.
- Does not fix the discrete rung k that determines kappa.
Lean usage
have hring := ring_coercivity hn sformal statement (Lean)
368theorem ring_coercivity {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
369 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤ ringCost s := by
proof body
Tactic-mode proof.
370 let u : ℝ := -(2 * Real.pi * s.winding) / (8 * n : ℝ)
371 have hphi := phiCost_quadratic_lb u
372 have hmul :=
373 mul_le_mul_of_nonneg_left hphi (by positivity : 0 ≤ (8 * n : ℝ))
374 have hleft :
375 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤
376 (8 * n : ℝ) * phiCost u := by
377 have hcalc :
378 (8 * n : ℝ) * (kappa * u ^ 2 / 2) =
379 Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) := by
380 dsimp [u]
381 field_simp [show (8 * n : ℝ) ≠ 0 by positivity]
382 ring
383 rw [← hcalc]
384 exact hmul
385 exact hleft.trans (jensen_ring_bound hn s)
386
387/-- The topological floor: minimum possible cost for charge m on ring n. -/