Provednlightninglightningpr-14deep-formalization

Commitment-number XOR obscuring is an involution

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

\htmlData{mx=6}{\htmlData{mx=0}{\operatorname{xor}}(\htmlData{mx=4}{\htmlData{mx=1}{\operatorname{xor}}(\htmlData{mx=2}{\mathit{number}}, \htmlData{mx=3}{\mathit{factor}})}, \htmlData{mx=5}{\mathit{factor}})} \mathrel{\htmlData{mx=8}{=}} \htmlData{mx=7}{\mathit{number}}

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: number, factor range over natural numbers: the statement must hold for every choice. ((number factor : Nat))
xor: Nat.xor: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nat.xor)
=Equality: xor(xor(number, factor), factor) and number are the same. (Nat.xor (Nat.xor number factor) factor …)
f(x)Function application: Nat.xor applied to number, factor. Lean writes f x; papers write f(x). (Nat.xor number factor)

theorem nlightning-commitment-obscure-involution (number factor : Nat) :
    Nat.xor (Nat.xor number factor) factor = number

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-number XOR obscuring is an involution

How it was proved

More proved statements