Provednlightninglightningpr-14formal-invariant

Accepted splice RBF total fee is nondecreasing

For all $\htmlData{mx=1}{\mathit{previous}, \mathit{current} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=3}{\lnot \htmlData{mx=0}{\mathit{current}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{\mathit{previous}}}$ , then

\htmlData{mx=0}{\mathit{previous}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{current}}

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: previous, current range over natural numbers: the statement must hold for every choice. ((previous current : Nat))
¬Not: It is not the case that current < previous. (¬ current < previous)
≤At most: previous is less than or equal to current. (previous ≤ current)
<Less than: current is strictly smaller than previous. (current < previous)

theorem nlightning-rbf-fee-nondecrease (previous current : Nat) (accepted : ¬ current < previous) :
    previous ≤ current

Arithmetic consequence of rejecting current total fees below the prior attempt.

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

Accepted splice RBF total fee is nondecreasing

How it was proved

More proved statements