Provednlightninglightningpr-14formal-invariant

Forwarding fee acceptance is upward closed in incoming amount

For all $\htmlData{mx=1}{\mathit{required}, \mathit{incoming}, \mathit{larger} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{\mathit{required}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{incoming}}$ and $\htmlData{mx=0}{\mathit{incoming}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{larger}}$ , then

\htmlData{mx=0}{\mathit{required}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{larger}}

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: required, incoming, larger range over natural numbers: the statement must hold for every choice. ((required incoming larger : Nat))
≤At most: required is less than or equal to incoming. (required ≤ incoming)

theorem nlightning-fee-acceptance-upward-closed (required incoming larger : Nat) (h₁ : required ≤ incoming) (h₂ : incoming ≤ larger) :
    required ≤ larger

Order-theoretic core of forwarding fee sufficiency.

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

Forwarding fee acceptance is upward closed in incoming amount

How it was proved

More proved statements