jcost_squared_form
plain-language theorem explainer
The declaration establishes the algebraic identity expressing J-cost as the squared deviation ratio (x-1)^2/(2x) for nonzero real x. Researchers deriving convexity bounds or complexity certificates in Recognition Science cite this form for explicit calculations. The proof is a direct one-line application of the core expansion lemma Jcost_eq_sq.
Claim. For every real number $x$ with $x ≠ 0$, the J-cost satisfies $J(x) = (x-1)^2 / (2x)$.
background
Module F1 develops the log-domain geometry of the canonical reciprocal cost J(x) = ½(x + x^{-1}) - 1. The squared form isolates the deviation from the equilibrium point x = 1. This module re-exports and extends core identities from JcostCore to support the foundation paper's results on geometric-mean optimality and simultaneous versus sequential descent.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_eq_sq from the Cost module, passing the hypothesis x ≠ 0 directly.
why it matters
This identity supplies the squared_form field in jConvexityUniversalityCert and appears verbatim in the IC-005 certificate for physics complexity classes. It realizes proposition F1.1.8 of the foundation paper, enabling downstream upper bounds for r ≥ 1 and strict positivity away from x = 1. The form is used in the Recognition Science framework to make J-cost convexity explicit for the eight-tick octave and phi-ladder calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.