Provednlightninglightningpr-14deep-formalization

Satoshi to millisatoshi conversion and flooring round-trips

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

\htmlData{mx=2}{\frac{\htmlData{mx=1}{\htmlData{mx=0}{\mathit{sats}} \cdot 1000}}{1000}} \mathrel{\htmlData{mx=4}{=}} \htmlData{mx=3}{\mathit{sats}}

What the notation means · or point at any symbol

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

theorem nlightning-satoshi-msat-roundtrip (sats : Nat) :
    sats * 1000 / 1000 = sats

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

Satoshi to millisatoshi conversion and flooring round-trips

How it was proved

More proved statements