Provednlightninglightningpr-14deep-formalization
Packed short-channel ID recovers its block height
For all , if and , 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
- tx is strictly smaller than 2^24. (
tx < 2^24) - a/bDivision
- block · 2^40 + tx · 2^16 + out divided by 2^40. In Lean, dividing by 0 gives 0. (
(block * 2^40 + tx * 2^16 + out) / 2^40) - =Equality
- (block · 2^40 + tx · 2^16 + out)/2^40 and block are the same. (
(block * 2^40 + tx * 2^16 + out) / 2^40…) - ·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 24. (
2^24)
theorem nlightning-scid-block-roundtrip (block tx out : Nat) (txBound : tx < 2^24) (outBound : out < 2^16) :
(block * 2^40 + tx * 2^16 + out) / 2^40 = blockRepository-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.