friedmannCert
plain-language theorem explainer
Both classical Friedmann equations follow from the Einstein field equations on a flat FRW background whenever the scale factor is positive and C². Cosmologists and GR formalizers cite this as the single certificate that the two component theorems hold together. The proof is a one-line pairing of the already-proved Friedmann I and II lemmas under the shared EinsteinEqns hypothesis.
Claim. For all $a,\rho,p:\mathbb{R}\to\mathbb{R}$ and $\kappa\in\mathbb{R}$, if $a$ is $C^2$, $a(t)>0$ for all $t$, and the Einstein equations $G_{\mu\nu}=\kappa T_{\mu\nu}$ hold componentwise on the flat FRW background with perfect fluid $(\rho,p)$, then $\bigl(\dot a/a\bigr)^2=\kappa\rho/3$ and $\ddot a/a=-\kappa(\rho+3p)/6$ at every $t$.
background
The module derives the Friedmann equations from componentwise flat FRW geometry (signature $(-,+,+,+)$, $c=1$, spatial curvature $k=0$, $\kappa=8\pi G$). Layer 1 builds the metric, Christoffels, Ricci, and Einstein tensor as finite Fin-4 differential algebra. Layer 2 feeds a named model premise: the Einstein field equations hold componentwise against a comoving perfect fluid.
That premise is EinsteinEqns: for all $\mu,\nu\in\mathrm{Fin},4$ and times $t$, the Einstein tensor equals $\kappa$ times the stress-energy. The doc states it is "the honest GR import until the field equations are forced upstream." Classical targets include $G_{00}=3(\dot a/a)^2$ and the two Friedmann identities.
Upstream, friedmann_I extracts $(\dot a/a)^2=\kappa\rho/3$ from the $00$ component, and friedmann_II extracts the acceleration equation $\ddot a/a=-\kappa(\rho+3p)/6$. This certificate simply packages both under one hypothesis bundle.
proof idea
Term-mode one-liner. Introduce the scale factor, density, pressure, coupling, the $C^2$ hypothesis, positivity, and the EinsteinEqns premise. Return the pair of universal statements by applying friedmann_I and friedmann_II at each $t$ with those shared hypotheses. No new algebra; pure bundling of the two component theorems.
why it matters
Closes the Layer-2 certificate in the Target C cosmo-chain skeleton: Friedmann I and II become theorems from the Einstein equations on FRW, upgrading the older bare Prop definitions in Relativity.Cosmology.Friedmann. The module doc frames this as the panel-prescribed two-layer derivation unlocked by the FRW components probe.
No downstream consumers are wired yet (used_by is empty), so the declaration is the present top of the FRW-to-Friedmann stack. It keeps the Einstein equations as an explicit model premise rather than a forced RS identity, matching the honest-import stance until field equations are derived upstream in the Recognition forcing chain. Standard GR content only; no direct appeal to T0–T8, $\phi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.