gMetric
plain-language theorem explainer
Defines the diagonal flat FRW line element in coordinates: time-time entry −1, spatial diagonals a(t)², off-diagonals zero. Cosmologists and GR formalizers cite it as the metric input to Christoffel and Friedmann calculations. 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 metric component functions are $g_{00}(t)=-1$, $g_{ii}(t)=a(t)^2$ for $i=1,2,3$, and $g_{\mu\nu}(t)=0$ whenever $\mu\neq\nu$.
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 metric is the standard homogeneous isotropic line element $ds^2=-dt^2+a(t)^2,d\mathbf{x}^2$, encoded as functions $\mathbb{R}\to\mathbb{R}$ indexed by $\mathrm{Fin},4$. The same definition appears upstream in the Friedmann module; this probe copy exists so simp-friendly lemmas on components can be discharged in isolation.
Downstream partials treat $\partial_0 f=\mathrm{deriv},f$ and spatial $\partial_i=0$, feeding 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})$.
proof idea
Not a proof: a noncomputable definition. For each pair of indices it returns the constant function $-1$ on the time-time slot, the pointwise square of the scale factor on spatial diagonals, and the zero function off the diagonal. No lemmas are applied; later simp lemmas unfold this case split directly.
why it matters
This is the geometric seed of the FRW component probe. Parent results include the simp lemmas that spatial diagonals equal $a^2$ and off-diagonals vanish, the partial-derivative encoding, and the Friedmann-module identities $\Gamma^0_{00}=0$ and $\Gamma^0_{ii}=a\dot a$ (the panel's named first probe targets). Closing those Christoffels is the gate before locking Ricci, Einstein tensor, and Friedmann I/II from a named Einstein-equations proposition. In the broader RS relativity stack it supplies the classical $D=3$ FLRW background against which recognition-scale corrections would later be compared; it does not itself invoke $\phi$, the eight-tick octave, or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.