theorem
proved
double_entry_exists
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 193.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
190 debit_has_credit : ∀ (d : ℤ), d > 0 → ∃ (c : ℤ), c = -d
191
192/-- Double-entry is always satisfied (by construction). -/
193theorem double_entry_exists : DoubleEntry := {
194 credit_has_debit := fun c _ => ⟨-c, rfl⟩,
195 debit_has_credit := fun d _ => ⟨-d, rfl⟩
196}
197
198/-! ## Ledger Algebra Summary -/
199
200/-- The complete ledger algebra bundle. -/
201structure LedgerAlgebra where
202 /-- The transaction type. -/
203 transaction : Type := Transaction
204 /-- The ledger type. -/
205 ledger : Type := Ledger
206 /-- Transactions are balanced. -/
207 transactions_balanced : ∀ t : Transaction, t.debit + t.credit = 0 := fun t => t.balanced
208 /-- Ledgers are balanced. -/
209 ledgers_balanced : ∀ L : Ledger, L.net = 0 := fun L => L.global_balance
210 /-- Double-entry holds. -/
211 double_entry : DoubleEntry := double_entry_exists
212
213/-- The ledger algebra is consistent. -/
214theorem ledger_algebra_consistent : Nonempty LedgerAlgebra := ⟨{}⟩
215
216end RRF.Foundation
217end IndisputableMonolith