jensen_ring_bound
plain-language theorem explainer
The theorem establishes a Jensen lower bound on ringCost for an AnnularRingSample using convexity of phiCost. Researchers deriving coercivity estimates for topological winding in Recognition Science cite it to obtain the exact floor before applying quadratic bounds. The proof constructs uniform weights summing to one over the 8n increments, invokes the convexity map_sum_le lemma, matches the average to the winding constraint, and scales the resulting inequality by 8n.
Claim. For positive integer $n$ and annular ring sample $s$ with $8n$ phase increments summing to $-2$ times $2$ times pi times the integer winding number of $s$, one has $8n$ times phiCost of the average increment $-(2$ times pi times winding of $s)/(8n)$ is at most the ring cost of $s$, where phiCost$(u)$ equals cosh of (log phi) times $u$ minus 1.
background
The Annular J-Cost Framework in NumberTheory.AnnularCost defines phiCost u as cosh((log phi) u) - 1, equivalently J(phi^u) with J the recognition cost from the forcing chain. An AnnularRingSample n is the structure holding a Fin(8*n) array of real increments together with an integer winding whose sum constraint equals -(2 pi winding). The module formalizes the phi-weighted cost and annular sampling machinery for the RS topological cost-covering bridge, with Jensen-based coercivity as the central tool. Upstream results include the convexity property phiCost_convexOn and cost definitions from ObserverForcing and MultiplicativeRecognizerL4.
proof idea
The tactic proof first obtains positivity of 8n and defines uniform weights w_i = 1/(8n). It verifies nonnegativity and that the weights sum to one via Finset.sum_const and field_simp. The map_sum_le lemma from phiCost_convexOn is applied to the increments. The weighted average is rewritten via the winding_constraint to equal the target argument of phiCost. The weighted sum of phiCost values is identified with ringCost s divided by 8n. The inequality is scaled by 8n using mul_le_mul_of_nonneg_left and finished by field_simp.
why it matters
This supplies the precise Jensen lower bound renamed topologicalFloor and used directly by ringCost_ge_topologicalFloor. It enables the downstream ring_coercivity theorem that extracts the quadratic floor pi squared kappa m squared over 4n for nonzero winding m. Within the Recognition Science framework it completes the annular layer formalization that converts topological winding into cost coercivity, supporting the J-uniqueness step and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.