equilibria
plain-language theorem explainer
The equilibria definition extracts the set of states at which a given strain functional vanishes. Modelers of RRF strain dynamics cite it to identify balanced configurations before applying minimizer checks or octave compositions. The implementation is a direct set comprehension over the isBalanced predicate supplied by the functional.
Claim. Let $S$ be a strain functional on a state space. The equilibria of $S$ are the states $x$ satisfying $J_S(x)=0$, where $J_S$ denotes the non-negative cost map of $S$.
background
StrainFunctional is a structure that assigns a non-negative real cost $J$ to each state, with the property that $J(x)=0$ if and only if $x$ is balanced. The RRF.Core.Strain module treats strain as the fundamental deviation from recognition equilibrium, with the governing law that strain approaches zero. Upstream, the isBalanced predicate is drawn from Cosmology.DarkEnergy where it requires total ledger cost to vanish, while State is the discrete Galerkin state type from ClassicalBridge.Fluids.CPM2D.
proof idea
This is a one-line definition that constructs the set of all states $x$ for which the strain functional $S$ satisfies its isBalanced condition.
why it matters
This definition supplies the equilibrium set used by the octave composition in RRF.Core.Octave and by vantage category constructions in RRF.Foundation.VantageCategory. It realizes the core RRF principle that strain vanishes at equilibrium, feeding into theorems on minimizers and order preservation. It connects to the broader forcing chain through the J-uniqueness property at T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.