inverse_minkowski_apply
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.