Jcost_nonneg
plain-language theorem explainer
Non-negativity of the J-cost holds for every positive real x, where J(x) equals (x + x^{-1})/2 - 1. Researchers in acoustics, action principles, and aesthetic modeling cite this inequality to guarantee valid costs. The argument reduces the expression to a squared ratio via an algebraic identity and concludes with the positivity tactic.
Claim. For every real number $x > 0$, $J(x) := (x + x^{-1})/2 - 1$ satisfies $J(x) ≥ 0$.
background
The Cost module defines the J-cost function by Jcost x = (x + x^{-1})/2 - 1. This expression encodes the deviation from unity that appears in the J-uniqueness step of the forcing chain and obeys the Recognition Composition Law. The sibling lemma Jcost_eq_sq supplies the equivalent form (x - 1)^2 / (2x) for x ≠ 0, which serves as the algebraic bridge to non-negativity.
proof idea
The proof first extracts x ≠ 0 from the strict positivity hypothesis. It then invokes the upstream lemma Jcost_eq_sq to replace Jcost x by the squared ratio. The positivity tactic finishes the argument because the numerator is a square and the denominator is positive.
why it matters
This lemma supplies the non-negativity foundation invoked by forty downstream results, among them pitchCost_nonneg in acoustics, actionJ_nonneg in path-space actions, and narrativeTension_nonneg in aesthetic geodesics. It confirms that costs remain valid measures on the positive ray, consistent with AM-GM and the phi-ladder constructions. The claim is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
Universal differential equations blend physics laws with neural nets
"Training a UDE amounts to minimizing a cost function C(θ) defined on uθ(t), the current solution to the differential equation with respect to the choice of parameters θ."
-
Two-loss JEPA trains stable world models from pixels
"SIGReg regularization term enforces Gaussian-distributed latent embeddings"
-
Survey maps causes and fixes for hallucinations in vision-language models
"We review recent advances in identifying, evaluating, and mitigating these hallucinations, offering a detailed overview of the underlying causes, evaluation benchmarks, metrics, and strategies developed to address this issue."