Provednlightninglightningpr-14deep-formalization
Packed short-channel ID recovers its output index
For all , if , then
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
- block, tx, out range over natural numbers: the statement must hold for every choice. (
(block tx out : Nat)) - <Less than
- out is strictly smaller than 2^16. (
out < 2^16) - modRemainder
- The remainder when block · 2^40 + tx · 2^16 + out is divided by 2^16. (
(block * 2^40 + tx * 2^16 + out) % 2^16) - =Equality
- (block · 2^40 + tx · 2^16 + out) % 2^16 and out are the same. (
(block * 2^40 + tx * 2^16 + out) % 2^16…) - ·Multiplication
- block times 2^40. (
block * 2^40) - +Addition
- block · 2^40 plus tx · 2^16. (
block * 2^40 + tx * 2^16) - aᵇPower
- 2 raised to the power 16. (
2^16)
theorem nlightning-scid-output-roundtrip (block tx out : Nat) (outBound : out < 2^16) :
(block * 2^40 + tx * 2^16 + out) % 2^16 = outRepository-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
Sign in to see the proofThe proof, its signed report and its history.