Provednlightninglightningpr-14formal-invariant

Not trimmed is equivalent to meeting the dust-plus-fee threshold

For all $\htmlData{mx=1}{\mathit{amount}, \mathit{dust}, \mathit{fee} \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=6}{\lnot \htmlData{mx=1}{\frac{\htmlData{mx=0}{\mathit{amount}}}{1000}} \mathrel{\htmlData{mx=5}{<}} \htmlData{mx=4}{\htmlData{mx=2}{\mathit{dust}} + \htmlData{mx=3}{\mathit{fee}}}} \mathrel{\htmlData{mx=13}{\iff}} \htmlData{mx=9}{\htmlData{mx=7}{\mathit{dust}} + \htmlData{mx=8}{\mathit{fee}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\frac{\htmlData{mx=10}{\mathit{amount}}}{1000}}

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: amount, dust, fee range over natural numbers: the statement must hold for every choice. ((amount dust fee : Nat))
⟺If and only if: ¬(amount/1000 < dust + fee) holds exactly when dust + fee ≤ amount/1000 holds. ((¬ amount / 1000 < dust + fee) ↔ dust +…)
¬Not: It is not the case that amount/1000 < dust + fee. (¬ amount / 1000 < dust + fee)
a/bDivision: amount divided by 1000. In Lean, dividing by 0 gives 0. (amount / 1000)
<Less than: amount/1000 is strictly smaller than dust + fee. (amount / 1000 < dust + fee)
+Addition: dust plus fee. (dust + fee)
≤At most: dust + fee is less than or equal to amount/1000. (dust + fee ≤ amount / 1000)

theorem nlightning-htlc-trim-threshold-complement (amount dust fee : Nat) :
    (¬ amount / 1000 < dust + fee) ↔ dust + fee ≤ amount / 1000

Linear-order complement of the exact HTLC trimming predicate.

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: Classical.choice, Quot.sound, propext
Proof: 6 lines of Lean