isMinimizer
plain-language theorem explainer
A state x minimizes strain functional S precisely when it is weakly better than every alternative y. RRF model builders and equilibrium theorems cite this predicate to certify global minima of the J-cost. The declaration is a direct definition expanding to a universal quantification over the weaklyBetter relation.
Claim. Let $S$ be a strain functional on a state space. A state $x$ is a minimizer of $S$ when $S.J(x) ≤ S.J(y)$ for every state $y$.
background
The RRF.Core.Strain module treats strain as the fundamental deviation from equilibrium, with the law that strain tends to zero. A StrainFunctional is a structure that assigns a non-negative real cost J to each state, satisfying J(x) = 0 exactly when the state is balanced. Upstream results define equilibria as the set of states where isBalanced holds and supply concrete State types from discrete vorticity and ILG action models.
proof idea
This is a definition that directly encodes the minimizer predicate as the statement ∀ y, S.weaklyBetter x y. No lemmas or tactics are applied; the body supplies the base predicate consumed by equilibria_are_minimizers and the quadratic model theorems.
why it matters
The predicate feeds the theorem equilibria_are_minimizers, which shows that balanced states are minimizers under non-negative strain. It is re-exported in the Glossary and used to verify argmin preservation in quadratic and trivial models. It directly implements the J → 0 drive stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.