Provednlightninglightningpr-14formal-invariant

Subtracting a positive covered CLTV delta strictly decreases expiry

For all $\htmlData{mx=1}{\mathit{expiry}, \mathit{delta} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{delta}}$ and $\htmlData{mx=0}{\mathit{delta}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{expiry}}$ , then

\htmlData{mx=2}{\htmlData{mx=0}{\mathit{expiry}} - \htmlData{mx=1}{\mathit{delta}}} \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\mathit{expiry}}

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: expiry, delta range over natural numbers: the statement must hold for every choice. ((expiry delta : Nat))
<Less than: 0 is strictly smaller than delta. (0 < delta)
≤At most: delta is less than or equal to expiry. (delta ≤ expiry)
-Subtraction: expiry minus delta. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (expiry - delta)

theorem nlightning-cltv-route-decrease (expiry delta : Nat) (positive : 0 < delta) (covered : delta ≤ expiry) :
    expiry - delta < expiry

Single-hop arithmetic core of strictly decreasing route expiries.

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

Subtracting a positive covered CLTV delta strictly decreases expiry

How it was proved

More proved statements