jcost_entropy_floor
plain-language theorem explainer
The theorem states that J-cost is non-negative for every positive real argument, supplying the entropy floor required by the Recognition Science thermodynamic selection argument. Pre-Big-Bang cosmologists cite it when they treat entropy non-decrease as a ledger-closed selection rule on recognition paths. The proof is a one-line wrapper that forwards the hypothesis directly to the algebraic non-negativity lemma already established by AM-GM.
Claim. For every real number $x>0$, the J-cost function satisfies $J(x) = (x + x^{-1})/2 - 1 = (x-1)^2/(2x) ≥ 0$.
background
In the Cosmology.ThermodynamicSelectionCert module the J-cost function is the recognition cost of a positive ratio, defined via the multiplicative recognizer comparator and shown equivalent to $(x-1)^2/(2x)$. The module formalizes the pre-Big-Bang claim that entropy non-decrease emerges as a selection principle on closed recognition ledgers: any recognition-decreasing path from the boundary of the positive reals must have non-decreasing J-cost. The upstream lemma Jcost_nonneg records the same inequality via AM-GM: “J(x) ≥ 0 for positive x (AM-GM inequality)”.
proof idea
One-line wrapper that applies the upstream Jcost_nonneg lemma to the supplied hypothesis 0 < x.
why it matters
The result is one of the five structural inputs bundled into the thermodynamicSelectionCert definition, which packages ground-state uniqueness, entropy floor, and divergence at the boundaries. It directly fills the §3.4 scaffold of the pre-Big-Bang paper by supplying the non-negativity half of the monotone-selection claim. The parent certificate is the only downstream consumer; the lemma closes the structural half of the thermodynamic-selection argument while leaving the dynamical path-monotonicity statement for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.