Provednlightninglightningpr-14formal-invariant

Two 330-satoshi anchors add a 660-satoshi funder cost

For all $\htmlData{mx=1}{\mathit{baseFee} \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{\mathit{baseFee}} + \htmlData{mx=1}{2 \cdot 330}} \mathrel{\htmlData{mx=5}{=}} \htmlData{mx=4}{\htmlData{mx=3}{\mathit{baseFee}} + 660}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
+Addition: baseFee plus 2 · 330. (baseFee + 2 * 330)
=Equality: baseFee + 2 · 330 and baseFee + 660 are the same. (baseFee + 2 * 330 = baseFee + 660)
·Multiplication: 2 times 330. (2 * 330)

theorem nlightning-anchor-funder-surcharge (baseFee : Nat) :
    baseFee + 2 * 330 = baseFee + 660

Exact arithmetic normalization of the anchor funder surcharge.

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