Provednlightninglightningpr-14formal-invariant

Canonical record sorting preserves aggregate value

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

\htmlData{mx=14}{\operatorname{sum}\left(\htmlData{mx=13}{\htmlData{mx=9}{\operatorname{mergeSort}\left(\htmlData{mx=8}{\mathit{xs}}\right)}(\htmlData{mx=10}{\cdot} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\cdot})}\right)} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\operatorname{sum}\left(\htmlData{mx=16}{\mathit{xs}}\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)
e.fsum: sum of mergeSort(· ≤ ·): Lean's dot notation e.sum means sum applied to e. ((xs.mergeSort (· ≤ ·)).sum)
=Equality: sum(mergeSort(· ≤ ·)) and xs.sum are the same. ((xs.mergeSort (· ≤ ·)).sum = xs.sum)
e.fmergeSort: mergeSort of xs: Lean's dot notation e.mergeSort means mergeSort applied to e. (xs.mergeSort)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
·Placeholder: Stands for the argument of an anonymous function: f (·) means x ↦ f x. (·)
≤At most: · is less than or equal to ·. (· ≤ ·)

theorem nlightning-canonical-order-preserves-total (xs : List Nat) :
    (xs.mergeSort (· ≤ ·)).sum = xs.sum

Abstract merge-sort/sum invariant for canonical record ordering.

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