minkowski
plain-language theorem explainer
The Minkowski metric is the diagonal bilinear form diag(-1, +1, +1, +1) on four spacetime indices. Researchers verifying vacuum Einstein equations or flat-space limits in coordinate GR cite it as the baseline metric. The definition directly instantiates the MetricTensor structure and confirms symmetry by exhaustive case split on index equality.
Claim. The Minkowski metric tensor satisfies $g_{00}=-1$, $g_{ii}=1$ for $i=1,2,3$, and $g_{mu nu}=0$ for $mu neq nu$, where indices label local spacetime coordinates.
background
MetricTensor is the structure consisting of a map g from pairs of indices to reals together with the axiom that this map is symmetric in its arguments. The module works entirely in local coordinate patches on four-dimensional spacetime to define the Levi-Civita connection, bypassing the absence of abstract manifold connections in Mathlib. Upstream MetricTensor interfaces from the Hamiltonian, Homogenization, and Relativity modules supply the same local bilinear-form abstraction used here.
proof idea
Direct definition that supplies the component function for g and proves the required symmetry field by splitting on whether the indices are equal and simplifying the resulting cases.
why it matters
This definition supplies the flat metric required by HilbertVariationCert, hilbert_variation_flat, einstein_flat, and minkowski_is_vacuum_solution to certify that the vacuum Einstein field equations hold with vanishing curvature and Ricci tensor. It anchors the flat limit inside the Recognition Science gravity formalization and is invoked whenever the eight-tick octave or D=3 spatial dimensions are specialized to Minkowski signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.