Provedcommons

Spacelike basis vectors square to −1

For all $\htmlData{mx=2}{i \in \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Fin}}\,3}}$ :

\htmlData{mx=10}{\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{gamma}}(\htmlData{mx=3}{\operatorname{succ}\left(\htmlData{mx=2}{i}\right)})} \cdot \htmlData{mx=9}{\htmlData{mx=5}{\operatorname{gamma}}(\htmlData{mx=8}{\operatorname{succ}\left(\htmlData{mx=7}{i}\right)})}} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{-1}

What the notation means · or point at any symbol

Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application: Fin applied to 3. Lean writes f x; papers write f(x). (Fin 3)
gamma: Commons.gamma: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.gamma)
·Multiplication: gamma(i.succ) times gamma(i.succ). (Commons.gamma i.succ * Commons.gamma i.…)
=Equality: gamma(i.succ) · gamma(i.succ) and −1 are the same. (Commons.gamma i.succ * Commons.gamma i.…)
e.fsucc: succ of i: Lean's dot notation e.succ means succ applied to e. (i.succ)
−xNegation: The negative of 1. (-1)

theorem gamma-spacelike-squares-to-minus-one (i : Fin 3) :
    Commons.gamma i.succ * Commons.gamma i.succ = -1

From our commons: Commons.gamma_mul_self_succ in the Commons.Physics.SpacetimeAlgebra definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 9 lines of Lean