LedgerClosure
plain-language theorem explainer
LedgerClosure defines the property that a state x satisfies the double-entry constraint under a LedgerConstraint L. Developers of Reality Recognition Framework models would reference it to enforce conservation accounting. The definition is a direct one-line alias to the isClosed predicate.
Claim. For a ledger constraint $L$ on states of type $State$, the ledger closure property holds for state $x$ precisely when the debit and credit entries balance, i.e., $L$.debit$(x) = L$.credit$(x)$.
background
The RRF Core Glossary module supplies canonical terminology for the Reality Recognition Framework. It lists L as the LedgerConstraint symbol denoting double-entry conservation accounting where debit equals credit, alongside J for the strain functional and related concepts such as Vantage and Octave.
proof idea
One-line wrapper that applies the isClosed definition from the Strain module, which states a state satisfies the ledger constraint if debit equals credit.
why it matters
This definition supplies the standard name for ledger closure in the RRF glossary, supporting uniform reference to conservation across modules. It directly implements the Ledger entry in the module's key symbols table. No downstream uses appear in the current graph, but the entry anchors balance checks that feed recognition and strain laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.