Jcost_nonneg
plain-language theorem explainer
The J-cost functional equals half the sum of a positive real x and its reciprocal minus one and is nonnegative for every such x. Modelers of recognition action in gravitational coherence collapse or quantum measurement contexts cite this inequality to guarantee that integrated costs remain nonnegative. The proof rewrites the expression algebraically as a square divided by twice x then invokes nonnegativity of squares together with linear arithmetic.
Claim. For every real number $x > 0$, the J-cost satisfies $J(x) = 0$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The Coherence Collapse module formalizes recognition action as the integral of J-cost along paths, connecting gravitational collapse to the Born rule through the identity C = 2A. J-cost is the functional J(x) = (x + x^{-1})/2 - 1. Upstream lemmas in the Cost module establish the identical nonnegativity statement via the AM-GM inequality or by direct rewriting to a square form.
proof idea
The tactic proof unfolds the definition of Jcost, establishes the algebraic identity equating it to (x-1)^2/(2x) via field_simp and ring, proves the right-hand side nonnegative by sq_nonneg and division by a positive denominator, then concludes with linarith.
why it matters
This nonnegativity is invoked by forty downstream results, including actionJ_nonneg in PathSpace that ensures path actions are nonnegative and multiple cost nonnegativity statements in acoustics and aesthetics. It supplies the basic inequality required for recognition action C[γ] to be well-defined and nonnegative, thereby supporting the emergence of Born-rule probabilities exp(-C_I) in the coherence collapse framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.