friedmann_I
plain-language theorem explainer
The first Friedmann equation follows from the Einstein field equations on flat FRW: the squared Hubble rate equals κ times energy density over three. Cosmologists and GR formalizers cite it when expansion dynamics are derived from the field equations rather than postulated. The proof specializes the (0,0) Einstein component, rewrites via the precomputed G₀₀ identity, simplifies the perfect-fluid stress-energy, and closes by linear arithmetic.
Claim. Let $a,\rho,p:\mathbb{R}\to\mathbb{R}$ and $\kappa\in\mathbb{R}$. If $a$ is $C^2$, strictly positive, and the Einstein equations $G_{\mu\nu}=\kappa T_{\mu\nu}$ hold componentwise for a comoving perfect fluid on flat FRW, then for every $t$, $\bigl(\dot a(t)/a(t)\bigr)^2=(\kappa/3)\,\rho(t)$.
background
This module derives the Friedmann equations as theorems from componentwise FRW geometry plus a named Einstein-equations premise, rather than taking them as bare definitions. Layer 1 builds the flat FRW metric in a Fin-4 encoding, then Christoffel symbols, Ricci tensor/scalar, and Einstein tensor as finite sums of time derivatives (convergence-free differential algebra). Layer 2 imports the field equations as a model premise together with a comoving perfect fluid.
Conventions: signature (−,+,+,+), $c=1$, spatial curvature $k=0$, $\kappa=8\pi G$. Classical identities on this background include $G_{00}=3(\dot a/a)^2$ and perfect-fluid $T_{00}=\rho$. The named hypothesis asserts $G_{\mu\nu}(t)=\kappa T_{\mu\nu}(t)$ at every component and time. The upstream identity for the Einstein-tensor $(0,0)$ entry supplies the explicit reduction used here.
proof idea
Specialize the Einstein-equations hypothesis to the $(0,0)$ slot at time $t$. Rewrite that equality with the precomputed $(0,0)$ Einstein-tensor identity, which under $C^2$ and positivity of the scale factor equals $3(\dot a/a)^2$. Simplify the stress-energy side by the perfect-fluid definition ($T_{00}=\rho$). The resulting relation $3(\dot a/a)^2=\kappa\rho$ rearranges by linear arithmetic to the claimed form. Four short tactic steps; no induction or analysis beyond the already-proved component identity.
why it matters
First half of the upgrade from bare Prop definitions of Friedmann I/II to derived consequences of Einstein on FRW (Target C skeleton, cosmo-chain panel). It feeds the certificate that bundles both Friedmann equations: from the named Einstein-equations premise, both hold on any positive $C^2$ scale factor. In the Recognition Science stack the Einstein equations remain an honest model import until forced from the ledger/forcing chain (T0–T8); this lemma isolates that dependency so cosmology can proceed once the GR input is discharged. Pure classical GR content; no RS mass ladder, eight-tick octave, or alpha band enters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.