Provednlightninglightningpr-14deep-formalization

Money division reconstructs the original millisatoshi amount

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

\htmlData{mx=8}{\htmlData{mx=2}{\htmlData{mx=0}{\mathit{amount}} \bmod \htmlData{mx=1}{\mathit{parts}}} + \htmlData{mx=7}{\htmlData{mx=3}{\mathit{parts}} \cdot \left(\htmlData{mx=6}{\frac{\htmlData{mx=4}{\mathit{amount}}}{\htmlData{mx=5}{\mathit{parts}}}}\right)}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\mathit{amount}}

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: amount, parts range over natural numbers: the statement must hold for every choice. ((amount parts : Nat))
modRemainder: The remainder when amount is divided by parts. (amount % parts)
+Addition: amount % parts plus parts · (amount/parts). (amount % parts + parts * (amount / part…)
=Equality: amount % parts + parts · (amount/parts) and amount are the same. (amount % parts + parts * (amount / part…)
·Multiplication: parts times amount/parts. (parts * (amount / parts))
a/bDivision: amount divided by parts. In Lean, dividing by 0 gives 0. (amount / parts)

theorem nlightning-money-division-reconstructs (amount parts : Nat) :
    amount % parts + parts * (amount / parts) = amount

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: propext
Proof: 6 lines of Lean

Money division reconstructs the original millisatoshi amount

How it was proved

More proved statements