phiCost_quadratic_lb
plain-language theorem explainer
A quadratic lower bound holds for the phi-weighted cost: kappa u squared over 2 is at most cosh((log phi) u) minus 1 for any real u. Coercivity arguments in the annular J-cost framework cite this estimate to control ring costs from winding numbers. The tactic proof reduces via substitution t equals log phi times u to the standard cosh inequality, handling signs separately with sinh bounds and double-angle identities.
Claim. For every real number $u$, $k u^2/2$ is at most $cosh((log phi) u) - 1$, where $k = (log phi)^2$.
background
In the Annular J-Cost Framework the phi-weighted cost is defined as cosh((log phi) u) minus 1 and equals the J-cost evaluated at phi to the power u. This supplies the cost function for annular sampling on concentric rings, enabling Jensen-based coercivity estimates that force quadratic growth in winding number. The constant kappa equals (log phi) squared so that the bound reads kappa u squared over 2 at most the cost function. The upstream result Jlog_as_cosh certifies Jlog t equals cosh t minus 1, which underpins the identification with the core J functional.
proof idea
Unfolding kappa and the cost function reduces the goal to t squared over 2 at most cosh t minus 1 with t defined as log phi times u. Nonnegativity of the left side is immediate. Case analysis on the sign of t applies the self_le_sinh_iff lemma to obtain sinh(x) at least x for the halved argument, followed by squaring and the identity cosh t minus 1 equals 2 sinh(t/2) squared obtained from cosh_two_mul and cosh_sq. Nlinarith closes each branch, with the negative case reduced to the positive one by evenness of cosh.
why it matters
The result is invoked by ring_coercivity to obtain the explicit lower bound pi squared kappa m squared over 4 n on ring cost for nonzero winding m. It also supports topologicalFloor_pos_of_charge_ne_zero by ensuring the floor is positive. In the Recognition Science framework this fills the quadratic coercivity step in the annular layer, advancing the topological cost-covering bridge that connects to the phi-ladder, the eight-tick octave, and spatial dimension D equals 3. The module doc notes that the annular layer is now formalized constructively except for the concrete trace family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.