trivial_ledger_closed
plain-language theorem explainer
The trivial ledger constraint on the unit state satisfies the closed condition because its debit and credit functions are both constantly zero. Researchers verifying base cases in the Recognition Science RRF models cite this result to confirm internal consistency of the axiom bundle. The proof is a direct reflexivity step that matches the definition of isClosed to the trivialLedger construction.
Claim. Let $L$ be the ledger constraint on the unit state with $L$.debit$(x) = 0$ and $L$.credit$(x) = 0$ for every state $x$. Then $L$ is closed: $L$.debit$(x) = L$.credit$(x)$.
background
The RRF Models Trivial module constructs the simplest model satisfying RRF axioms, with state space the unit type, J-cost identically zero, and ledger entries of zero debit and credit. This setup demonstrates internal consistency of the core axiom bundle. The isClosed predicate on a ledger constraint $L$ and state $x$ holds precisely when debit equals credit. The trivialLedger is the concrete ledger constraint whose debit and credit maps are both the constant zero function.
proof idea
The proof is a term-mode reflexivity that applies the definition of isClosed directly to trivialLedger. Both sides of the required equality evaluate definitionally to zero, so rfl closes the goal without further tactics.
why it matters
This result supplies one conjunct in the proof of trivial_is_valid, which establishes that the trivial state is valid. It completes the base case for the trivial model and thereby supports the module claim that the construction proves internal consistency of the RRF axiom bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.