inverse_minkowski_apply
The lemma establishes that the inverse Minkowski metric, when evaluated with index selectors for μ and ν, returns the diagonal Lorentzian components: -1 on the time-time entry and +1 on the spatial diagonals when indices match, zero otherwise. Researchers computing Hamiltonian densities or gradient contractions in flat spacetime within Recognition Science would cite this for explicit metric inversion. The proof is a direct matrix computation that converts the metric to diagonal form, verifies self-inversion, and extracts the entry.
claimFor the Minkowski metric tensor with components $g_{ab} = -1$ if $a=b=0$ and $+1$ if $a=b>0$ (and 0 otherwise), the inverse metric satisfies $g^{ab} = -1$ if $a=b=0$, $+1$ if $a=b>0$, and 0 otherwise.
background
The Minkowski tensor is the flat metric tensor whose bilinear form eta returns -1 when both lowered indices select the time component (index 0) and +1 when they match on a spatial index. The auxiliary metric_to_matrix converts this tensor at a point x into the explicit 4x4 diagonal matrix with entries -1,1,1,1. The inverse_metric accessor is defined as the matrix inverse of that representation applied to the chosen contravariant indices.
proof idea
The proof unfolds inverse_metric to reach the matrix inverse of metric_to_matrix minkowski_tensor x. It first proves by index cases that this matrix equals the diagonal matrix diag(-1,1,1,1). It then applies Matrix.inv_eq_left_inv to show the diagonal matrix equals its own inverse, verifying the product is the identity matrix. Finally it unfolds the diagonal and reads off the value according to whether μ equals ν and whether the common index is 0.
why it matters in Recognition Science
This result is used directly by gradient_squared_minkowski_sum to contract the inverse metric with gradients and obtain the Lorentzian squared norm -(grad 0)^2 + sum of spatial squares. It supplies the concrete inverse required for the Hamiltonian density construction in the Relativity.Geometry module before curved or cosmological metrics are introduced. In the Recognition framework it anchors the flat-space limit consistent with the standard special-relativistic structure.
scope and limits
- Does not treat curved spacetime or position-dependent metrics.
- Does not derive the Minkowski form from the forcing chain or RCL.
- Does not prove uniqueness of the inverse beyond this explicit case.
- Does not handle index raising or lowering operations outside the given selectors.
Lean usage
rw [inverse_minkowski_apply]formal statement (Lean)
72lemma inverse_minkowski_apply (x : Fin 4 → ℝ) (μ ν : Fin 4) :
73 inverse_metric minkowski_tensor x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) =
74 if μ = ν then (if (μ : ℕ) = 0 then -1 else 1) else 0 := by
proof body
Tactic-mode proof.
75 unfold inverse_metric
76 dsimp
77 have h_mat : metric_to_matrix minkowski_tensor x = Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1) := by
78 ext i j
79 unfold metric_to_matrix minkowski_tensor eta
80 dsimp
81 by_cases h : i = j
82 · rw [if_pos h, h]
83 simp
84 · rw [if_neg h]
85 simp [h]
86 rw [h_mat]
87 have h_inv : (Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1))⁻¹ =
88 Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1) := by
89 apply Matrix.inv_eq_left_inv
90 rw [Matrix.diagonal_mul_diagonal]
91 ext i j
92 rw [Matrix.one_apply]
93 unfold Matrix.diagonal
94 dsimp
95 by_cases h : i = j
96 · rw [if_pos h]
97 split_ifs <;> norm_num
98 · rw [if_neg h]
99 simp [h]
100 rw [h_inv]
101 unfold Matrix.diagonal
102 dsimp
103