einstein_11
plain-language theorem explainer
On flat FRW, the spatial Einstein-tensor component equals $G_{11}=-(2a\ddot a+\dot a^2)$. Anyone deriving the acceleration (Friedmann II) equation from the Einstein equations on FRW cites this identity. The proof substitutes the precomputed Ricci $11$ component and Ricci scalar, inserts the spatial metric factor $a^2$, and finishes by field simplification and ring.
Claim. Let $a:\mathbb{R}\to\mathbb{R}$ be twice continuously differentiable with $a(t)>0$ for every $t$. Then the Einstein tensor of the flat FRW metric satisfies $G_{11}(t)=-(2a(t)\,\ddot a(t)+\dot a(t)^2)$.
background
This module carries out a two-layer derivation of the Friedmann equations from componentwise flat FRW geometry. Layer 1 builds the metric, Christoffels, Ricci tensor, Ricci scalar, and Einstein tensor as finite Fin 4 sums of time derivatives (convergence-free differential algebra). Conventions are signature $(-,+,+,+)$, $c=1$, spatial curvature $k=0$, and $\kappa=8\pi G$.
The Einstein tensor is defined pointwise by $G_{\mu\nu}=R_{\mu\nu}-\tfrac12 g_{\mu\nu}R$. For the FRW line element the spatial diagonal metric entries are $g_{ii}=a(t)^2$. Classical GR lists $R_{ii}=a\ddot a+2\dot a^2$, $R=6(\ddot a/a+(\dot a/a)^2)$, and therefore $G_{ii}=-(2a\ddot a+\dot a^2)$; this theorem is that last identity, stated for the $11$ slot.
Layer 2 treats the Einstein equations as a named model premise (not yet forced upstream) together with a comoving perfect fluid, so that Friedmann I and II become theorems rather than bare definitions.
proof idea
Positivity of $a(t)$ gives $a(t)\neq 0$. Unfold the Einstein-tensor definition $G_{\mu\nu}=R_{\mu\nu}-\tfrac12 g_{\mu\nu}R$. Rewrite the two geometric inputs via the already-proved identities for the Ricci $11$ component and the Ricci scalar. Simplify the metric factor on the spatial diagonal ($g_{11}=a^2$). field_simp clears denominators; ring reduces the remaining polynomial identity to $-(2a\ddot a+\dot a^2)$.
why it matters
The sole downstream consumer is friedmann_II, which obtains the acceleration equation $\ddot a/a=-\kappa(\rho+3p)/6$ from the Einstein equations on FRW. That proof reads the $00$ Einstein equation for the density constraint and this $11$ component (together with the perfect-fluid stress-energy) for the pressure combination; without the closed form of $G_{11}$, Friedmann II would remain a definition rather than a derived consequence.
In the module's Target C skeleton this is one of the standard classical GR component identities being formalized so the cosmo-chain can treat Friedmann I/II as theorems. It does not touch the Recognition forcing chain (T0–T8) or the RCL; those sit upstream of whether the Einstein equations themselves are forced. The honest residual is that EinsteinEqns is still a model premise until that forcing is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.