proofs
Provednlightninglightningpr-14deep-formalization

Base plus proportional liquidity fee is monotone

For all base,basis,a,b∈N\htmlData{mx=1}{\mathit{base}, \mathit{basis}, a, b \in \htmlData{mx=0}{\mathbb{N}}}, if a≤b\htmlData{mx=0}{a} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{b}, then

base+a⋅basis10000≤base+b⋅basis10000\htmlData{mx=5}{\htmlData{mx=0}{\mathit{base}} + \htmlData{mx=4}{\frac{\htmlData{mx=3}{\htmlData{mx=1}{a} \cdot \htmlData{mx=2}{\mathit{basis}}}}{10000}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\htmlData{mx=6}{\mathit{base}} + \htmlData{mx=10}{\frac{\htmlData{mx=9}{\htmlData{mx=7}{b} \cdot \htmlData{mx=8}{\mathit{basis}}}}{10000}}}
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, basis, a, b range over natural numbers: the statement must hold for every choice. ((base basis a b : Nat))
≤At most
a is less than or equal to b. (a ≤ b)
+Addition
base plus a · basis/10000. (base + a * basis / 10000)
·Multiplication
a times basis. (a * basis)
a/bDivision
a · basis divided by 10000. In Lean, dividing by 0 gives 0. (a * basis / 10000)

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