gInv
plain-language theorem explainer
Defines the inverse flat-FRW metric components in cosmic time: diagonal with g^{00}=-1 and g^{ii}=1/a(t)^2, off-diagonal zero. Cosmology and GR formalizations cite it as the raised-index partner of the scale-factor metric. 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 indices $\mu,\nu\in\{0,1,2,3\}$, the inverse metric component functions are $g^{\mu\nu}(t)=-1$ if $\mu=\nu=0$, $g^{\mu\nu}(t)=1/a(t)^2$ if $\mu=\nu\in\{1,2,3\}$, and $g^{\mu\nu}(t)=0$ otherwise.
background
The module is a standalone componentwise probe of flat FRW geometry (k=0, c=1) before locking a full two-layer Friedmann skeleton. Every field depends only on cosmic time t, so spatial partials vanish and $\partial_0$ is ordinary differentiation.
The covariant metric is the usual diagonal FRW form $g_{00}=-1$, $g_{ii}=a(t)^2$. Its inverse is the raised-index partner used in the Christoffel formula $\Gamma^\lambda_{\mu\nu}=\frac12\sum_\sigma g^{\lambda\sigma}(\partial_\mu g_{\nu\sigma}+\partial_\nu g_{\mu\sigma}-\partial_\sigma g_{\mu\nu})$. The same definition appears in the sibling FRWFriedmann module; this probe copy keeps the Fin-4 encoding self-contained for simp-driven differential algebra.
proof idea
Pure definition: a noncomputable function of the scale factor and two Fin-4 indices returning a real function of t. On the diagonal it branches on the time index (constant -1) versus spatial indices (1/a(t)^2); off-diagonal entries are identically zero. No lemmas or tactics.
why it matters
Feeds the panel's named first probes $\Gamma^0_{ii}=a\dot a$ and $\Gamma^i_{0i}=\dot a/a$. Downstream, christoffel_0_00, christoffel_0_11, christoffel_0_22, and christoffel_0_33 all simp with this inverse metric (together with pd, gMetric, and Fin.sum_univ_four) to close the $\Gamma^0_{ii}$ identities as function equations. Those closures are the gate before locking Ricci, Einstein tensor, and Friedmann I/II from a named EinsteinEqns Prop. In the broader RS relativity stack this is ordinary GR bookkeeping inside the D=3, c=1 FRW sector, not a new forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.