proofs
Provednlightninglightningpr-14formal-invariant

Rounded-down commitment base fee is monotone in feerate

For all r1,r2,weight∈N\htmlData{mx=1}{r_{1}, r_{2}, \mathit{weight} \in \htmlData{mx=0}{\mathbb{N}}}, if r1≤r2\htmlData{mx=0}{r_{1}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{r_{2}}, then

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

Fixed-weight monotonicity for feerate * weight / 1000.

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