LedgerClosure
LedgerClosure defines the predicate asserting that a state x satisfies the double-entry constraint for ledger L. RRF modelers cite it when enforcing conservation in state accounting across discrete systems. The definition is a direct one-line alias to the isClosed check on debit-credit equality.
claimFor ledger constraint $L$ on states of type $State$ and state $x$, LedgerClosure$(L,x)$ holds if and only if $L$.debit$(x) = L$.credit$(x)$.
background
The RRF Core Glossary supplies canonical vocabulary for the Reality Recognition Framework. LedgerConstraint $L$ encodes the double-entry rule that debit must equal credit. The upstream isClosed predicate from the Strain module supplies the concrete equality $L$.debit $x = L$.credit $x$ that LedgerClosure aliases.
proof idea
One-line wrapper that directly returns the result of isClosed applied to the supplied ledger constraint and state.
why it matters in Recognition Science
The definition anchors conservation accounting inside the RRF glossary, consistent with the framework requirement that strain $J$ tends to zero under balanced ledgers. It supplies the predicate used to label closed states in discrete models drawn from fluids, vorticity, and spin-statistics modules.
scope and limits
- Does not specify the concrete debit or credit functions inside any LedgerConstraint.
- Does not enforce numerical zero-balance beyond the equality check.
- Does not extend the predicate to continuous or infinite state spaces.
- Does not address time evolution or updates of ledger entries.
formal statement (Lean)
62def LedgerClosure {State : Type*} (L : LedgerConstraint State) (x : State) : Prop :=
proof body
Definition body.
63 L.isClosed x
64
65/-- Channel equivalence: two channels induce the same state ordering. -/