Provednlightninglightningpr-14deep-formalization

Optional feature-bit pairing decodes its feature index

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

\htmlData{mx=3}{\frac{\htmlData{mx=2}{\htmlData{mx=1}{2\htmlData{mx=0}{\mathit{feature}}} + 1}}{2}} \mathrel{\htmlData{mx=5}{=}} \htmlData{mx=4}{\mathit{feature}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
a/bDivision: 2 · feature + 1 divided by 2. In Lean, dividing by 0 gives 0. ((2 * feature + 1) / 2)
=Equality: (2 · feature + 1)/2 and feature are the same. ((2 * feature + 1) / 2 = feature)
·Multiplication: 2 times feature. (2 * feature)
+Addition: 2 · feature plus 1. (2 * feature + 1)

theorem nlightning-feature-optional-decode (feature : Nat) :
    (2 * feature + 1) / 2 = feature

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

Optional feature-bit pairing decodes its feature index

How it was proved

More proved statements