minkowski_inverse
plain-language theorem explainer
Explicit components of the inverse Minkowski metric are supplied by this definition as g^{μν} = diag(-1, +1, +1, +1) inside the InverseMetric structure. Researchers verifying vacuum solutions or the vanishing of Christoffel symbols in coordinate-based general relativity within the Recognition Science framework cite it. The implementation directly encodes the diagonal form and verifies symmetry via case analysis and simplification.
Claim. The inverse metric tensor satisfies $g^{μν} = diag(-1, +1, +1, +1)$ with the symmetry property $g^{μν} = g^{νμ}$ for all indices μ, ν.
background
The module formalizes the Levi-Civita connection in local coordinate patches, where the metric is a smooth map from R^4 to 4×4 matrices. The InverseMetric structure encodes the inverse metric g^{μν} satisfying g^{μρ} g_{ρν} = δ^μ_ν. The Minkowski metric is the flat metric η_{μν} = diag(-1, +1, +1, +1), whose inverse coincides with itself under the mostly-plus signature.
proof idea
This is a direct definition of the InverseMetric structure. The ginv field is assigned the explicit diagonal function returning -1 on the time index and +1 on spatial indices. Symmetry is established by a tactic performing case splits on the indices followed by simplification using equality commutation.
why it matters
This definition supplies the concrete flat metric instance required by downstream certificates such as ConnectionCert and flat_christoffel_vanish, which establish that the Minkowski metric is a vacuum solution to the Einstein field equations. It anchors the coordinate treatment of gravity in the Recognition Science framework, where flat spacetime serves as the base case for curvature vanishing and connection compatibility. The construction aligns with the eight-tick octave by separating the time component in the signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.