ledger_algebra_consistent
plain-language theorem explainer
The declaration establishes that a LedgerAlgebra instance exists by direct term construction. Workers on conservation structures in the Recognition framework cite it to confirm the double-entry axioms are satisfiable without internal contradiction. The proof is a one-line term that supplies the structure literal relying on the defaults for balanced transactions and ledgers.
Claim. The LedgerAlgebra structure is non-empty: there exists a bundle containing a transaction type, a ledger type, and proofs that every transaction satisfies debit + credit = 0 and every ledger has net zero.
background
The module sets the ledger as the core accounting structure that enforces conservation via double-entry bookkeeping, with the fundamental constraint that debit + credit = 0 for each transaction and net = 0 for each ledger. Upstream, RRF is the local non-sealed recognition field interface defined as (Fin 4 → ℝ) → ℝ. The LedgerAlgebra bundles the transaction and ledger types together with the two balance conditions.
proof idea
The proof is a term-mode construction that directly supplies an instance of LedgerAlgebra by the empty structure literal, which inherits the default proofs for transactions_balanced and ledgers_balanced from the structure definition.
why it matters
This theorem confirms the internal consistency of the ledger algebra that underpins conservation laws in the RRF framework. It supports the Recognition Science derivation by ensuring the accounting structure for energy, charge, and momentum admits at least one model. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.