proofs
Provednlightninglightningpr-14deep-formalization

Mutual-close fee is monotone in transaction weight

For all rate,w1,w2∈N\htmlData{mx=1}{\mathit{rate}, w_{1}, w_{2} \in \htmlData{mx=0}{\mathbb{N}}}, if w1≤w2\htmlData{mx=0}{w_{1}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{w_{2}}, then

rate⋅w11000≤rate⋅w21000\htmlData{mx=3}{\frac{\htmlData{mx=2}{\htmlData{mx=0}{\mathit{rate}} \cdot \htmlData{mx=1}{w_{1}}}}{1000}} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\frac{\htmlData{mx=6}{\htmlData{mx=4}{\mathit{rate}} \cdot \htmlData{mx=5}{w_{2}}}}{1000}}
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
rate, w₁, w₂ range over natural numbers: the statement must hold for every choice. ((rate w₁ w₂ : Nat))
≤At most
w₁ is less than or equal to w₂. (w₁ ≤ w₂)
·Multiplication
rate times w₁. (rate * w₁)
a/bDivision
rate · w₁ divided by 1000. In Lean, dividing by 0 gives 0. (rate * w₁ / 1000)

Repository-grounded Lean formalization for NLightning PR #14. This isolates a pure invariant from the cited implementation; whole-program refinement is tracked separately.

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
Sign in to see the proofThe proof, its signed report and its history.

More proved statements