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

The Minkowski metric on $\mathbb{R}^{1+n}$ as a matrix: $m_{\mu \nu} = \operatorname{diag}(-1, 1, 1, \ldots, 1)$.

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

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

theorem NullFrame.minkowskiInner_comm (n : ℕ) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n X Y = minkowskiInner n Y X

The Minkowski inner product is symmetric: $m(X, Y) = m(Y, X)$.

structure NullFrame.NullFrameData (n : ℕ) : Type

A null frame for $\mathbb{R}^{1+n}$ (Definition 2.2.1): a basis $\{L, \underline{L}, e_{(1)}, \ldots, e_{(n-1)}\}$ where $L$ and $\underline{L}$ are null vectors normalized by $m(L, \underline{L}) = -2$, and the $e_{(i)}$ are $m$-orthonormal vectors that span the $m$-orthogonal complement of $\operatorname{span}(L, \underline{L})$. The completeness field expresses every vector $X$ in null-frame components.

• L : Fin (n + 1) → ℝ
• Lb : Fin (n + 1) → ℝ
• e : Fin (n - 1) → Fin (n + 1) → ℝ
• L_null : minkowskiInner n self.L self.L = 0
• Lb_null : minkowskiInner n self.Lb self.Lb = 0
• L_Lb_inner : minkowskiInner n self.L self.Lb = -2
• e_orthonormal (i j : Fin (n - 1)) : minkowskiInner n (self.e i) (self.e j) = if i = j then 1 else 0
• L_e_orthog (i : Fin (n - 1)) : minkowskiInner n self.L (self.e i) = 0
• Lb_e_orthog (i : Fin (n - 1)) : minkowskiInner n self.Lb (self.e i) = 0
• completeness (X : Fin (n + 1) → ℝ) : X = (-(1 / 2) * minkowskiInner n self.Lb X) • self.L + (-(1 / 2) * minkowskiInner n self.L X) • self.Lb + ∑ i : Fin (n - 1), minkowskiInner n (self.e i) X • self.e i

def NullFrame.angularMetric (n : ℕ) (nf : NullFrameData n) (X Y : Fin (n + 1) → ℝ) : ℝ

The angular (transverse) part $h(X, Y) = \sum_i m(e_{(i)}, X) \, m(e_{(i)}, Y)$ of the Minkowski metric appearing in the null frame decomposition.

theorem NullFrame.nullFrame_decomposition {n : ℕ} (nf : NullFrameData n) (X Y : Fin (n + 1) → ℝ) : minkowskiInner n X Y = -(1 / 2) * minkowskiInner n nf.L X * minkowskiInner n nf.Lb Y - 1 / 2 * minkowskiInner n nf.Lb X * minkowskiInner n nf.L Y + angularMetric n nf X Y

Null frame decomposition of the Minkowski metric (Proposition 2.2.1, applied form): $m(X, Y) = -\tfrac{1}{2} m(L, X) m(\underline{L}, Y) - \tfrac{1}{2} m(\underline{L}, X) m(L, Y)

• h(X, Y)$ for all $X, Y \in \mathbb{R}^{1+n}$.

theorem NullFrame.angularMetric_vanish_L {n : ℕ} (nf : NullFrameData n) (Y : Fin (n + 1) → ℝ) : angularMetric n nf nf.L Y = 0

The angular metric vanishes when one argument is $L$: $h(L, Y) = 0$.

theorem NullFrame.angularMetric_vanish_Lb {n : ℕ} (nf : NullFrameData n) (Y : Fin (n + 1) → ℝ) : angularMetric n nf nf.Lb Y = 0

The angular metric vanishes when one argument is $\underline{L}$: $h(\underline{L}, Y) = 0$.

theorem NullFrame.angularMetric_comm {n : ℕ} (nf : NullFrameData n) (X Y : Fin (n + 1) → ℝ) : angularMetric n nf X Y = angularMetric n nf Y X

The angular metric is symmetric: $h(X, Y) = h(Y, X)$.

theorem NullFrame.angularMetric_vanish_L_right {n : ℕ} (nf : NullFrameData n) (X : Fin (n + 1) → ℝ) : angularMetric n nf X nf.L = 0

The angular metric vanishes when its right argument is $L$: $h(X, L) = 0$.

theorem NullFrame.angularMetric_vanish_Lb_right {n : ℕ} (nf : NullFrameData n) (X : Fin (n + 1) → ℝ) : angularMetric n nf X nf.Lb = 0

The angular metric vanishes when its right argument is $\underline{L}$: $h(X, \underline{L}) = 0$.

theorem NullFrame.angularMetric_on_e {n : ℕ} (nf : NullFrameData n) (i j : Fin (n - 1)) : angularMetric n nf (nf.e i) (nf.e j) = if i = j then 1 else 0

On the orthonormal transverse frame vectors, $h(e_{(i)}, e_{(j)}) = \delta_{ij}$.

theorem NullFrame.angularMetric_nonneg {n : ℕ} (nf : NullFrameData n) (X : Fin (n + 1) → ℝ) : 0 ≤ angularMetric n nf X X

The angular metric is non-negative on the diagonal: $h(X, X) \geq 0$.

theorem NullFrame.angularMetric_pos_def {n : ℕ} (nf : NullFrameData n) (X : Fin (n + 1) → ℝ) (hL : minkowskiInner n nf.L X = 0) (hLb : minkowskiInner n nf.Lb X = 0) (hX : X ≠ 0) : 0 < angularMetric n nf X X

The angular metric is positive-definite on the $m$-orthogonal complement of $\operatorname{span}(L, \underline{L})$: if $m(L, X) = m(\underline{L}, X) = 0$ and $X \neq 0$, then $h(X, X) > 0$.

theorem NullFrame.minkowskiMetric_sq (n : ℕ) : minkowskiMetric n * minkowskiMetric n = 1

The Minkowski metric squares to the identity: $m \cdot m = I$.

theorem NullFrame.minkowskiMetric_inv (n : ℕ) : (minkowskiMetric n)⁻¹ = minkowskiMetric n

The Minkowski metric is its own inverse: $m^{-1} = m$.

theorem NullFrame.minkowskiInner_eta_cancel (n : ℕ) (V W : Fin (n + 1) → ℝ) : minkowskiInner n V ((minkowskiMetric n).mulVec W) = V ⬝ᵥ W

Multiplying the right argument by $m$ converts the Minkowski inner product into the Euclidean dot product: $m(V, m \cdot W) = V \cdot W$.

theorem NullFrame.nullFrame_inverse_decomposition {n : ℕ} (nf : NullFrameData n) (μ ν : Fin (n + 1)) : (minkowskiMetric n)⁻¹ μ ν = -(1 / 2) * nf.L μ * nf.Lb ν - 1 / 2 * nf.Lb μ * nf.L ν + ∑ i : Fin (n - 1), nf.e i μ * nf.e i ν

Null frame decomposition of the inverse Minkowski metric (Proposition 2.2.1, raised-index form): $(m^{-1})^{\mu \nu} = -\tfrac{1}{2} L^{\mu} \underline{L}^{\nu}

• \tfrac{1}{2} \underline{L}^{\mu} L^{\nu} + \sum_i e_{(i)}^{\mu} e_{(i)}^{\nu}$.

theorem NullFrame.nullFrame_decomposition_full {n : ℕ} (nf : NullFrameData n) : (∀ (X Y : Fin (n + 1) → ℝ), minkowskiInner n X Y = -(1 / 2) * minkowskiInner n nf.L X * minkowskiInner n nf.Lb Y - 1 / 2 * minkowskiInner n nf.Lb X * minkowskiInner n nf.L Y + angularMetric n nf X Y) ∧ (∀ (X : Fin (n + 1) → ℝ), minkowskiInner n nf.L X = 0 → minkowskiInner n nf.Lb X = 0 → X ≠ 0 → 0 < angularMetric n nf X X) ∧ (∀ (Y : Fin (n + 1) → ℝ), angularMetric n nf nf.L Y = 0) ∧ (∀ (Y : Fin (n + 1) → ℝ), angularMetric n nf nf.Lb Y = 0) ∧ ∀ (μ ν : Fin (n + 1)), (minkowskiMetric n)⁻¹ μ ν = -(1 / 2) * nf.L μ * nf.Lb ν - 1 / 2 * nf.Lb μ * nf.L ν + ∑ i : Fin (n - 1), nf.e i μ * nf.e i ν

Combined statement of Proposition 2.2.1 (null frame decomposition of $m$): the applied-form decomposition of $m$, positive-definiteness of $h$ on the transverse plane, vanishing of $h$ on $L$ and $\underline{L}$, and the raised-index decomposition of $m^{-1}$.