Provednlightninglightningpr-14deep-formalization

Commitment-number 24-bit halves recombine exactly

For all $\htmlData{mx=1}{\mathit{obscured} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{\mathit{obscured}} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{2^{48}}$ , then

\htmlData{mx=8}{\htmlData{mx=4}{\htmlData{mx=2}{\frac{\htmlData{mx=0}{\mathit{obscured}}}{\htmlData{mx=1}{2^{24}}}} \cdot \htmlData{mx=3}{2^{24}}} + \htmlData{mx=7}{\htmlData{mx=5}{\mathit{obscured}} \bmod \htmlData{mx=6}{2^{24}}}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\mathit{obscured}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
<Less than: obscured is strictly smaller than 2^48. (obscured < 2^48)
·Multiplication: obscured/2^24 times 2^24. ((obscured / 2^24) * 2^24)
+Addition: obscured/2^24 · 2^24 plus obscured % 2^24. ((obscured / 2^24) * 2^24 + obscured % 2…)
=Equality: obscured/2^24 · 2^24 + obscured % 2^24 and obscured are the same. ((obscured / 2^24) * 2^24 + obscured % 2…)
a/bDivision: obscured divided by 2^24. In Lean, dividing by 0 gives 0. (obscured / 2^24)
aᵇPower: 2 raised to the power 48. (2^48)
modRemainder: The remainder when obscured is divided by 2^24. (obscured % 2^24)

theorem nlightning-commitment-halves-recombine (obscured : Nat) (bound : obscured < 2^48) :
    (obscured / 2^24) * 2^24 + obscured % 2^24 = obscured

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 24-bit halves recombine exactly

How it was proved

More proved statements