Provednlightninglightningpr-14formal-invariant

Internal lot debts cancel from the aggregate pool total

For all $\htmlData{mx=1}{\mathit{lots}, \mathit{owedTo}, \mathit{owedBy} \in \htmlData{mx=0}{\mathbb{Z}}}$ , if $\htmlData{mx=0}{\mathit{owedTo}} \mathrel{\htmlData{mx=2}{=}} \htmlData{mx=1}{\mathit{owedBy}}$ , then

\htmlData{mx=4}{\htmlData{mx=2}{\htmlData{mx=0}{\mathit{lots}} + \htmlData{mx=1}{\mathit{owedTo}}} - \htmlData{mx=3}{\mathit{owedBy}}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\mathit{lots}}

What the notation means · or point at any symbol

ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (Int)
x ∈ TVariables: lots, owedTo, owedBy range over integers: the statement must hold for every choice. ((lots owedTo owedBy : Int))
=Equality: owedTo and owedBy are the same. (owedTo = owedBy)
+Addition: lots plus owedTo. (lots + owedTo)
-Subtraction: lots + owedTo minus owedBy. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (lots + owedTo - owedBy)

theorem nlightning-lot-pool-debt-cancellation (lots owedTo owedBy : Int) (internal : owedTo = owedBy) :
    lots + owedTo - owedBy = lots

Abstract aggregate core of the financial lot bucket invariant.

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: 6 lines of Lean

Internal lot debts cancel from the aggregate pool total

How it was proved

More proved statements