equilibria_are_minimizers
plain-language theorem explainer
Non-negative strain functionals have the property that any equilibrium state with zero strain is a global minimizer. RRF model builders and order-preservation proofs invoke this to confirm minimal elements without further computation. The term-mode proof introduces an arbitrary comparison state, unfolds the balanced hypothesis to zero strain, and applies the nonnegativity axiom directly.
Claim. Let $S$ be a strain functional with $S.J(y)geq 0$ for every state $y$. If a state $x$ satisfies $S.J(x)=0$, then $S.J(x)leq S.J(y)$ for every state $y$.
background
StrainFunctional supplies an abstract J-cost that quantifies deviation from recognition balance, with lower values corresponding to more consistent states. The NonNeg class requires $J(x)geq 0$ for all inputs, while isBalanced holds precisely when $J(x)=0$. The module sets strain to zero as the governing law, encoding deviation from equilibrium in the RRF interface. Upstream LedgerFactorization and PhiForcingDerived calibrate the J-cost itself, and IntegrationGap supplies the active-edge count that anchors the discrete setting.
proof idea
The term proof introduces an arbitrary state y, simplifies the definitions of weaklyBetter and isBalanced, rewrites the balanced hypothesis to obtain zero strain at x, and applies the NonNeg.nonneg axiom at y to conclude the inequality.
why it matters
This theorem feeds the trivial_is_minimizer result in RRF.Models.Trivial and the equilibria_minimal theorem in OrderPreservation. It closes the direct link from the strain-to-zero law in the RRF core to the existence of minimal elements, consistent with the recognition composition law and the phi-ladder forcing chain. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.