Jcost_nonneg
plain-language theorem explainer
Nonnegativity of the J-cost J(x) = (x + x^{-1})/2 - 1 for every positive real x is recorded in the energy processing bridge. Acoustics, aesthetics, and action modules cite it to bound derived quantities such as pitch deviation costs and path actions. The tactic proof unfolds the definition then reduces x + x^{-1} - 2 to the ratio of a square over a positive denominator, closing with nlinarith.
Claim. For every real $x > 0$, $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(x) ≥ 0$.
background
The J-cost is defined by J(x) := (x + x^{-1})/2 - 1 for x > 0. It is the unique cost functional forced by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This theorem appears inside the Gravity.EnergyProcessingBridge module, which links energy distributions to processing gradients and gravitational modifiers. Upstream lemmas in Cost.JcostCore and CoherenceCollapse establish the same nonnegativity via square identities or AM-GM.
proof idea
Unfold Jcost. Show x + x^{-1} ≥ 2 by rewriting the difference as (x-1)^2 / x. The numerator is nonnegative by squaring and the denominator is positive by the hypothesis 0 < x. The steps apply field_simp, ring, div_nonneg, and nlinarith on sq_nonneg (x-1).
why it matters
Forty downstream results invoke this nonnegativity, including pitchCost_nonneg for music JND, actionJ_nonneg for admissible paths, aestheticCost_nonneg for cultural preferences, and narrativeTension_nonneg. It supplies the base inequality for all cost bounds in the Recognition framework, consistent with J-uniqueness at T5 and the composition law. In the gravity setting it ensures energy-to-processing conversions produce nonnegative modifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.