Provednlightninglightningpr-14formal-invariant

Rounded-up collaborative fee is within one satoshi of floor

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

\begin{aligned} & \htmlData{mx=2}{\frac{\htmlData{mx=1}{\mathit{product}}}{1000}} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\frac{\htmlData{mx=4}{\htmlData{mx=3}{\mathit{product}} + 999}}{1000}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=9}{\frac{\htmlData{mx=8}{\htmlData{mx=7}{\mathit{product}} + 999}}{1000}} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\htmlData{mx=11}{\frac{\htmlData{mx=10}{\mathit{product}}}{1000}} + 1} \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)
a/bDivision: product divided by 1000. In Lean, dividing by 0 gives 0. (product / 1000)
≤At most: product/1000 is less than or equal to (product + 999)/1000. (product / 1000 ≤ (product + 999) / 1000)
∧And: Both hold: product/1000 ≤ (product + 999)/1000, and (product + 999)/1000 ≤ product/1000 + 1. (product / 1000 ≤ (product + 999) / 1000…)
+Addition: product plus 999. (product + 999)

theorem nlightning-rounded-fee-sandwich (product : Nat) :
    product / 1000 ≤ (product + 999) / 1000 ∧ (product + 999) / 1000 ≤ product / 1000 + 1

Arithmetic relation between FeeForWeight and MinimumFeeForWeight.

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: Classical.choice, Quot.sound, propext
Proof: 7 lines of Lean