proofs
Provednlightninglightningpr-14deep-formalization

Liquidity-rate compatibility is convex within the advertised interval

For all minimum,maximum,a,b∈N\htmlData{mx=1}{\mathit{minimum}, \mathit{maximum}, a, b \in \htmlData{mx=0}{\mathbb{N}}}, if minimum≤a∧a≤maximum\htmlData{mx=0}{\mathit{minimum}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{a} \mathbin{\htmlData{mx=6}{\land}} \htmlData{mx=3}{a} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\mathit{maximum}}, a≤b\htmlData{mx=0}{a} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{b} and b≤maximum\htmlData{mx=0}{b} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{maximum}}, then

minimum≤b∧b≤maximum\htmlData{mx=0}{\mathit{minimum}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{b} \mathbin{\htmlData{mx=6}{\land}} \htmlData{mx=3}{b} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\mathit{maximum}}
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
minimum, maximum, a, b range over natural numbers: the statement must hold for every choice. ((minimum maximum a b : Nat))
≤At most
minimum is less than or equal to a. (minimum ≤ a)
∧And
Both hold: minimum ≤ a, and a ≤ maximum. (minimum ≤ a ∧ a ≤ maximum)

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
Classical.choice, Quot.sound, propext
Proof
6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements