Provednlightninglightningpr-14formal-invariant

A liquidity fee transfer preserves combined channel balance

For all $\htmlData{mx=1}{\mathit{buyer}, \mathit{seller}, \mathit{fee} \in \htmlData{mx=0}{\mathbb{Z}}}$ :

\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{\mathit{buyer}} - \htmlData{mx=1}{\mathit{fee}}} + (\htmlData{mx=5}{\htmlData{mx=3}{\mathit{seller}} + \htmlData{mx=4}{\mathit{fee}}})} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=7}{\mathit{buyer}} + \htmlData{mx=8}{\mathit{seller}}}

What the notation means · or point at any symbol

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

theorem nlightning-liquidity-fee-conservation (buyer seller fee : Int) :
    (buyer - fee) + (seller + fee) = buyer + seller

Abstract Int model of the buyer-to-seller balance move.

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