gm_pair_unity
plain-language theorem explainer
For any positive real x the geometric mean of x and its reciprocal equals one. Recognition Science proofs establishing the J-cost as an AM-GM gap cite this identity to fix the constant offset at minus one. The proof is a one-line term reduction that cancels the product to one and takes the square root.
Claim. For every real $x > 0$, $√(x · x^{-1}) = 1$.
background
In the Quantum Gravity Octave Duality module the J-cost is defined as the arithmetic-geometric mean gap of the pair {x, x^{-1}}, so Jcost x = (x + x^{-1})/2 - √(x · x^{-1}). The module proves that this gap is nonnegative with equality only at x = 1, supplying the foundation for the octave duality κ · ℏ = 8. Upstream results include the cost definition in MultiplicativeRecognizerL4 (derivedCost on positive ratios) and the recognition-event cost in ObserverForcing (Jcost of the state).
proof idea
The proof is a one-line term-mode wrapper. It rewrites the product inside the square root by the multiplicative inverse cancellation mul_inv_cancel₀ (using 0 < x) and then applies Real.sqrt_one.
why it matters
This identity anchors §1 of the module by confirming that the geometric-mean term is identically 1, so the constant offset in Jcost is exactly -1. It is invoked directly by the downstream theorem jcost_is_amgm_gap to obtain Jcost x = AM(x, x^{-1}) - 1. In the Recognition framework the result supports T5 J-uniqueness and the AM-GM reading of recognition cost that feeds the phi-ladder mass formulas and the κ ℏ = 8 duality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.