jcost_upper_bound_at_geq_one
plain-language theorem explainer
For real r at least 1 the J-cost satisfies J(r) ≤ (r-1)^2 / 2. Cross-domain arguments on J-convexity universality cite the bound to control quadratic growth away from the r=1 minimum. The argument rewrites the cost via the squared algebraic identity and compares the denominators 2r and 2 using a division monotonicity step.
Claim. For every real number $r$ with $r ≥ 1$, the J-cost satisfies $J(r) ≤ (r-1)^2 / 2$.
background
Module C25 establishes J-cost convexity on (0, ∞) with a global minimum of zero at r=1. The central algebraic identity is the squared form J(r) = (r-1)^2 / (2r), already proved in Foundation.JCostGeometry and reused in Information.PhysicsComplexityStructure and CrossDomain.JConvexityUniversality. This form makes the leading-order quadratic sensitivity coefficient 1/2 explicit near equilibrium.
proof idea
The proof applies the upstream squared-form theorem jcost_squared_form to replace Jcost r by (r-1)^2 / (2r). It then records nonnegativity of the numerator and the comparison 2r ≥ 2, then invokes div_le_div_of_nonneg_left to finish the inequality.
why it matters
The bound is assembled into the JConvexityUniversalityCert definition together with the squared form, sensitivity_at_one and universalSensitivity_eq. It supplies the local quadratic approximation that fixes the universal sensitivity constant of 1/2 referenced in the module documentation for the C25 wave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.