jcost_is_amgm_gap
plain-language theorem explainer
The declaration shows that the recognition cost for positive real x equals the arithmetic-geometric mean gap of the pair {x, x^{-1}}. Researchers deriving quantum-gravity relations from the single J-functional would cite this identity when establishing cost non-negativity or the kappa-hbar duality. The proof is a one-line wrapper that rewrites via the geometric-mean unity lemma and unfolds the cost definition.
Claim. For all real $x > 0$, the recognition cost satisfies $J(x) = (x + x^{-1})/2 - (x x^{-1})^{1/2}$.
background
In the Quantum-Gravity Octave Duality module the recognition cost is defined as the AM-GM gap of the pair {x, x^{-1}}, where AM(x, x^{-1}) = (x + x^{-1})/2 and GM(x, x^{-1}) = sqrt(x x^{-1}). This supplies the algebraic root of non-negativity and of the reciprocal symmetry J(x) = J(x^{-1}). The module setting is the forcing chain that locks kappa = 8 phi^5 and hbar = phi^{-5} by the eight-tick octave, yielding the central identity kappa hbar = 8. Upstream results include the reciprocal automorphism from CostAlgebra (which closes the pair under inversion) and the J-calibration structures from LedgerFactorization and PhiForcingDerived.
proof idea
The proof applies the sibling lemma gm_pair_unity (which states that the geometric mean of {x, x^{-1}} equals 1) and then unfolds the definition of the cost function to match the right-hand side by reflexivity.
why it matters
This result completes §1 of the module by identifying the cost with the AM-GM gap, thereby grounding the central theorem kappa hbar = 8 and the subsequent derivations of G hbar = 1/pi and Planck area = 1/pi. It directly instantiates the T5 J-uniqueness step of the forcing chain and supplies the algebraic origin of sigma = 0 conservation. No open questions remain; the claim is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.