proofs
Provednlightninglightningpr-14deep-formalization

Adjacent gossip block ranges partition their combined window

For all first,left,right,height∈N\htmlData{mx=1}{\mathit{first}, \mathit{left}, \mathit{right}, \mathit{height} \in \htmlData{mx=0}{\mathbb{N}}}, if first≤height∧height<first+(left+right)\htmlData{mx=0}{\mathit{first}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{height}} \mathbin{\htmlData{mx=10}{\land}} \htmlData{mx=3}{\mathit{height}} \mathrel{\htmlData{mx=9}{<}} \htmlData{mx=8}{\htmlData{mx=4}{\mathit{first}} + (\htmlData{mx=7}{\htmlData{mx=5}{\mathit{left}} + \htmlData{mx=6}{\mathit{right}}})}, then

(first≤height∧height<first+left)∨(first+left≤height∧height<first+left+right)\begin{aligned} & (\htmlData{mx=1}{\mathit{first}} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\mathit{height}} \mathbin{\htmlData{mx=9}{\land}} \htmlData{mx=4}{\mathit{height}} \mathrel{\htmlData{mx=8}{<}} \htmlData{mx=7}{\htmlData{mx=5}{\mathit{first}} + \htmlData{mx=6}{\mathit{left}}}) \\ & \htmlData{mx=0}{\lor} (\htmlData{mx=12}{\htmlData{mx=10}{\mathit{first}} + \htmlData{mx=11}{\mathit{left}}} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\mathit{height}} \mathbin{\htmlData{mx=22}{\land}} \htmlData{mx=15}{\mathit{height}} \mathrel{\htmlData{mx=21}{<}} \htmlData{mx=20}{\htmlData{mx=18}{\htmlData{mx=16}{\mathit{first}} + \htmlData{mx=17}{\mathit{left}}} + \htmlData{mx=19}{\mathit{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)
x ∈ TVariables
first, left, right, height range over natural numbers: the statement must hold for every choice. ((first left right height : Nat))
≤At most
first is less than or equal to height. (first ≤ height)
∧And
Both hold: first ≤ height, and height < first + (left + right). (first ≤ height ∧ height < first + (left…)
∨Or
At least one holds: first ≤ height ∧ height < first + left, or first + left ≤ height ∧ height < first + left + right. ((first ≤ height ∧ height < first + left…)
<Less than
height is strictly smaller than first + (left + right). (height < first + (left + right))
+Addition
left plus right. (left + right)

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