einstein_00
plain-language theorem explainer
The (0,0) Einstein-tensor component on flat FRW equals three times the squared Hubble rate: G_{00}=3(ȧ/a)^2. Anyone deriving Friedmann I from the Einstein equations on FRW cites this geometric identity. The proof unfolds G_{μν}=R_{μν}-½g_{μν}R, substitutes the proved R_{00} and scalar-curvature formulae, then finishes by field simplification and ring algebra (ä terms cancel).
Claim. Let $a:\mathbb{R}\to\mathbb{R}$ be twice continuously differentiable and strictly positive. At every time $t$, the Einstein tensor of the flat FRW metric satisfies $G_{00}(t)=3\bigl(\dot{a}(t)/a(t)\bigr)^2$.
background
The module builds Friedmann I and II as theorems from componentwise FRW geometry (Target C skeleton), not as bare definitions. Layer 1 encodes the flat FRW metric in Fin 4 with signature (−,+,+,+), c=1, and spatial curvature k=0: g_{00}=−1 and g_{ii}=a(t)^2 on the diagonal. Christoffel symbols yield Ricci components and the Ricci scalar by finite sums of time derivatives; the Einstein tensor is then defined by G_{μν}=R_{μν}−½ g_{μν} R.
Two upstream identities feed the (0,0) slot: R_{00}=−3ä/a and R=6(ä/a+(ȧ/a)^2). Only the metric factor g_{00}=−1 enters. Twice continuous differentiability of a supplies the second derivatives curvature needs; strict positivity keeps every division by a well-defined.
proof idea
Record a(t)≠0 from positivity. Unfold G_{00}=R_{00}−½ g_{00} R. Rewrite R_{00} and R by the upstream lemmas ricci_00 and ricci_scalar_eq. Simplify g_{00}=−1. field_simp clears denominators; ring finishes. Explicitly the ä pieces cancel: −3ä/a −½(−1)·6(ä/a+(ȧ/a)^2)=−3ä/a+3ä/a+3(ȧ/a)^2.
why it matters
This is the pure-geometry half of Friedmann I. Downstream, friedmann_I rewrites the Einstein equation G_{00}=κ T_{00} via this identity and T_{00}=ρ, obtaining (ȧ/a)^2=κρ/3. friedmann_II likewise opens from the cleared 00-equation. The module thereby upgrades earlier bare Prop definitions of Friedmann I/II to derived consequences of a named EinsteinEqns premise on FRW (Layer 2 still treats the Einstein equations as a model input until forced upstream). In the Recognition stack this is classical GR formalization inside the relativity/cosmology chain, not a T0–T8 forcing step; it sits under the continuum geometry that the discrete recognition ledger must eventually match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.