gInv
plain-language theorem explainer
Defines the inverse flat FRW metric in signature (−,+,+,+): diagonal entries g^{00}=−1 and g^{ii}=1/a(t)^2, off-diagonal zero. Cosmology and GR formalizations cite it as the raising operator for Christoffel and curvature sums. The body is a pure piecewise definition on Fin 4 indices, no proof obligations.
Claim. For a scale factor $a:\mathbb{R}\to\mathbb{R}$ and spacetime indices $\mu,\nu\in\{0,1,2,3\}$, the inverse metric components are the functions of cosmic time $t$ given by $g^{00}(t)=-1$, $g^{ii}(t)=1/a(t)^2$ (no sum), and $g^{\mu\nu}(t)=0$ whenever $\mu\neq\nu$.
background
This module builds Friedmann I and II as theorems from componentwise flat FRW geometry plus the Einstein equations as a named model premise. Conventions are signature (−,+,+,+), $c=1$, spatial curvature $k=0$, and $\kappa=8\pi G$. Layer 1 is pure differential algebra on Fin 4: metric, inverse metric, Christoffel symbols, Ricci, Einstein tensor.
The covariant metric (sibling) is diagonal with $g_{00}=-1$ and $g_{ii}=a(t)^2$. The inverse defined here is the algebraic dual used to raise indices in the standard formula $\Gamma^\lambda_{\mu\nu}=\tfrac12\sum_\sigma g^{\lambda\sigma}(\partial_\mu g_{\nu\sigma}+\partial_\nu g_{\mu\sigma}-\partial_\sigma g_{\mu\nu})$. Coordinate partials treat $\partial_0$ as $d/dt$ and kill spatial derivatives by homogeneity.
The same inverse-metric definition appears in the tractability probe that unlocked this skeleton; the Friedmann file reuses it so Christoffel and curvature lemmas can simp against a single component table.
proof idea
Definition only: a noncomputable function of cosmic time that branches on whether the Fin 4 indices agree and whether the common index is the time slot. No lemmas are applied; the body is the classical diagonal inverse of flat FRW written as a total function $\mathbb{R}\to\mathbb{R}$ for each index pair.
why it matters
Every Christoffel component in this file unfolds the inverse metric inside the usual half-sum formula. Downstream lemmas such as $\Gamma^0_{00}=0$, $\Gamma^0_{11}=a\dot a$, $\Gamma^0_{22}=a\dot a$, $\Gamma^0_{33}=a\dot a$, and $\Gamma^1_{01}=\dot a/a$ all simp with this definition (together with the metric, partials, and the $d(a^2)/dt=2a\dot a$ identity). Those symbols feed Ricci $R_{00}=-3\ddot a/a$, $R_{ii}=a\ddot a+2\dot a^2$, the scalar $R=6(\ddot a/a+(\dot a/a)^2)$, and Einstein $G_{00}=3(\dot a/a)^2$, from which Friedmann I and II become theorems rather than bare Props.
In the Recognition stack this is classical GR scaffolding inside the relativity domain: it does not invoke the forcing chain (T5–T8), RCL, or the phi-ladder, but it supplies the geometric layer needed before any RS-native cosmology can sit on derived Friedmann equations instead of postulated ones. Status remains a statement-fixed skeleton until the remaining curvature sorries close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.