equilibrium_zero
plain-language theorem explainer
equilibrium_zero establishes that the recognition cost J vanishes at the equilibrium ratio r = 1. Researchers modeling the thermodynamic arrow of time from J-cost cite this to fix the zero point of the potential. The result follows by direct reference to the upstream simplification of the explicit J formula.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the recognition cost.
background
The module develops the thermodynamic arrow of time in Recognition Science terms. Recognition cost J(r) reaches its global minimum at equilibrium (r = 1, J = 0), so evolution toward this point defines the forward time direction. The explicit form J(x) = (x-1)^2/(2x) is supplied by the Cost module.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module (and its duplicate in JcostCore). That lemma itself reduces the claim by simp on the definition of Jcost.
why it matters
The result supplies the equilibrium field inside entropyArrowCert, which packages five_arrows, nonneg, equilibrium, and time_reversal_symmetric. It is also referenced by statMechCert and StatMechCert in the statistical-mechanics layer. Within the framework it anchors the zero of the J-potential, consistent with J-uniqueness (T5) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.