proofs
Provednlightninglightningpr-14deep-formalization

A balance transfer followed by its reverse restores both balances

For all left,right,amount∈Z\htmlData{mx=1}{\mathit{left}, \mathit{right}, \mathit{amount} \in \htmlData{mx=0}{\mathbb{Z}}}:

(left−amount+amount,right+amount−amount)=(left,right)\begin{aligned} & \htmlData{mx=11}{\left( \htmlData{mx=5}{\htmlData{mx=3}{\htmlData{mx=1}{\mathit{left}} - \htmlData{mx=2}{\mathit{amount}}} + \htmlData{mx=4}{\mathit{amount}}}, \htmlData{mx=10}{\htmlData{mx=8}{\htmlData{mx=6}{\mathit{right}} + \htmlData{mx=7}{\mathit{amount}}} - \htmlData{mx=9}{\mathit{amount}}} \right)} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=14}{\left( \htmlData{mx=12}{\mathit{left}}, \htmlData{mx=13}{\mathit{right}} \right)} \end{aligned}
What the notation means · or point at any symbol
ZIntegers
The integers …, −2, −1, 0, 1, 2, …. (Int)
x ∈ TVariables
left, right, amount range over integers: the statement must hold for every choice. ((left right amount : Int))
(a, b)Tuple
The ordered pair (or tuple) of left − amount + amount, right + amount − amount. (((left - amount) + amount, (right + amo…)
=Equality
(left − amount + amount, right + amount − amount) and (left, right) are the same. (((left - amount) + amount, (right + amo…)
+Addition
left − amount plus amount. ((left - amount) + amount)
-Subtraction
left minus amount. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (left - amount)

Repository-grounded Lean formalization for NLightning PR #14. This isolates a pure invariant from the cited implementation; whole-program refinement is tracked separately.

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
propext
Proof
6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements