jcost_nonneg_amgm
plain-language theorem explainer
The J-cost function is non-negative for every positive real input. Workers on the Recognition Science derivation of quantum-gravity duality cite this when confirming that recognition costs cannot be negative in the octave-locked framework. The proof rewrites the cost to its squared-over-linear form and invokes non-negativity of squares together with positivity of the denominator.
Claim. For every real number $x > 0$, $0 ≤ (x-1)^2 / (2x)$.
background
In the Quantum-Gravity Octave Duality module the J-cost is the arithmetic-geometric mean gap of the pair {x, x^{-1}}. The module states that Jcost x equals (x-1)^2 / (2x), obtained from AM(x, x^{-1}) = (x + x^{-1})/2 and GM = 1, so that J equals AM minus GM. This supplies the positivity ingredient for the central claim that kappa times hbar equals 8.
proof idea
The proof is a one-line wrapper. It rewrites the goal via the identity jcost_eq_sq_div to reach the squared form, then applies div_nonneg using sq_nonneg on the numerator and mul_pos on the positive denominator 2x.
why it matters
This supplies the non-negativity clause inside the QG Octave Certificate, which assembles the full duality package including kappa hbar = 8 and the phi-fifth-power relations. It closes the positivity half of the J-cost analysis required by the T5 J-uniqueness step and the AM-GM inequality in the Recognition Science forcing chain. The downstream qg_octave_cert invokes it directly as the j_nonneg field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.