J_nonneg
plain-language theorem explainer
J_nonneg shows that the cost functional J remains non-negative for every positive real argument. Researchers deriving physics from the Recognition Science cost axioms cite it to ground the interpretation of J as a deviation measure with zero at unity. The proof reduces J(x) to an algebraic expression that is visibly non-negative via field simplification and positivity.
Claim. For every real number $x > 0$, the cost functional $J(x) := (x + x^{-1})/2 - 1$ satisfies $J(x) >= 0$.
background
The module CostAxioms formalizes three primitive axioms for the cost functional F. A1 requires F(1) = 0, A2 is the Recognition Composition Law F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), and A3 sets the second logarithmic derivative at zero to 1. From these, J is derived as the unique solution J(x) = (x + x^{-1})/2 - 1, which satisfies the axioms and serves as the canonical cost measure.
proof idea
The proof unfolds the definition of J with simp. It then establishes the algebraic identity (x + x^{-1})/2 - 1 = ((x-1)^2 / x)/2 by field_simp and ring. Finally, positivity of (x-1)^2 / x for x > 0 yields the result.
why it matters
This result anchors the economic reading of the axioms in the Foundation module, where low J corresponds to cheap, coherent configurations. It supports the uniqueness theorem for J as the solution to the functional equation and the law of existence that equates existence with J(x)=0. No open questions are directly touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.