proofs
Provednlightninglightningpr-14deep-formalization

Every BOLT 12 offer-field range lies in the invoice-request range

For all t∈N\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}}:

((1≤t∧t≤79∨1000000000≤t∧t≤1999999999)  ⟹  (t≤159∨1000000000≤t∧t≤2999999999))\begin{aligned} & \left(\right. (1 \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{t} \mathbin{\htmlData{mx=5}{\land}} \htmlData{mx=3}{t} \mathrel{\htmlData{mx=4}{\leq}} 79 \mathbin{\htmlData{mx=11}{\lor}} 1000000000 \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{t} \mathbin{\htmlData{mx=10}{\land}} \htmlData{mx=8}{t} \mathrel{\htmlData{mx=9}{\leq}} 1999999999) \\ & \htmlData{mx=0}{\implies} (\htmlData{mx=12}{t} \mathrel{\htmlData{mx=13}{\leq}} 159 \mathbin{\htmlData{mx=19}{\lor}} 1000000000 \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{t} \mathbin{\htmlData{mx=18}{\land}} \htmlData{mx=16}{t} \mathrel{\htmlData{mx=17}{\leq}} 2999999999) \left.\right) \end{aligned}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
⟹Implies
If 1 ≤ t ∧ t ≤ 79 ∨ 1000000000 ≤ t ∧ t ≤ 1999999999, then t ≤ 159 ∨ 1000000000 ≤ t ∧ t ≤ 2999999999. (Between types, A → B is the type of functions from A to B.) (((1 ≤ t ∧ t ≤ 79) ∨ (1000000000 ≤ t ∧ t…)
∨Or
At least one holds: 1 ≤ t ∧ t ≤ 79, or 1000000000 ≤ t ∧ t ≤ 1999999999. ((1 ≤ t ∧ t ≤ 79) ∨ (1000000000 ≤ t ∧ t …)
≤At most
1 is less than or equal to t. (1 ≤ t)
∧And
Both hold: 1 ≤ t, and t ≤ 79. (1 ≤ t ∧ t ≤ 79)

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