validStates
plain-language theorem explainer
validStates extracts the subset of states satisfying zero strain and closed ledger conditions for a given StrainLedger. Researchers modeling discrete fluids or recognition dynamics cite this set to restrict attention to equilibrium configurations. The definition is a direct set comprehension over the isValid predicate supplied by the ledger structure.
Claim. For a strain ledger $SL$, the set of valid states is defined by $validStates(SL) = { x | isValid(SL, x) }$, where $isValid(SL, x)$ holds if and only if the strain component of $SL$ is balanced at $x$ and the ledger component of $SL$ is closed at $x$.
background
Strain quantifies deviation from equilibrium in the RRF framework, with the governing law requiring strain to approach zero (equivalently $J$ to zero). The StrainLedger structure combines a StrainFunctional that evaluates balance with a LedgerConstraint that enforces closure properties. The upstream isValid predicate declares a state valid precisely when both conditions hold simultaneously. This module supplies the abstract interface for strain evaluations on discrete state types such as 2D Galerkin states or finite vorticity lattices.
proof idea
The definition is a one-line set comprehension that directly invokes the isValid predicate on the input StrainLedger.
why it matters
This definition supplies the concrete set of admissible states for RRF dynamics, enabling restriction to configurations where strain vanishes and ledgers close. It supports the broader strain functional interface in the module, where lower strain corresponds to greater consistency. No downstream uses are recorded, leaving open how the set integrates into larger existence or minimization results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.