inverse_metric
This definition supplies the contravariant metric tensor as a bilinear form by inverting the 4x4 matrix of a given covariant MetricTensor at each spacetime point. Researchers computing Christoffel symbols, Ricci scalars, or squared gradients in the Recognition framework would cite it to raise indices on tensors. The body is a direct wrapper that extracts the matrix via metric_to_matrix and applies built-in inversion to the supplied index pair.
claimGiven a symmetric bilinear metric tensor $g$ on spacetime points, the inverse metric $g^{ab}$ is the contravariant bilinear form whose components at each $x$ are obtained by matrix inversion of the $4times4$ representation of $g$.
background
In the Relativity.Geometry.Metric module, MetricTensor is a structure carrying a BilinearForm $g$ together with an explicit symmetry condition that swaps the two lower indices. The sibling definition metric_to_matrix converts this form into an explicit Matrix (Fin 4) (Fin 4) ℝ at each point $x$. ContravariantBilinear is the imported type for objects with two upper indices. The module provides a local, non-sealed interface for 4D spacetime geometry that downstream curvature and Hamiltonian constructions rely on.
proof idea
The definition is a one-line wrapper. It constructs the contravariant bilinear form by feeding the point $x$ and the two upper indices into the matrix inverse of (metric_to_matrix g x), selecting the appropriate entries via (up 0) and (up 1). No lemmas or tactics are invoked beyond the matrix inverse primitive.
why it matters in Recognition Science
This definition supplies the contravariant metric required by christoffel, ricci_scalar, gradient_squared, StressEnergyTensor, and the Hamiltonian density. It therefore sits at the base of the local geometry layer that feeds the Recognition Science forcing chain once relativistic structures are introduced. Without an explicit inverse, index-raising steps in the eight-tick octave and phi-ladder constructions remain blocked.
scope and limits
- Does not prove that the output satisfies the Kronecker-delta contraction identity with the original metric.
- Does not handle singular or degenerate metrics.
- Does not incorporate coordinate transformations or manifold transition functions.
- Does not compute the inverse in a coordinate-free or abstract-index manner.
Lean usage
example (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ := (inverse_metric g) x (fun i => if i.val = 0 then 0 else 1) (fun _ => 0)formal statement (Lean)
67noncomputable def inverse_metric (g : MetricTensor) : ContravariantBilinear :=
proof body
Definition body.
68 fun x up _ =>
69 (metric_to_matrix g x)⁻¹ (up 0) (up 1)
70
71/-- Inverse Minkowski metric components. -/