isClosed
plain-language theorem explainer
The isClosed definition states that a state x satisfies a ledger constraint L exactly when the debit assigned to x equals the credit assigned to x. Researchers deriving scale hierarchies and phi emergence from ledger balance cite this predicate to enforce zero net strain. The definition is realized as a direct equality between the debit and credit fields of the LedgerConstraint structure.
Claim. A state $x$ satisfies the ledger constraint $L$ if and only if the debit of $x$ under $L$ equals the credit of $x$ under $L$.
background
In the RRF Core Strain module, strain measures deviation from equilibrium, with strain approaching zero corresponding to the recognition law J approaching zero. The LedgerConstraint structure consists of two maps debit and credit, each from State to integers, that together encode the accounting balance condition required for zero net strain.
proof idea
This is a definition that directly equates the debit and credit components of the LedgerConstraint for the given state. It is a one-line wrapper around the equality L.debit x = L.credit x with no lemmas or tactics applied.
why it matters
This definition supplies the closedness predicate required by downstream theorems such as hierarchy_emergence_forces_phi and ledger_forces_phi, which derive the golden ratio from ledger primitives and additive closure. It realizes the balance axiom in the MinimalHierarchy structure and supports self-similar forcing toward phi, linking to T5 J-uniqueness and T6 phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.