friedmann_II
plain-language theorem explainer
The second Friedmann equation (acceleration) follows from the Einstein equations on flat FRW: ä/a = −κ(ρ + 3p)/6 for any positive C² scale factor. Cosmologists and GR formalizers cite it when deriving expansion dynamics from the field equations rather than postulating them. The proof combines the 00 and 11 Einstein components, cancels a² via positivity of a, and rearranges.
Claim. Let $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 stress-energy, then at every $t$, $$\frac{\ddot a(t)}{a(t)}=-\frac{\kappa}{6}\bigl(\rho(t)+3p(t)\bigr).$$
background
This module derives the classical Friedmann equations as theorems from componentwise FRW geometry plus a named Einstein-equation premise, rather than taking them as bare definitions. Layer 1 builds the flat FRW metric in a Fin-4 encoding, Christoffel symbols, Ricci tensor/scalar, and Einstein tensor as finite sums of time derivatives. Layer 2 imports EinsteinEqns: for all indices μ,ν and times t, the Einstein tensor equals κ times the perfect-fluid stress-energy, with κ = 8πG.
Conventions are signature (−,+,+,+), c = 1, spatial curvature k = 0. Standard intermediate identities already in scope include G₀₀ = 3(ȧ/a)² and Gᵢᵢ = −(2a ä + ȧ²). Friedmann I is the companion (ȧ/a)² = κρ/3; this declaration is Friedmann II, the acceleration equation.
The premise EinsteinEqns is an honest MODEL import until the field equations are forced upstream in the Recognition chain. The result upgrades earlier bare Prop stubs to derived consequences on any positive C² scale factor.
proof idea
Specialize the Einstein equations at (0,0) and (1,1). Rewrite the 00-component via the already-proved Einstein-tensor identity for G₀₀, simplify the stress-energy, and clear denominators with field_simp/linarith to obtain 3 ȧ² = κ ρ a².
Do the same for the 11-component: G₁₁ gives −(2a ä + ȧ²) = κ p a² after simplification. Combine the two algebraic relations by nlinarith to produce 2a ä = −κ p a² − ȧ², substitute ȧ² from the 00-equation, and rearrange to ä · a = (−κ/6)(ρ + 3p) a².
Cancel the nonzero factor a(t) (from positivity) by mul_right_cancel₀, then divide by a to reach ä/a = −κ(ρ + 3p)/6.
why it matters
This is one half of the classical Friedmann pair that governs cosmic expansion and acceleration. Downstream, friedmannCert bundles it with Friedmann I: from the named EinsteinEqns premise, both equations hold for every positive C² scale factor. That certificate is the clean export surface for the cosmology chain.
In the Recognition Science stack this sits in the relativity/cosmology layer that consumes GR as a model premise until the Einstein equations themselves are forced upstream. It does not yet touch T5–T8 (J-uniqueness, φ, eight-tick, D = 3) or the mass ladder; those enter when RS-native sources replace the perfect-fluid (ρ, p). The module status note records that geometry components were unlocked by the FRWComponentsProbe; this theorem closes the field-equation half of Target C for the acceleration equation.
Anyone auditing whether Friedmann dynamics are definitions or theorems in the mirror should land here: they are theorems modulo EinsteinEqns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.