equilibria
plain-language theorem explainer
The equilibria definition returns the set of states at which a given strain functional vanishes. Researchers modeling balance in RRF systems cite this set when identifying stable or zero-cost configurations. The definition is a direct set comprehension over the isBalanced predicate supplied by the StrainFunctional structure.
Claim. Let $S$ be a strain functional on a state space. The equilibria of $S$ are the set of states $x$ such that the strain cost $J_S(x)=0$.
background
A strain functional assigns a non-negative real cost $J$ to each state, with $J(x)=0$ precisely when the state is balanced. The RRF.Core.Strain module treats strain as the deviation from equilibrium, with the governing law that strain tends to zero. The State type is the discrete 2D Galerkin state from CPM2D; related balance predicates appear in the ledger-cost definition from DarkEnergy.
proof idea
One-line definition that builds the set of states satisfying the isBalanced predicate of the input strain functional.
why it matters
This supplies the equilibrium set referenced by Octave.equilibria and VantageCategory.equilibria, and feeds the isMinimizer predicate and prime-gap counting arguments. It directly encodes the strain-to-zero law of the RRF framework and supports the composition and transfer results in the OctaveTransfer module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.