Provednlightninglightningpr-14deep-formalization

A zero-length gossip block range contains no height

For all $\htmlData{mx=1}{\mathit{first}, \mathit{height} \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=8}{\lnot (\htmlData{mx=0}{\mathit{first}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{\mathit{height}} \mathbin{\htmlData{mx=7}{\land}} \htmlData{mx=3}{\mathit{height}} \mathrel{\htmlData{mx=6}{<}} \htmlData{mx=5}{\htmlData{mx=4}{\mathit{first}} + 0})}

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, height range over natural numbers: the statement must hold for every choice. ((first height : Nat))
¬Not: It is not the case that first ≤ height ∧ height < first + 0. (¬ (first ≤ height ∧ height < first + 0))
≤At most: first is less than or equal to height. (first ≤ height)
∧And: Both hold: first ≤ height, and height < first + 0. (first ≤ height ∧ height < first + 0)
<Less than: height is strictly smaller than first + 0. (height < first + 0)
+Addition: first plus 0. (first + 0)

theorem nlightning-empty-block-range (first height : Nat) :
    ¬ (first ≤ height ∧ height < first + 0)

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: propext
Proof: 6 lines of Lean

A zero-length gossip block range contains no height

How it was proved

More proved statements