Provednlightninglightningpr-14formal-invariant

Accumulated hop fees telescope to receiver amount plus fee sum

For all $\htmlData{mx=1}{\mathit{receiver} \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=3}{\mathit{fees} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\mathbb{N}}}}$ :

\htmlData{mx=7}{\htmlData{mx=2}{\operatorname{foldr}\left(\htmlData{mx=1}{\mathit{fees}}\right)}(\htmlData{mx=5}{\htmlData{mx=3}{\cdot} + \htmlData{mx=4}{\cdot}}, \htmlData{mx=6}{\mathit{receiver}})} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{\htmlData{mx=8}{\mathit{receiver}} + \htmlData{mx=11}{\operatorname{sum}\left(\htmlData{mx=10}{\mathit{fees}}\right)}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
f(x)Function application: List applied to Nat. Lean writes f x; papers write f(x). (List Nat)
e.ffoldr: foldr of fees: Lean's dot notation e.foldr means foldr applied to e. (fees.foldr)
=Equality: foldr(· + ·, receiver) and receiver + fees.sum are the same. (fees.foldr (· + ·) receiver = receiver …)
·Placeholder: Stands for the argument of an anonymous function: f (·) means x ↦ f x. (·)
+Addition: · plus ·. (· + ·)
e.fsum: sum of fees: Lean's dot notation e.sum means sum applied to e. (fees.sum)

theorem nlightning-multihop-fees-telescope (receiver : Nat) (fees : List Nat) :
    fees.foldr (· + ·) receiver = receiver + fees.sum

Abstract multi-hop amount aggregation law.

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

Accumulated hop fees telescope to receiver amount plus fee sum

How it was proved

More proved statements