proofs
Provednlightninglightningpr-14deep-formalization

Membership in a gossip block window bounds the offset

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

first≤height∧height−first<count\htmlData{mx=0}{\mathit{first}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{height}} \mathbin{\htmlData{mx=8}{\land}} \htmlData{mx=5}{\htmlData{mx=3}{\mathit{height}} - \htmlData{mx=4}{\mathit{first}}} \mathrel{\htmlData{mx=7}{<}} \htmlData{mx=6}{\mathit{count}}
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, count, height range over natural numbers: the statement must hold for every choice. ((first count height : Nat))
≤At most
first is less than or equal to height. (first ≤ height)
∧And
Both hold: first ≤ height, and height < first + count. (first ≤ height ∧ height < first + count)
<Less than
height is strictly smaller than first + count. (height < first + count)
-Subtraction
height minus first. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (height - first)
+Addition
first plus count. (first + count)

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