Provednlightninglightningpr-14formal-invariant

Commitment weight is monotone in untrimmed HTLC count

For all $\htmlData{mx=1}{\mathit{base}, n, m \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{n} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{m}$ , then

\htmlData{mx=3}{\htmlData{mx=0}{\mathit{base}} + \htmlData{mx=2}{\htmlData{mx=1}{n} \cdot 172}} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\htmlData{mx=4}{\mathit{base}} + \htmlData{mx=6}{\htmlData{mx=5}{m} \cdot 172}}

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: base, n, m range over natural numbers: the statement must hold for every choice. ((base n m : Nat))
≤At most: n is less than or equal to m. (n ≤ m)
+Addition: base plus n · 172. (base + n * 172)
·Multiplication: n times 172. (n * 172)

theorem nlightning-commitment-weight-monotone (base n m : Nat) (h : n ≤ m) :
    base + n * 172 ≤ base + m * 172

Abstract monotonicity of the affine commitment weight formula.

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

Commitment weight is monotone in untrimmed HTLC count

How it was proved

More proved statements