isBalanced
plain-language theorem explainer
The glossary supplies the canonical name isBalanced for the zero-strain predicate on states of any type. RRF workers on consistency checks and octave morphisms cite it to enforce uniform terminology across modules. The declaration is a direct alias to the predicate defined in the Strain module.
Claim. A state $x$ of type $State$ satisfies the zero-strain predicate when the strain functional $J$ obeys $J(x)=0$.
background
The RRF glossary module establishes official symbols, with $J$ denoting the strain/cost functional and strain defined as deviation from balance where the law requires $J$ to reach zero. The upstream Strain module supplies the concrete predicate: a state is balanced precisely when its strain functional returns zero. Sibling definitions in the same file introduce the related minimizer predicate and the J-minimization law asserting existence of at least one such state.
proof idea
One-line wrapper that aliases the isBalanced predicate from the StrainFunctional interface.
why it matters
This supplies the standard name consumed by JMinimizationLaw (existence of a zero-strain state) and isConsistent (low strain conjoined with ledger closure). It also appears in octave well-posedness and the preservation of equilibria under morphisms. The declaration anchors the J to zero drive that runs through the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.