Provednlightninglightningpr-14formal-invariant
Equal and opposite accounting postings sum to zero
For all :
What the notation means · or point at any symbol
- ZIntegers
- The integers …, −2, −1, 0, 1, 2, …. (
Int) - +Addition
- amount plus −amount. (
amount + (-amount)) - =Equality
- amount + −amount and 0 are the same. (
amount + (-amount) = 0) - −xNegation
- The negative of amount. (
-amount)
theorem nlightning-double-entry-zero-sum (amount : Int) :
amount + (-amount) = 0Abstract signed-amount model of a balanced double entry.
How it was proved
- Proved
- 6 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Quot.sound, propext
- Proof
- 5 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.