gMetric_offdiag
plain-language theorem explainer
Off-diagonal components of the flat FRW metric vanish identically as functions of cosmic time. Anyone simplifying Christoffel symbols or Ricci terms in the Fin-4 FRW encoding cites this. The proof is a one-line unfold of the metric definition under the index inequality, discharged by simp after funext.
Claim. Let $a:\mathbb{R}\to\mathbb{R}$ be a scale factor and let $\mu,\nu\in\{0,1,2,3\}$ with $\mu\neq\nu$. Then the metric component $g_{\mu\nu}(a)$ is the zero function of cosmic time: $g_{\mu\nu}(a)(t)=0$ for all $t$.
background
The module is a standalone tractability probe for flat FRW geometry before locking a 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$ is ordinary differentiation.
The metric is a componentwise map on $\mathrm{Fin},4\times\mathrm{Fin},4$ sending a scale factor $a$ to functions of $t$. Diagonal entries carry the usual $-1$ and $a(t)^2$ structure; off-diagonal slots are defined to be zero. Time is identified with $\mathbb{R}$ in RS-native units.
Probe targets named by the cosmo-chain panel are $\Gamma^0_{ii}=a\dot a$ and $\Gamma^i_{0i}=\dot a/a$. Vanishing off-diagonals are the first algebraic fact those Christoffel computations need.
proof idea
Term-style one-liner: extensionality on the cosmic-time argument, then simp unfolds the metric definition and uses the hypothesis $\mu\neq\nu$ to hit the zero branch. No external lemmas beyond the definition of the metric and the inequality on indices.
why it matters
This is the basic diagonal-support fact for the FRW component probe. Downstream, christoffel_symm in the Friedmann module uses it twice (once for each order of indices) to show $g_{mn}=g_{nm}$ when $m\neq n$, which makes the Christoffel bracket symmetric in the lower indices by definition. The sibling time-derivative lemma for $a^2$ is written in the lambda form that metric simp lemmas produce, so the off-diagonal rule participates in the same simp set.
If the probe closes ($\Gamma^0_{ii}=a\dot a$, $\Gamma^i_{0i}=\dot a/a$), the full skeleton (Ricci, Einstein tensor, Friedmann I/II from a named Einstein-equations proposition) locks as loop targets. The lemma is pure differential algebra on the Fin-4 encoding; it does not itself invoke the Recognition forcing chain, but it is the gate that must open before cosmological Einstein equations can be stated in this codebase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.