proofs
Provednlightninglightningpr-14deep-formalization

Composed channel transfers preserve aggregate balance

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

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

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