def MinkowskiVectors.minkowskiMetric (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The Minkowski metric on $\mathbb{R}^{1+n}$ in standard coordinates, $m_{\mu\nu} = \mathrm{diag}(-1, 1, \ldots, 1)$.

def MinkowskiVectors.minkowskiInner (n : ℕ) (X Y : Fin (n + 1) → ℝ) : ℝ

The Minkowski inner product $m(X, Y) = m_{\alpha\beta} X^\alpha Y^\beta$ for vectors $X, Y \in \mathbb{R}^{1+n}$.

def MinkowskiVectors.IsTimelike (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is timelike if $m(X, X) < 0$ (Definition 2.0.1).

def MinkowskiVectors.IsSpacelike (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is spacelike if $m(X, X) > 0$ (Definition 2.0.1).

def MinkowskiVectors.IsNull (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X$ is null if $m(X, X) = 0$ (Definition 2.0.1).

def MinkowskiVectors.IsCausal (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector is causal if it is timelike or null (Definition 2.0.1).

def MinkowskiVectors.IsFutureDirected (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is future-directed if its time-component $X^0$ is positive (Definition 2.0.2).

def MinkowskiVectors.IsPastDirected (n : ℕ) (X : Fin (n + 1) → ℝ) : Prop

A vector $X \in \mathbb{R}^{1+n}$ is past-directed if its time-component $X^0$ is negative.

def MinkowskiVectors.IsLorentzTransformation (n : ℕ) (Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) : Prop

A Lorentz transformation is a linear map preserving the Minkowski metric, i.e. $\Lambda^T m \Lambda = m$ (Definition 2.1.1).

theorem MinkowskiVectors.lorentz_preserves_inner {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n (Λ.mulVec X) (Λ.mulVec Y) = minkowskiInner n X Y

A Lorentz transformation preserves the Minkowski inner product: $m(\Lambda X, \Lambda Y) = m(X, Y)$.

theorem MinkowskiVectors.lorentz_preserves_timelike {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsTimelike n X) : IsTimelike n (Λ.mulVec X)

Lorentz transformations preserve the timelike character of a vector (Corollary 2.1.1, timelike case).

theorem MinkowskiVectors.lorentz_preserves_spacelike {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsSpacelike n X) : IsSpacelike n (Λ.mulVec X)

Lorentz transformations preserve the spacelike character of a vector (Corollary 2.1.1, spacelike case).

theorem MinkowskiVectors.lorentz_preserves_null {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsNull n X) : IsNull n (Λ.mulVec X)

Lorentz transformations preserve the null character of a vector (Corollary 2.1.1, null case).

theorem MinkowskiVectors.lorentz_preserves_causal {n : ℕ} {Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} (hΛ : IsLorentzTransformation n Λ) {X : Fin (n + 1) → ℝ} (hX : IsCausal n X) : IsCausal n (Λ.mulVec X)

Lorentz transformations preserve the causal character of a vector.

theorem MinkowskiVectors.lorentz_preserves_causal_character {n : ℕ} (Λ : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) (hΛ : IsLorentzTransformation n Λ) (X : Fin (n + 1) → ℝ) : (IsTimelike n X → IsTimelike n (Λ.mulVec X)) ∧ (IsSpacelike n X → IsSpacelike n (Λ.mulVec X)) ∧ (IsNull n X → IsNull n (Λ.mulVec X))

Corollary 2.1.1 (packaged): a Lorentz transformation preserves each of the three causal classifications — timelike, spacelike, and null.