Provednlightninglightningpr-14formal-invariant

Anchor HTLC timeout and success base fees are zero

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

\begin{aligned} & \left(\left(\htmlData{mx=5}{\begin{cases} 0 & \text{if } \htmlData{mx=1}{\operatorname{true}} \\ \htmlData{mx=4}{\frac{\htmlData{mx=3}{\htmlData{mx=2}{\mathit{rate}} \cdot 663}}{1000}} & \text{otherwise} \end{cases}}\right) \mathrel{\htmlData{mx=6}{=}} 0\right) \\ & \htmlData{mx=0}{\land} \left(\left(\htmlData{mx=11}{\begin{cases} 0 & \text{if } \htmlData{mx=7}{\operatorname{true}} \\ \htmlData{mx=10}{\frac{\htmlData{mx=9}{\htmlData{mx=8}{\mathit{rate}} \cdot 703}}{1000}} & \text{otherwise} \end{cases}}\right) \mathrel{\htmlData{mx=12}{=}} 0\right) \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)
∧And: Both hold: 0 if true, else rate · 663/1000 = 0, and 0 if true, else rate · 703/1000 = 0. (((if true then 0 else rate * 663 / 1000…)
=Equality: 0 if true, else rate · 663/1000 and 0 are the same. ((if true then 0 else rate * 663 / 1000)…)
{ a if c; b otherwiseCases (if … then … else): 0 when true, and rate · 663/1000 otherwise. (if true then 0 else rate * 663 / 1000)
true: true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (true)
·Multiplication: rate times 663. (rate * 663)
a/bDivision: rate · 663 divided by 1000. In Lean, dividing by 0 gives 0. (rate * 663 / 1000)

theorem nlightning-anchor-second-stage-zero (rate : Nat) :
    ((if true then 0 else rate * 663 / 1000) = 0) ∧ ((if true then 0 else rate * 703 / 1000) = 0)

Direct model of the anchor branch in both second-stage fee formulas.

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

Anchor HTLC timeout and success base fees are zero

How it was proved

More proved statements