Provednlightninglightningpr-14deep-formalization

Commitment locktime and sequence tag bytes are distinct

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

\htmlData{mx=0}{\mathit{upper}} \mathrel{\htmlData{mx=3}{=}} \htmlData{mx=2}{0(\htmlData{mx=1}{\operatorname{x20}})} \mathrel{\htmlData{mx=8}{\implies}} \htmlData{mx=4}{\mathit{upper}} \mathrel{\htmlData{mx=7}{\neq}} \htmlData{mx=6}{0(\htmlData{mx=5}{\operatorname{x80}})}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
=Equality: upper and 0(x20) are the same. (upper = 0x20)
⟹Implies: If upper = 0(x20), then upper ≠ 0(x80). (Between types, A → B is the type of functions from A to B.) (upper = 0x20 → upper ≠ 0x80)
f(x)Function application: 0 applied to x20. Lean writes f x; papers write f(x). (0x20)
x20: x20: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (x20)
≠Not equal: upper and 0(x80) are different. (upper ≠ 0x80)
x80: x80: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (x80)

theorem nlightning-commitment-tags-distinct (upper : Nat) :
    upper = 0x20 → upper ≠ 0x80

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: Quot.sound, propext
Proof: 6 lines of Lean

Commitment locktime and sequence tag bytes are distinct

How it was proved

More proved statements