DoubleEntry
The DoubleEntry structure encodes the double-entry bookkeeping principle by requiring that every negative integer credit has a matching positive debit of equal magnitude and every positive debit has a matching negative credit. Ledger models of conservation in Recognition Science cite this as the primitive zero-sum constraint before any transaction algebra is built. The definition is realized directly by its two field declarations with no separate proof or lemma applications required.
claimA DoubleEntry structure consists of the two properties: for every integer $c < 0$ there exists an integer $d = -c$, and for every integer $d > 0$ there exists an integer $c = -d$.
background
The RRF Foundation module defines the ledger as the core accounting structure that enforces conservation, with every conservation law (energy, charge, momentum) realized as an instance of ledger closure. Double-entry bookkeeping is introduced as the requirement that debit plus credit equals zero for each transaction. The module states: 'The ledger is the core accounting structure that enforces conservation' and 'Each conservation law is an instance of ledger closure.' Upstream imports supply collision-free program checks and simplicial edge lengths but do not alter the algebraic content of this definition.
proof idea
This is a pure structure definition with an empty proof body. The two fields are stated directly as universal quantifiers over the integers; no lemmas are applied and no tactics are invoked.
why it matters in Recognition Science
DoubleEntry supplies the foundational constraint for the ledger algebra bundle and is instantiated by the theorem double_entry_exists via explicit field construction. It anchors the Recognition Science treatment of conservation as zero-sum entries, consistent with the eight-tick octave and phi-ladder constructions. The definition closes the basic accounting interface before mechanism-design results are layered on top.
scope and limits
- Does not assign specific numerical magnitudes to any credits or debits.
- Does not extend the rule to non-integer transaction amounts.
- Does not incorporate probabilistic or quantum extensions of the ledger.
- Does not prove existence of non-trivial balanced ledgers beyond the zero transaction.
formal statement (Lean)
186structure DoubleEntry where
187 /-- For every credit, there's a corresponding debit. -/
188 credit_has_debit : ∀ (c : ℤ), c < 0 → ∃ (d : ℤ), d = -c
189 /-- For every debit, there's a corresponding credit. -/
190 debit_has_credit : ∀ (d : ℤ), d > 0 → ∃ (c : ℤ), c = -d
191
192/-- Double-entry is always satisfied (by construction). -/