EinsteinT
plain-language theorem explainer
Defines the Einstein tensor componentwise on a flat FRW background as G_{μν} = R_{μν} − ½ g_{μν} R, with all objects functions of cosmic time. Cosmologists deriving Friedmann I/II from the field equations cite it as the geometric left-hand side. The body is a direct one-line combination of the already-defined Ricci tensor, metric, and Ricci scalar.
Claim. For a scale factor $a:\mathbb{R}\to\mathbb{R}$ and indices $\mu,\nu\in\{0,1,2,3\}$, the Einstein tensor component is the time-dependent function $G_{\mu\nu}(t)=R_{\mu\nu}(t)-\tfrac12 g_{\mu\nu}(t)\,R(t)$, where $R_{\mu\nu}$ is the Ricci tensor of the flat FRW metric, $g_{\mu\nu}$ its components, and $R$ the Ricci scalar.
background
This module builds Friedmann I and II as theorems from componentwise FRW geometry rather than bare propositions. Layer 1 is pure differential algebra on a flat FRW metric in signature $(-,+,+,+)$ with $c=1$ and $k=0$: metric, Christoffels, Ricci, scalar curvature, then Einstein tensor. All sums are finite over Fin 4, so no convergence issues.
The metric is diagonal with $g_{00}=-1$ and $g_{ii}=a(t)^2$. The Ricci tensor is the standard contraction of Christoffels, $R_{\mu\nu}=\partial_\lambda\Gamma^\lambda_{\mu\nu}-\partial_\nu\Gamma^\lambda_{\mu\lambda}+\Gamma^\lambda_{\lambda\sigma}\Gamma^\sigma_{\mu\nu}-\Gamma^\lambda_{\nu\sigma}\Gamma^\sigma_{\mu\lambda}$. The Ricci scalar is $R=g^{\mu\nu}R_{\mu\nu}$. The Einstein tensor is the usual combination of those three objects.
Classical targets recorded in the module doc include $G_{00}=3(\dot a/a)^2$ and $G_{ii}=-(2a\ddot a+\dot a^2)$, which feed Friedmann I/II once the field equations are imposed.
proof idea
Pure definitional abbreviation: at each $t$, return the Ricci component minus half the metric component times the Ricci scalar. No lemmas, no tactics; it wires RicciT, gMetric, and RicciScalarT into the standard GR formula $G_{\mu\nu}=R_{\mu\nu}-\tfrac12 g_{\mu\nu}R$.
why it matters
This is the geometric left-hand side of the Einstein equations on FRW. Downstream, einstein_00 proves $G_{00}=3(\dot a/a)^2$ and einstein_11 proves $G_{11}=-(2a\ddot a+\dot a^2)$, the two classical identities that become Friedmann I and II once $G_{\mu\nu}=\kappa T_{\mu\nu}$ is assumed.
EinsteinEqns packages that assumption as a named Prop (honest MODEL premise until the field equations are forced upstream): componentwise equality of this tensor to $\kappa$ times the perfect-fluid stress-energy. The module upgrades earlier bare FriedmannI/FriedmannII props to derived consequences of that premise on FRW.
In the Recognition Science cosmo chain this sits in Target C (componentwise FRW geometry). It does not yet touch T0–T8 forcing, the J-cost, or $\phi$-ladder mass formulae; those live upstream of why Einstein gravity itself appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.