equilibrium_is_zero
plain-language theorem explainer
equilibrium_is_zero establishes that the J-cost vanishes at the unit ratio, supplying the degeneracy condition required for multiple admissible paths in the free-will mechanism. Researchers modeling compatibilist free will via sigma conservation in Recognition Science cite this as the base equilibrium. The proof is a direct term application of the Jcost unit lemma.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$ is the cost function of a recognition event at positive ratio $x$.
background
The module derives free will from sigma conservation by identifying free choice with degeneracy in the J-cost landscape: multiple paths achieve the minimum cost J = 0. The cost function J is defined via the multiplicative recognizer as J(x) = (x-1)^2 / (2x), which is non-negative and zero only at x=1. Upstream, the lemma Jcost_unit0 proves this by direct simplification, and the cost of a recognition event is given by Cost.Jcost e.state. From the module documentation: 'When multiple paths tie at J = 0 (multiplicity > 1), the agent has genuine optionality — this is the RS mechanism of free choice.'
proof idea
The proof is a one-line wrapper applying the lemma Jcost_unit0 from the Cost module, which itself follows by simplification of the definition J(x) = (x-1)^2 / (2x).
why it matters
This theorem provides the equilibrium field for the freeWillCert definition, which certifies the five compatibilist positions under sigma conservation. It realizes the first key theorem listed in the module: 'J(1) = 0 — equilibrium is unique per direction.' In the Recognition Science framework it anchors the J-uniqueness (T5) and the degeneracy at zero cost that permits free choice while preserving conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.