double_entry_exists
plain-language theorem explainer
The double-entry principle holds by construction in the ledger algebra, guaranteeing that every negative credit has a matching positive debit and every positive debit has a matching negative credit. Researchers deriving conservation laws for physical quantities in Recognition Science would cite this when building accounting structures that enforce closure. The proof is a direct term-mode construction that supplies negation as the explicit witness for both directions.
Claim. The double-entry structure is inhabited: for every integer credit $c < 0$ there exists a debit $d = -c$, and for every integer debit $d > 0$ there exists a credit $c = -d$.
background
In the RRF Foundation module the ledger is the core accounting structure that enforces conservation, with every transaction required to satisfy debit plus credit equals zero. The DoubleEntry structure formalizes this bookkeeping principle via two forall-exists statements over the integers. This result rests on the DoubleEntry definition itself together with the completeness predicate imported from the SAT backpropagation module.
proof idea
The proof is a term-mode construction of the DoubleEntry structure. It supplies credit_has_debit by the function that sends any negative credit c to the debit -c witnessed by reflexivity, and symmetrically supplies debit_has_credit by the function that sends any positive debit d to the credit -d witnessed by reflexivity.
why it matters
This theorem supplies the DoubleEntry instance required by the LedgerAlgebra bundle, which packages the transaction type, ledger type, and balanced-transaction property. It directly supports the framework claim that conservation laws (energy, charge, momentum) arise as instances of ledger closure, consistent with the Recognition Science derivation of physics from a single functional equation and the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.