Provednlightninglightningpr-14formal-invariant

A channel balance transfer preserves total balance

For all $\htmlData{mx=1}{\mathit{localBal}, \mathit{remoteBal}, \mathit{amount} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{\mathit{amount}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{localBal}}$ , then

\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{\mathit{localBal}} - \htmlData{mx=1}{\mathit{amount}}} + (\htmlData{mx=5}{\htmlData{mx=3}{\mathit{remoteBal}} + \htmlData{mx=4}{\mathit{amount}}})} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=7}{\mathit{localBal}} + \htmlData{mx=8}{\mathit{remoteBal}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
x ∈ TVariables: localBal, remoteBal, amount range over natural numbers: the statement must hold for every choice. ((localBal remoteBal amount : Nat))
≤At most: amount is less than or equal to localBal. (amount ≤ localBal)
=Equality: localBal − amount + (remoteBal + amount) and localBal + remoteBal are the same. ((localBal - amount) + (remoteBal + amou…)
-Subtraction: localBal minus amount. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (localBal - amount)
+Addition: remoteBal plus amount. (remoteBal + amount)

theorem nlightning-balance-transfer-conservation (localBal remoteBal amount : Nat) (covered : amount ≤ localBal) :
    (localBal - amount) + (remoteBal + amount) = localBal + remoteBal

Abstract Nat model of moving a covered amount between channel sides.

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

A channel balance transfer preserves total balance

How it was proved

More proved statements