Gravity Connection Inverse Metric

The inverse metric

In general relativity, the metric tensor g_μν encodes the geometry of spacetime: it tells you how to measure distances and angles at each point. Its inverse, written g^μν, is the matrix inverse of the metric, satisfying g^μρg_ρν = δ^μ_ν (the Kronecker delta). This inverse is not a luxury; it is the workhorse of tensor calculus. It raises indices, converting a covariant vector (like a gradient) into a contravariant one (like a velocity), and it appears in every contraction, including the definition of the Christoffel symbols and the Einstein field equations themselves.

The Recognition Science framework's machine-checked library of formal theorems formalizes this object in a coordinate patch. Its InverseMetric declaration establishes that the inverse metric is a symmetric, real-valued function of two indices, just as the metric itself is. The library also proves a key property: the Christoffel symbols, built from the inverse metric and the metric's derivatives, are symmetric in their lower two indices, which corresponds to the connection being torsion-free. It further proves that for flat Minkowski spacetime, where the metric components are constant, all Christoffel symbols vanish identically. These are the local, coordinate-patch facts that underpin the standard computations of general relativity.

What the declaration does not claim is just as important. It does not assert the existence of a global inverse metric on a curved manifold; it works in a local patch where the metric is a smooth matrix-valued function. It does not prove the Levi-Civita connection is unique, nor does it establish metric compatibility as a theorem; that property is stated as a definition, a condition one chooses to impose. The library formalizes the algebraic and differential machinery, but it does not derive the Einstein field equations or any dynamical content. Those remain targets for future formalization, not results of this declaration.

/-- The inverse metric g^{mu nu} (satisfying g^{mu rho} g_{rho nu} = delta^mu_nu). -/
structure InverseMetric where
  ginv : Idx → Idx → ℝ
  symmetric : ∀ mu nu, ginv mu nu = ginv nu mu

/-- Christoffel symbols are symmetric in the lower two indices (torsion-free).
    This follows from the symmetry of the metric derivatives:
    dg mu nu sigma = d_mu g_{nu sigma} is symmetric in (nu, sigma) because
    g_{nu sigma} = g_{sigma nu}. -/
theorem christoffel_symmetric (ginv : InverseMetric)
    (dg : Idx → Idx → Idx → ℝ)
    (dg_metric_sym : ∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) :
    ∀ rho mu nu,
      (christoffel_from_metric ginv dg).gamma rho mu nu =
      (christoffel_from_metric ginv dg).gamma rho nu mu := by
  intro rho mu nu
  simp only [christoffel_from_metric]
  congr 1
  apply Finset.sum_congr rfl
  intro sigma _
  congr 1
  rw [dg_metric_sym mu nu sigma, dg_metric_sym nu mu sigma,
      dg_metric_sym sigma mu nu, dg_metric_sym sigma nu mu]
  ring

/-- For flat spacetime (Minkowski metric with constant components),
    all Christoffel symbols vanish. -/
theorem flat_christoffel_vanish :
    ∀ rho mu nu : Idx,
      (christoffel_from_metric minkowski_inverse (fun _ _ _ => 0)).gamma rho mu nu = 0 := by
  intro rho mu nu
  simp only [christoffel_from_metric, minkowski_inverse]
  norm_num

What this page does not claim

The declaration does not prove the existence of a global inverse metric on a curved manifold. It does not prove the uniqueness of the Levi-Civita connection or metric compatibility as a theorem. It does not derive the Einstein field equations or any dynamical content of general relativity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Connection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: