Provednlightninglightningpr-14deep-formalization

Mutual-close estimated weight is symmetric in output scripts

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

\begin{aligned} & \htmlData{mx=8}{\htmlData{mx=7}{(\htmlData{mx=6}{\htmlData{mx=3}{47 + (\htmlData{mx=2}{9 + \htmlData{mx=1}{\mathit{localLen}}})} + (\htmlData{mx=5}{9 + \htmlData{mx=4}{\mathit{remoteLen}}})}) \cdot 4} + 224} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=16}{\htmlData{mx=15}{(\htmlData{mx=14}{\htmlData{mx=11}{47 + (\htmlData{mx=10}{9 + \htmlData{mx=9}{\mathit{remoteLen}}})} + (\htmlData{mx=13}{9 + \htmlData{mx=12}{\mathit{localLen}}})}) \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: localLen, remoteLen range over natural numbers: the statement must hold for every choice. ((localLen remoteLen : Nat))
·Multiplication: 47 + (9 + localLen) + (9 + remoteLen) times 4. ((47 + (9 + localLen) + (9 + remoteLen))…)
=Equality: (47 + (9 + localLen) + (9 + remoteLen)) · 4 + 224 and (47 + (9 + remoteLen) + (9 + localLen)) · 4 + 224 are the same. ((47 + (9 + localLen) + (9 + remoteLen))…)
+Addition: 9 plus localLen. (9 + localLen)

theorem nlightning-close-weight-symmetric (localLen remoteLen : Nat) :
    (47 + (9 + localLen) + (9 + remoteLen)) * 4 + 224 = (47 + (9 + remoteLen) + (9 + localLen)) * 4 + 224

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

Mutual-close estimated weight is symmetric in output scripts

How it was proved

More proved statements