InverseMetric
plain-language theorem explainer
The InverseMetric structure encodes the contravariant metric tensor g^{μν} as a symmetric real-valued function on pairs of spacetime indices in four dimensions. It is referenced when constructing Christoffel symbols from the metric and when varying the Einstein-Hilbert action. The declaration is a direct structure with a component map and a symmetry condition, requiring no additional proof steps.
Claim. An inverse metric consists of a map $g^{μν} : Fin 4 → Fin 4 → ℝ$ together with a proof that $g^{μν} = g^{νμ}$ for all indices $μ, ν$.
background
The Gravity.Connection module develops the Levi-Civita connection in local coordinates on four-dimensional spacetime, bypassing the absence of manifold connections in Mathlib. Idx is the abbreviation for Fin 4, indexing the spacetime coordinates. The upstream Minkowski metric eta from Relativity.Geometry.Metric supplies the flat-space case, defined componentwise as diag(-1, +1, +1, +1).
proof idea
The declaration is a pure structure definition introducing the fields ginv for the components and symmetric for the symmetry property. No tactics or lemmas are applied; it serves as a type for subsequent constructions such as christoffel_from_metric.
why it matters
InverseMetric feeds directly into christoffel_from_metric, which builds the connection coefficients, and into ConnectionCert for verifying torsion-freeness. It underpins the Hilbert variation holds theorem in EinsteinHilbertAction by providing the inverse metric for the action variation. Within Recognition Science, this supports the gravity sector computations leading to the Einstein equations, consistent with the eight-tick octave and D = 3 spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.