gMetric_spatial
plain-language theorem explainer
For any spatial index i (i ≠ 0) the flat FRW diagonal metric component equals the squared scale factor as a function of cosmic time. Cosmologists and GR formalizers cite it when reducing Christoffel or Einstein-tensor components under the Fin-4 encoding. The proof is a one-line funext plus simp on the piecewise definition of gMetric.
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 cosmic time $t$ (equivalently, $g_{ii}=a^2$ as functions).
background
The module is a standalone tractability probe for flat FRW geometry before locking the full two-layer Friedmann skeleton. Encoding: homogeneous flat FRW with $k=0$ and $c=1$; every field depends only on cosmic time $t$, so spatial partials vanish and $\partial_0=\mathrm{deriv}$.
The metric is the diagonal flat-FRW chart on $\mathrm{Fin},4$: $g_{00}=-1$ and $g_{ii}=a(t)^2$ for spatial $i$, with off-diagonals zero. The definition is the piecewise function that returns $-1$ on the time-time slot, $a(t)^2$ on spatial diagonal slots, and $0$ otherwise.
Probe targets named by the cosmo-chain panel are the Christoffel identities $\Gamma^0_{ii}=a\dot a$ and $\Gamma^i_{0i}=\dot a/a$. This lemma is the first simplification step that makes those identities discharge under simp.
proof idea
Term-mode one-liner. Apply functional extensionality in $t$, then simp unfolds the piecewise definition of the metric and uses the hypothesis $i\neq 0$ to select the spatial branch $(a,t)^2$. No auxiliary lemmas are required beyond the definition itself.
why it matters
Closes the spatial-diagonal case of the componentwise FRW metric under the Fin-4 encoding prescribed by the cosmo-chain panel (2026-07-02). Without it, the named first probe $\Gamma^0_{ii}=a\dot a$ cannot simplify. The identical lemma is re-exported in the full FRWFriedmann module, so this probe version is the convergence check that authorizes locking the skeleton (Ricci, Einstein tensor, Friedmann I/II from a named EinsteinEqns Prop). It is pure differential algebra, not a Recognition-forcing step (T0–T8), but it is the geometric substrate on which any later RS cosmology (phi-ladder expansion history, eight-tick cadence in cosmic time) must sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.