jcost_nonneg
plain-language theorem explainer
The recognition cost J(r) is non-negative for every positive real r. Researchers constructing the thermodynamic arrow of time cite this to establish that equilibrium at r = 1 is the global minimum of cost. The proof splits on whether r equals 1, then invokes either the unit-value lemma or the strict-positivity lemma.
Claim. For every real number $r > 0$, the recognition cost satisfies $J(r) = Jcost(r) ≥ 0$.
background
In Recognition Science the J-cost quantifies the recognition effort needed to reconcile a scale factor r with its inverse. It is given explicitly by the squared-ratio formula $J(r) = (r-1)^2/(2r)$ for r > 0, which is equivalent to the hyperbolic expression cosh(log r) - 1. The module EntropyArrowFromJCost develops the pre-Big-Bang thermodynamic arrow by showing that evolution drives r toward the unique zero-cost point r = 1. The present theorem supplies the first of the five key claims listed in the module documentation: J(r) ≥ 0 always. It rests on the upstream lemmas Jcost_pos_of_ne_one (strict positivity away from unity) and Jcost_unit0 (normalization at equilibrium).
proof idea
The tactic proof performs a case split on the predicate r = 1. When the predicate holds, it rewrites with the lemma Jcost_unit0 to obtain equality to zero. When the predicate fails, it applies the lemma Jcost_pos_of_ne_one to obtain a strict lower bound and then uses le_of_lt to reach non-negativity.
why it matters
This theorem supplies the non-negativity property required by the EntropyArrowCert structure that certifies the five thermodynamic arrows and by the TachyonFreeCert that guarantees absence of tachyonic modes. It corresponds to theorem IC-005.1 and fills the first item in the module's key claims list. Within the forcing chain it supports the J-uniqueness step (T5) by confirming that the fixed point at unity is a minimum. The result closes the basic positivity requirement for all subsequent measure-theoretic and complexity arguments that rely on J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.