isBalanced
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any balanced state for a given functional.
- Does not specify the explicit form of the strain functional J.
- Does not incorporate ledger closure or vantage constraints.
- Does not apply outside the StrainFunctional interface.
formal statement (Lean)
50abbrev isBalanced {State : Type*} := StrainFunctional.isBalanced (State := State)
proof body
Definition body.
51
52/-- isMinimizer: Strain minimizer predicate. -/
used by (23)
-
isBalanced -
isConsistent -
JMinimizationLaw -
V -
preserves_equilibria -
wellPosed -
equilibria -
equilibria_are_minimizers -
hasUniqueMin -
isBalanced -
isValid -
equilibria -
equilibria_iso -
hasEquilibrium -
isBalanced -
preserves_balanced -
quadratic1D_equilibrium -
quadratic1D_unique_equilibrium -
shifted_equilibrium -
trivial_balanced -
equiv_equilibria_iff -
equiv_wellPosed -
equilibria_minimal