Provednlightninglightningpr-14formal-invariant

BOLT 7 forwarding fee worked example is 10,199 msat

\htmlData{mx=2}{200 + \htmlData{mx=1}{\frac{\htmlData{mx=0}{4999999 \cdot 2000}}{1000000}}} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{10199}

What the notation means · or point at any symbol

+Addition: 200 plus 4999999 · 2000/1000000. (200 + 4999999 * 2000 / 1000000)
=Equality: 200 + 4999999 · 2000/1000000 and 10199 are the same. (200 + 4999999 * 2000 / 1000000 = (10199…)
·Multiplication: 4999999 times 2000. (4999999 * 2000)
a/bDivision: 4999999 · 2000 divided by 1000000. In Lean, dividing by 0 gives 0. (4999999 * 2000 / 1000000)
(x : T)As natural numbers: 10199 read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((10199 : Nat))

theorem nlightning-forwarding-fee-example :
    200 + 4999999 * 2000 / 1000000 = (10199 : Nat)

Exact arithmetic example documented in ForwardingFee.

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