jcost_zero_iff_one
plain-language theorem explainer
The theorem states that the J-cost function on positive reals vanishes if and only if its argument equals one. Workers verifying the quantum-gravity octave duality certificate cite it to confirm the unique zero-cost balance point required for the kappa-hbar product. The argument rewrites the cost via its square-over-argument form and splits the resulting zero-divisor condition using real arithmetic and positivity.
Claim. For every positive real $x$, the J-cost satisfies $J(x)=0$ if and only if $x=1$, where $J(x)$ is the arithmetic-geometric mean gap of the pair $(x,x^{-1})$ given explicitly by $(x-1)^2/(2x)$.
background
In the Quantum-Gravity Octave Duality module the J-cost is defined as the exact AM-GM gap of the pair $(x,x^{-1})$ for $x>0$, yielding the closed form $(x-1)^2/(2x)$. This expression originates from the Recognition Composition Law together with the T5 J-uniqueness forcing step. Upstream structures supply the ledger factorization that calibrates J and the phi-derived forcing that produces the cost functional itself.
proof idea
The term proof first rewrites the cost via the sibling equality jcost_eq_sq_div, then invokes div_eq_zero_iff to obtain a disjunction of a square term and a positivity term. The square case reduces by sub_eq_zero while the positivity case is discharged by the hypothesis 0<x, leaving only the solution x=1.
why it matters
This result supplies the zero-cost characterization inside the qg_octave_cert construction that assembles the full QG Octave Duality Certificate. It thereby supports the central claim kappa * hbar = 8 forced by the eight-tick octave (T7) and the phi-fifth duality of the constants. The theorem closes the J-cost properties needed for the T5-T8 chain and the AM-GM interpretation of cost balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.