isValid
plain-language theorem explainer
The isValid definition declares a state x valid for StrainLedger SL precisely when the strain functional reports balance at x and the ledger reports closure at x. RRF model builders cite it to certify equilibrium states in quadratic and trivial examples. It is realized as a direct conjunction of the two component predicates with no further reduction.
Claim. Let $SL$ be a combined strain-and-ledger evaluator over a state space. A state $x$ is valid if the strain component is balanced at $x$ and the ledger component is closed at $x$.
background
The RRF Core Strain module treats strain as the measure of deviation from equilibrium, with the governing law that strain tends to zero (equivalently J tends to zero). The StrainLedger structure pairs a StrainFunctional that evaluates this deviation with a LedgerConstraint that enforces closure on the state ledger.
proof idea
This is a definition that directly conjoins the isBalanced predicate supplied by the strain component with the isClosed predicate supplied by the ledger component. No lemmas are invoked; the body is the primitive conjunction.
why it matters
The definition supplies the predicate used to build the set of valid states and is invoked in the proofs that the quadratic 1D model has zero as its unique valid state and that the trivial model has a valid unit state. It operationalizes the RRF balance law inside the Recognition Science framework, where J-uniqueness and the phi-ladder determine equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.