equilibria_are_minimizers
plain-language theorem explainer
Non-negative strain functionals send every balanced state to a global minimizer of the strain map. RRF model builders cite the result when closing the argument that equilibria are preferred states under the J-cost. The term-mode proof rewrites the balance hypothesis into the non-negativity axiom and concludes immediately.
Claim. Let $S$ be a strain functional obeying $S.J(x) ≥ 0$ for every state $x$. If $S.J(x) = 0$, then $S.J(x) ≤ S.J(y)$ holds for every state $y$.
background
The module defines strain as the deviation of a state from ledger balance, with the governing law that strain tends to zero. NonNeg is the class asserting that the strain map $J$ is everywhere non-negative. isBalanced is the predicate that a state has strain exactly zero; isMinimizer asserts that the state attains the global lower bound of $J$ under the weaklyBetter ordering. Upstream results supply the ledger-factorization and phi-forcing structures that calibrate $J$ itself.
proof idea
Term-mode proof. The tactic intro y brings in an arbitrary competitor; simp reduces weaklyBetter and isBalanced to the inequality $0 ≤ S.J y$; rw substitutes the hypothesis that $S.J x = 0$; exact applies the NonNeg.nonneg axiom to finish.
why it matters
The theorem supplies the base case for both trivial_is_minimizer in the Trivial model and equilibria_minimal in OrderPreservation. It therefore anchors the claim that equilibria are minimal elements inside the Recognition framework's strain-to-zero law. No open scaffolding remains; the result is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.