Provednlightninglightningpr-14formal-invariant

Forwarding required amount expands to amount plus policy fee

For all $\htmlData{mx=1}{\mathit{base}, \mathit{ppm}, \mathit{amount} \in \htmlData{mx=0}{\mathbb{N}}}$ :

\begin{aligned} & \htmlData{mx=8}{\htmlData{mx=1}{\mathit{amount}} + \left(\htmlData{mx=7}{\htmlData{mx=2}{\mathit{base}} + \htmlData{mx=6}{\frac{\htmlData{mx=5}{\htmlData{mx=3}{\mathit{amount}} \cdot \htmlData{mx=4}{\mathit{ppm}}}}{1000000}}}\right)} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=16}{\htmlData{mx=11}{\htmlData{mx=9}{\mathit{amount}} + \htmlData{mx=10}{\mathit{base}}} + \htmlData{mx=15}{\frac{\htmlData{mx=14}{\htmlData{mx=12}{\mathit{amount}} \cdot \htmlData{mx=13}{\mathit{ppm}}}}{1000000}}} \end{aligned}

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: base, ppm, amount range over natural numbers: the statement must hold for every choice. ((base ppm amount : Nat))
=Equality: amount + (base + amount · ppm/1000000) and amount + base + amount · ppm/1000000 are the same. (amount + (base + amount * ppm / 1000000…)
+Addition: base plus amount · ppm/1000000. (base + amount * ppm / 1000000)
·Multiplication: amount times ppm. (amount * ppm)
a/bDivision: amount · ppm divided by 1000000. In Lean, dividing by 0 gives 0. (amount * ppm / 1000000)

theorem nlightning-forwarding-fee-boundary (base ppm amount : Nat) :
    amount + (base + amount * ppm / 1000000) = amount + base + amount * ppm / 1000000

Exact Nat model of ForwardingFee.RequiredIncomingMsat, ignoring checked-machine overflow.

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

Forwarding required amount expands to amount plus policy fee

How it was proved

More proved statements