Provednlightninglightningpr-14deep-formalization

A larger safety margin moves an HTLC deadline no later

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

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

theorem nlightning-larger-safety-earlier-deadline (expiry fulfill failBack : Nat) (ordered : fulfill ≤ failBack) :
    (if failBack < expiry then expiry - failBack else 0) ≤ (if fulfill < expiry then expiry - fulfill else 0)

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 larger safety margin moves an HTLC deadline no later

How it was proved

More proved statements