Provednlightninglightningpr-14formal-invariant

Accounting reversal is an involution

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

\htmlData{mx=10}{\htmlData{mx=0}{\operatorname{map}}(\htmlData{mx=3}{x \mapsto \htmlData{mx=2}{-\htmlData{mx=1}{x}}}, \htmlData{mx=9}{\htmlData{mx=4}{\operatorname{map}}(\htmlData{mx=7}{x \mapsto \htmlData{mx=6}{-\htmlData{mx=5}{x}}}, \htmlData{mx=8}{\mathit{xs}})})} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\mathit{xs}}

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)
map: List.map: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List.map)
=Equality: map(x ↦ −x, map(x ↦ −x, xs)) and xs are the same. (List.map (fun x => -x) (List.map (fun x…)
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-accounting-reversal-involution (xs : List Int) :
    List.map (fun x => -x) (List.map (fun x => -x) xs) = xs

Abstract list model: negate every signed posting twice.

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