Provednlightninglightningpr-14deep-formalization

Short-channel ID packing is injective within field bounds

For all $\htmlData{mx=1}{b_{1}, t_{1}, o_{1}, b_{2}, t_{2}, o_{2} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{t_{1}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{24}}$ , $\htmlData{mx=0}{t_{2}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{24}}$ , $\htmlData{mx=0}{o_{1}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{16}}$ , $\htmlData{mx=0}{o_{2}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{16}}$ and $\htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{b_{1}} \cdot \htmlData{mx=1}{2^{40}}} + \htmlData{mx=5}{\htmlData{mx=3}{t_{1}} \cdot \htmlData{mx=4}{2^{16}}}} + \htmlData{mx=7}{o_{1}}} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\htmlData{mx=15}{\htmlData{mx=11}{\htmlData{mx=9}{b_{2}} \cdot \htmlData{mx=10}{2^{40}}} + \htmlData{mx=14}{\htmlData{mx=12}{t_{2}} \cdot \htmlData{mx=13}{2^{16}}}} + \htmlData{mx=16}{o_{2}}}$ , then

\htmlData{mx=0}{b_{1}} \mathrel{\htmlData{mx=2}{=}} \htmlData{mx=1}{b_{2}} \mathbin{\htmlData{mx=10}{\land}} \htmlData{mx=3}{t_{1}} \mathrel{\htmlData{mx=5}{=}} \htmlData{mx=4}{t_{2}} \mathbin{\htmlData{mx=9}{\land}} \htmlData{mx=6}{o_{1}} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{o_{2}}

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: b₁, t₁, o₁, b₂, t₂, o₂ range over natural numbers: the statement must hold for every choice. ((b₁ t₁ o₁ b₂ t₂ o₂ : Nat))
<Less than: t₁ is strictly smaller than 2^24. (t₁ < 2^24)
·Multiplication: b₁ times 2^40. (b₁ * 2^40)
+Addition: b₁ · 2^40 plus t₁ · 2^16. (b₁ * 2^40 + t₁ * 2^16)
=Equality: b₁ · 2^40 + t₁ · 2^16 + o₁ and b₂ · 2^40 + t₂ · 2^16 + o₂ are the same. (b₁ * 2^40 + t₁ * 2^16 + o₁ = b₂ * 2^40 …)
aᵇPower: 2 raised to the power 24. (2^24)
∧And: Both hold: t₁ = t₂, and o₁ = o₂. (t₁ = t₂ ∧ o₁ = o₂)

theorem nlightning-scid-pack-injective (b₁ t₁ o₁ b₂ t₂ o₂ : Nat) (t₁b : t₁ < 2^24) (t₂b : t₂ < 2^24) (o₁b : o₁ < 2^16) (o₂b : o₂ < 2^16) (same : b₁ * 2^40 + t₁ * 2^16 + o₁ = b₂ * 2^40 + t₂ * 2^16 + o₂) :
    b₁ = b₂ ∧ t₁ = t₂ ∧ o₁ = o₂

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

Short-channel ID packing is injective within field bounds

How it was proved

More proved statements