swaitsandClaude Fable 5.1
055decf7e2
The first edition's five laws (debits equal credits; the accounting equation; the trial balance balances; net income articulates to equity; the cash-flow sections sum to the change in cash) are theorems in bookspec/lean, ported from verify/lean (Basic, Entry, Statements, Closing, Ledger under namespace Bookspec) and restated by name in Laws.lean, each a statement about every reachable state of the books. Audit.lean prints their axioms; the checker's lean.rs test fails on a sorry, a law not audited, or any axiom beyond propext, Quot.sound and Classical.choice. Money is Int, the exact count of the smallest unit: every law is a law of addition, so the model is faithful to exact decimals. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp
15 lines
510 B
Lean4
15 lines
510 B
Lean4
import Bookspec
|
|
|
|
/-! Each of the five laws' axioms are printed, and must be only Lean's
|
|
standard three (`propext`, `Quot.sound`, `Classical.choice`) or fewer. No
|
|
`sorryAx`, nothing assumed. `bookspec/checker/tests/lean.rs` reads this
|
|
file's output shape; run it with `lake env lean Audit.lean`. -/
|
|
|
|
open Bookspec
|
|
|
|
#print axioms law_debits_equal_credits
|
|
#print axioms law_accounting_equation
|
|
#print axioms law_trial_balance
|
|
#print axioms law_net_income_articulates
|
|
#print axioms law_cash_flow_is_change_in_cash
|