Provednlightninglightningpr-14deep-formalization

Money split remainder is smaller than the positive part count

For all $\htmlData{mx=1}{\mathit{amount}, \mathit{parts} \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\mathit{parts}}$ , then

\htmlData{mx=2}{\htmlData{mx=0}{\mathit{amount}} \bmod \htmlData{mx=1}{\mathit{parts}}} \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\mathit{parts}}

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))
<Less than: 0 is strictly smaller than parts. (0 < parts)
modRemainder: The remainder when amount is divided by parts. (amount % parts)

theorem nlightning-money-split-remainder-bound (amount parts : Nat) (positive : 0 < parts) :
    amount % parts < parts

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

Money split remainder is smaller than the positive part count

How it was proved

More proved statements