isMinimizer
plain-language theorem explainer
isMinimizer is the predicate asserting that a state achieves the global minimum of the strain cost functional J. RRF modelers cite it when proving equilibrium properties or invariance of argmin under monotone transforms such as exponentiation. The declaration is a one-line abbreviation that forwards directly to the core definition in the StrainFunctional module.
Claim. A state $x$ is a minimizer of the strain functional if for every state $y$ the cost of $x$ is at most the cost of $y$, i.e., $x$ is weakly preferred to $y$ under the strain ordering.
background
In the RRF glossary the strain functional J measures deviation from balance, with the governing law that J tends to zero. The predicate isMinimizer is introduced as the canonical name for the property that a state realizes the infimum of J. It is defined via the weaklyBetter relation on states, which compares costs directly without reference to specific dynamics or channels.
proof idea
One-line wrapper that applies the definition of isMinimizer from StrainFunctional, which expands to the universal quantification forall y, weaklyBetter x y.
why it matters
The abbreviation supplies the uniform vocabulary required by downstream results such as equilibria_are_minimizers (which shows balanced states are minimizers under non-negative strain) and the quadratic-model theorems that preserve argmin under exp. It directly supports the J to 0 law stated in the module documentation as the fundamental drive of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.