proofs
Provednlightninglightningpr-14formal-invariant

Incoming below outgoing cannot cover a nonnegative forwarding fee

For all incoming,outgoing,fee∈N\htmlData{mx=1}{\mathit{incoming}, \mathit{outgoing}, \mathit{fee} \in \htmlData{mx=0}{\mathbb{N}}}, if incoming<outgoing\htmlData{mx=0}{\mathit{incoming}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{\mathit{outgoing}}, then

¬incoming≥outgoing+fee\htmlData{mx=5}{\lnot \htmlData{mx=0}{\mathit{incoming}} \mathrel{\htmlData{mx=4}{\geq}} \htmlData{mx=3}{\htmlData{mx=1}{\mathit{outgoing}} + \htmlData{mx=2}{\mathit{fee}}}}
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
incoming, outgoing, fee range over natural numbers: the statement must hold for every choice. ((incoming outgoing fee : Nat))
<Less than
incoming is strictly smaller than outgoing. (incoming < outgoing)
¬Not
It is not the case that incoming ≥ outgoing + fee. (¬ incoming ≥ outgoing + fee)
≥At least
incoming is greater than or equal to outgoing + fee. (incoming ≥ outgoing + fee)
+Addition
outgoing plus fee. (outgoing + fee)

Abstract arithmetic core of PaysSufficientFee's early rejection.

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