Provedcommons

The Minkowski form is v₀² − v₁² − v₂² − v₃²

For all $\htmlData{mx=4}{v : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Fin}}\,4} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{minkowskiForm}}(\htmlData{mx=1}{v})} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{\htmlData{mx=13}{\htmlData{mx=9}{\htmlData{mx=5}{\htmlData{mx=4}{\htmlData{mx=3}{v}(0)}^{2}} - \htmlData{mx=8}{\htmlData{mx=7}{\htmlData{mx=6}{v}(1)}^{2}}} - \htmlData{mx=12}{\htmlData{mx=11}{\htmlData{mx=10}{v}(2)}^{2}}} - \htmlData{mx=16}{\htmlData{mx=15}{\htmlData{mx=14}{v}(3)}^{2}}}

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 4. Lean writes f x; papers write f(x). (Fin 4)
⟹Implies: If Fin(4), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin 4 → ℝ)
minkowskiForm: Commons.minkowskiForm: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.minkowskiForm)
=Equality: minkowskiForm(v) and v(0)^2 − v(1)^2 − v(2)^2 − v(3)^2 are the same. (Commons.minkowskiForm v = v 0 ^ 2 - v 1…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
aᵇPower: v(0) raised to the power 2. (v 0 ^ 2)
-Subtraction: v(0)^2 minus v(1)^2. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (v 0 ^ 2 - v 1 ^ 2)

theorem minkowski-form-formula (v : Fin 4 → ℝ) :
    Commons.minkowskiForm v = v 0 ^ 2 - v 1 ^ 2 - v 2 ^ 2 - v 3 ^ 2

From our commons: Commons.minkowskiForm_apply in the Commons.Physics.Minkowski 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