isBalanced
plain-language theorem explainer
The glossary entry supplies the zero-strain predicate for arbitrary state types in the Reality Recognition Framework. Cosmology and discrete fluid modules cite it when stating ledger balance or equilibrium conditions. The declaration is a one-line abbreviation that forwards directly to the StrainFunctional predicate.
Claim. A state $x$ of type $State$ is balanced when the associated strain functional satisfies $J(x)=0$.
background
The RRF Core Glossary module supplies the single source of truth for framework vocabulary, with J denoting the strain/cost functional and strain defined as deviation from balance (J → 0 is the law). This entry aliases the zero-strain predicate for uniform reference across modules. Upstream, the Strain module defines the predicate explicitly: 'A state is balanced/equilibrium if its strain is exactly zero' via S.J x = 0. The sibling isMinimizer entry checks that no other state is strictly better under the same functional.
proof idea
One-line wrapper that applies StrainFunctional.isBalanced.
why it matters
This definition standardizes the balanced-state predicate so that downstream results can invoke it without redefinition. It is referenced by isConsistent (balanced strain and closed ledger), JMinimizationLaw (existence of a zero-strain state), and Octave.preserves_equilibria (morphisms preserve equilibria under non-negative strain). The entry therefore supports the framework-wide claim that strain minimization is the fundamental drive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.