proofs
Provednlightninglightningpr-14deep-formalization

Mutual-close weight is monotone in both script lengths

For all l1,l2,r1,r2∈N\htmlData{mx=1}{l_{1}, l_{2}, r_{1}, r_{2} \in \htmlData{mx=0}{\mathbb{N}}}, if l1≤l2\htmlData{mx=0}{l_{1}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{l_{2}} and r1≤r2\htmlData{mx=0}{r_{1}} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{r_{2}}, then

(47+(9+l1)+(9+r1))⋅4+224≤(47+(9+l2)+(9+r2))⋅4+224\begin{aligned} & \htmlData{mx=8}{\htmlData{mx=7}{(\htmlData{mx=6}{\htmlData{mx=3}{47 + (\htmlData{mx=2}{9 + \htmlData{mx=1}{l_{1}}})} + (\htmlData{mx=5}{9 + \htmlData{mx=4}{r_{1}}})}) \cdot 4} + 224} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=16}{\htmlData{mx=15}{(\htmlData{mx=14}{\htmlData{mx=11}{47 + (\htmlData{mx=10}{9 + \htmlData{mx=9}{l_{2}}})} + (\htmlData{mx=13}{9 + \htmlData{mx=12}{r_{2}}})}) \cdot 4} + 224} \end{aligned}
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
l₁, l₂, r₁, r₂ range over natural numbers: the statement must hold for every choice. ((l₁ l₂ r₁ r₂ : Nat))
≤At most
l₁ is less than or equal to l₂. (l₁ ≤ l₂)
·Multiplication
47 + (9 + l₁) + (9 + r₁) times 4. ((47 + (9 + l₁) + (9 + r₁)) * 4)
+Addition
9 plus l₁. (9 + l₁)

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
Sign in to see the proofThe proof, its signed report and its history.

More proved statements