equilibria_minimal
plain-language theorem explainer
Equilibria under non-negative strain functionals are minimal elements in the state ordering. Researchers analyzing order preservation in recognition resource fields cite this to confirm that zero-strain states achieve minimal cost. The proof is a one-line wrapper applying the core lemma that balanced states minimize strain.
Claim. Let $S$ be a non-negative strain functional on states. If a state $x$ satisfies the zero-strain balance condition under $S$, then $x$ is a strain minimizer under $S$.
background
The module establishes theorems on order preservation for RRF states, where the key insight is that recognition depends on relative ordering by strain rather than absolute values. StrainFunctional.NonNeg requires the functional to return non-negative values, while isBalanced is the zero-strain predicate and isMinimizer is the strain-minimizer predicate, both drawn from the RRF.Core.Glossary and Strain modules. Upstream results include the definition of RRF as a local non-sealed recognition field and the equilibria_are_minimizers lemma in Strain, which directly supplies the minimality link.
proof idea
The proof is a one-line wrapper that applies the equilibria_are_minimizers lemma from the Strain module to the given state and balance hypothesis.
why it matters
This declaration completes the statement that equilibria are minimal elements within the RRF order-preservation theorems. It supports the framework emphasis on strain ordering for recognition processes and connects to the broader chain of results on balanced states in RRF.Core. No downstream uses are recorded yet, leaving open its integration into larger minimality arguments for discrete fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.