proofs
Provednlightninglightningpr-14deep-formalization

Millisatoshi flooring lies between adjacent satoshi boundaries

For all msat∈N\htmlData{mx=1}{\mathit{msat} \in \htmlData{mx=0}{\mathbb{N}}}:

msat1000⋅1000≤msat∧msat<(msat1000+1)⋅1000\htmlData{mx=2}{\htmlData{mx=1}{\frac{\htmlData{mx=0}{\mathit{msat}}}{1000}} \cdot 1000} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\mathit{msat}} \mathbin{\htmlData{mx=11}{\land}} \htmlData{mx=5}{\mathit{msat}} \mathrel{\htmlData{mx=10}{<}} \htmlData{mx=9}{\left(\htmlData{mx=8}{\htmlData{mx=7}{\frac{\htmlData{mx=6}{\mathit{msat}}}{1000}} + 1}\right) \cdot 1000}
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
msat/1000 times 1000. ((msat / 1000) * 1000)
≤At most
msat/1000 · 1000 is less than or equal to msat. ((msat / 1000) * 1000 ≤ msat)
∧And
Both hold: msat/1000 · 1000 ≤ msat, and msat < (msat/1000 + 1) · 1000. ((msat / 1000) * 1000 ≤ msat ∧ msat < (m…)
a/bDivision
msat divided by 1000. In Lean, dividing by 0 gives 0. (msat / 1000)
<Less than
msat is strictly smaller than (msat/1000 + 1) · 1000. (msat < (msat / 1000 + 1) * 1000)
+Addition
msat/1000 plus 1. (msat / 1000 + 1)

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
Classical.choice, Quot.sound, propext
Proof
6 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements