jcost_eq_sq_div
plain-language theorem explainer
The algebraic identity equates the J-cost to (x-1)^2/(2x) for positive reals. Researchers deriving non-negativity or zero-cost conditions in quantum-gravity duality proofs would cite it. The proof reduces directly by unfolding the definition and applying field simplification followed by ring normalization.
Claim. For every real number $x > 0$, the recognition cost satisfies $J(x) = (x-1)^2 / (2x)$.
background
The Quantum-Gravity Octave Duality module proves that the Einstein coupling kappa and Planck action hbar multiply to exactly 8, forced by the single J-cost functional. J-cost measures squared deviation from balance at x=1 and equals the arithmetic-geometric mean gap of the pair {x, x^{-1}}, where AM(x, x^{-1}) = (x + x^{-1})/2 and GM = 1, yielding the squared form after clearing the denominator. This rests on J-uniqueness from the forcing chain (T5) and the Recognition Composition Law. Upstream results include the step definition that applies local rules to successor tapes in cellular automata and the via structure for recognition-weighted stellar assembly.
proof idea
The proof is a term-mode algebraic reduction. It unfolds the Jcost definition, applies field_simp using the positivity hypothesis to clear the denominator, and concludes with ring to verify the equality.
why it matters
This supplies the explicit squared form invoked by jcost_nonneg_amgm to prove non-negativity from (x-1)^2 >=0 and by jcost_zero_iff_one to characterize the zero at x=1. Both feed into qg_octave_cert that packages the duality results. The identity realizes the AM-GM characterization in section 1 of the module, supporting the central octave duality kappa hbar =8 and linking to the eight-tick cycle (T7) and phi-ladder constants in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.