proofs
Provednlightninglightningpr-14deep-formalization

Saturated offered-HTLC deadline is not before expiry

For all expiry,grace,maxHeight∈N\htmlData{mx=1}{\mathit{expiry}, \mathit{grace}, \mathit{maxHeight} \in \htmlData{mx=0}{\mathbb{N}}}, if expiry≤maxHeight\htmlData{mx=0}{\mathit{expiry}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{maxHeight}}, then

expiry≤min⁡(maxHeight,expiry+grace)\htmlData{mx=0}{\mathit{expiry}} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{\min(\htmlData{mx=1}{\mathit{maxHeight}}, \htmlData{mx=4}{\htmlData{mx=2}{\mathit{expiry}} + \htmlData{mx=3}{\mathit{grace}}})}
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, grace, maxHeight range over natural numbers: the statement must hold for every choice. ((expiry grace maxHeight : Nat))
≤At most
expiry is less than or equal to maxHeight. (expiry ≤ maxHeight)
minMinimum
The smaller of maxHeight and expiry + grace. (min maxHeight (expiry + grace))
+Addition
expiry plus grace. (expiry + grace)

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
Sign in to see the proofThe proof, its signed report and its history.

More proved statements