minkowski_inverse
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that the supplied ginv is the matrix inverse of the Minkowski metric.
- Does not extend to curved metrics or general coordinate transformations.
- Does not compute Christoffel symbols or curvature tensors.
- Does not address global manifold structure beyond local patches.
formal statement (Lean)
54def minkowski_inverse : InverseMetric where
55 ginv := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
proof body
Definition body.
56 symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
57
58/-! ## Christoffel Symbols -/
59
60/-- The Christoffel symbols of the second kind in local coordinates.
61 Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (d_mu g_{nu sigma} + d_nu g_{mu sigma} - d_sigma g_{mu nu})
62
63 We represent these as a function of three indices.
64 The partial derivatives d_mu g_{nu sigma} are provided as input
65 (they depend on the coordinate system and the point). -/