Provednlightninglightningpr-14formal-invariant

Route cost is additive under path concatenation

For all $\htmlData{mx=3}{\mathit{xs}, \mathit{ys} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\mathbb{N}}}}$ :

\htmlData{mx=8}{\operatorname{sum}\left(\htmlData{mx=7}{\htmlData{mx=4}{\mathit{xs}} + \htmlData{mx=6}{\mathtt{+}(\htmlData{mx=5}{\mathit{ys}})}}\right)} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=11}{\operatorname{sum}\left(\htmlData{mx=10}{\mathit{xs}}\right)} + \htmlData{mx=14}{\operatorname{sum}\left(\htmlData{mx=13}{\mathit{ys}}\right)}}

What the notation means · or point at any symbol

List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
f(x)Function application: List applied to Nat. Lean writes f x; papers write f(x). (List Nat)
x ∈ TVariables: xs, ys range over List Nat: the statement must hold for every choice. ((xs ys : List Nat))
e.fsum: sum of xs + +(ys): Lean's dot notation e.sum means sum applied to e. ((xs ++ ys).sum)
=Equality: sum(xs + +(ys)) and xs.sum + ys.sum are the same. ((xs ++ ys).sum = xs.sum + ys.sum)
+Addition: xs plus +(ys). (xs ++ ys)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)

theorem nlightning-route-cost-append (xs ys : List Nat) :
    (xs ++ ys).sum = xs.sum + ys.sum

Abstract list-sum model of additive route segment cost.

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