Provednlightninglightningpr-14deep-formalization

A fulfilled-HTLC deadline never lies after its expiry

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

\left(\htmlData{mx=6}{\begin{cases} \htmlData{mx=2}{\htmlData{mx=0}{\mathit{expiry}} - \htmlData{mx=1}{\mathit{safety}}} & \text{if } \htmlData{mx=3}{\mathit{safety}} \mathrel{\htmlData{mx=5}{<}} \htmlData{mx=4}{\mathit{expiry}} \\ 0 & \text{otherwise} \end{cases}}\right) \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\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, safety range over natural numbers: the statement must hold for every choice. ((expiry safety : Nat))
≤At most: expiry − safety if safety < expiry, else 0 is less than or equal to expiry. ((if safety < expiry then expiry - safet…)
{ a if c; b otherwiseCases (if … then … else): expiry − safety when safety < expiry, and 0 otherwise. (if safety < expiry then expiry - safety…)
<Less than: safety is strictly smaller than expiry. (safety < expiry)
-Subtraction: expiry minus safety. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (expiry - safety)

theorem nlightning-fulfill-deadline-bounded (expiry safety : Nat) :
    (if safety < expiry then expiry - safety else 0) ≤ expiry

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

A fulfilled-HTLC deadline never lies after its expiry

How it was proved

More proved statements