gMetric_spatial
plain-language theorem explainer
For the flat FRW metric in the Fin-4 component encoding, every spatial diagonal entry equals the squared scale factor as a function of time. Cosmologists and GR formalizers cite it when reducing Christoffel, Ricci, and Einstein components. The proof is a one-line function-extensionality plus simp on the piecewise definition of the metric.
Claim. Let $a:\mathbb{R}\to\mathbb{R}$ be a scale factor and let $i\in\{0,1,2,3\}$ with $i\neq 0$. Then the diagonal metric component satisfies $g_{ii}(t)=a(t)^2$ for all $t$.
background
The module builds Friedmann I and II as theorems from componentwise flat FRW geometry plus the Einstein equations, rather than as bare Props. Conventions are signature $(-+++)$, $c=1$, spatial curvature $k=0$, and $\kappa=8\pi G$.
The metric is encoded as a map on Fin 4 indices: diagonal with $g_{00}=-1$ and $g_{ii}=a(t)^2$ for spatial $i$, and zero off-diagonal. The same definition appears in the tractability probe FRWComponentsProbe, which unlocked this two-layer derivation.
This lemma isolates the spatial diagonal case. Sibling facts cover $g_{00}=-1$ and vanishing off-diagonals; together they feed Christoffel symbols such as $\Gamma^0_{ii}=a\dot a$ and the Ricci/Einstein reductions listed in the module header.
proof idea
Term-mode proof by function extensionality on $t$, then simp against the definition of the metric and the hypothesis $i\neq 0$. The piecewise if collapses to $(a,t)^2$ on the spatial diagonal. No external lemmas beyond the local metric definition.
why it matters
Layer-1 geometry needs every metric component in closed form before Christoffel, Ricci, and Einstein tensors can be computed as finite Fin 4 sums. This simp lemma discharges the spatial diagonal case used throughout those reductions.
It sits beside gMetric_00 and gMetric_offdiag and supports the classical targets $R_{ii}=a\ddot a+2\dot a^2$, $G_{ii}=-(2a\ddot a+\dot a^2)$, and ultimately Friedmann I/II as consequences of EinsteinEqns on a comoving perfect fluid. In the Recognition stack this is classical GR scaffolding inside the relativity domain, not a forcing-chain (T0–T8) step; it upgrades bare Friedmann Props to derived theorems once the Einstein premise is in place.
The probe file carries an identical lemma; the Friedmann module re-states it against its own local metric def so the cosmo-formalize loop can grind component identities in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.