jcost_nonneg'
plain-language theorem explainer
J-cost is non-negative for every positive real argument, with equality only at unity. Researchers citing the F1 foundation paper or applying the inequality in gravity, Navier-Stokes, or energy-processing modules would invoke this result. The proof is a one-line wrapper that forwards the core non-negativity lemma from the Cost module.
Claim. For every real $x > 0$, $J(x) = ½(x + x^{-1}) - 1$ satisfies $J(x) ≥ 0$.
background
The module develops the log-domain geometry of the canonical reciprocal cost introduced in the F1 foundation paper. J(x) is defined by the formula ½(x + x^{-1}) - 1 and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream lemmas in the Cost and JcostCore modules establish the same non-negativity claim by rewriting J(x) as (x-1)^2/(2x) and invoking positivity of squares and denominators; parallel proofs appear in Gravity.CoherenceCollapse and NavierStokes.PhiLadderCutoff, each using the AM-GM inequality x + 1/x ≥ 2 for x > 0.
proof idea
One-line wrapper that applies the Jcost_nonneg lemma from the Cost module.
why it matters
The declaration supplies the F1.1.3 non-negativity statement required by the foundation paper for subsequent results on geometric-mean optimality and total bond cost. It is referenced by downstream modules in Navier-Stokes and gravity that treat J-cost as a valid distance-like quantity on the phi-ladder. The result anchors the eight-tick octave and D = 3 spatial dimensions by guaranteeing that cost remains non-negative under the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.