Provednlightninglightningpr-14deep-formalization

Reversing every accounting posting negates the aggregate

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

\htmlData{mx=14}{\operatorname{sum}\left(\htmlData{mx=13}{\htmlData{mx=9}{\operatorname{map}\left(\htmlData{mx=8}{\mathit{xs}}\right)}(\htmlData{mx=12}{x \mapsto \htmlData{mx=11}{-\htmlData{mx=10}{x}}})}\right)} \mathrel{\htmlData{mx=19}{=}} \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 Int. Lean writes f x; papers write f(x). (List Int)
e.fsum: sum of map(x ↦ −x): Lean's dot notation e.sum means sum applied to e. ((xs.map (fun x => -x)).sum)
=Equality: sum(map(x ↦ −x)) and −xs.sum are the same. ((xs.map (fun x => -x)).sum = -xs.sum)
e.fmap: map of xs: Lean's dot notation e.map means map applied to e. (xs.map)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (Int)
x ↦ f(x)Function (λ-abstraction): The function sending x to −x. Lean writes fun x => …; papers write x ↦ …. (fun x => -x)
−xNegation: The negative of x. (-x)

theorem nlightning-reversed-postings-negate-total (xs : List Int) :
    (xs.map (fun x => -x)).sum = -xs.sum

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

Reversing every accounting posting negates the aggregate

How it was proved

More proved statements