continuity_from_friedmann
plain-language theorem explainer
The FRW continuity equation a ρ' = −3 a'(ρ+p) is forced by the two Friedmann equations: differentiate I and eliminate a″ via II. Cosmologists deriving adiabatic expansion or neutrino dilution without postulating continuity cite this. The proof is pure calculus with HasDerivAt, then a linear combination that cancels (8πG/3)a² under G≠0 and a(t)≠0.
Claim. Let $a,\rho,p:\mathbb{R}\to\mathbb{R}$ be differentiable as stated, with $G\neq 0$ and $a(t)\neq 0$. If the first Friedmann equation $a'(u)^2=(8\pi G/3)\,\rho(u)\,a(u)^2$ holds for all $u$, and the second $a''\,a(t)=-(4\pi G/3)\,(\rho(t)+3p(t))\,a(t)^2$ holds at time $t$, then the continuity equation $a(t)\,\rho'=-3\,a'(t)\,(\rho(t)+p(t))$ holds at $t$.
background
This module sits in the cosmology layer that discharges model hypotheses previously assumed in neutrino dilution: adiabatic expansion (comoving entropy $s a^3$ conserved) and free-streaming redshift ($a T_\nu$ constant). Both are derived here from FRW dynamics plus equilibrium thermodynamics, with zero sorry.
Section 0 isolates the continuity equation itself. In standard GR it is the Bianchi-identity compatibility of Einstein's equations with a perfect fluid. Here it is stated purely as ODEs on the scale factor and fluid variables: Friedmann I relates $a'^2$ to $\rho a^2$; Friedmann II relates $a'' a$ to $(\rho+3p)a^2$. The gravitational coupling $G$ enters only as a nonzero scalar (RS-native $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ is available but not required beyond $G\neq 0$).
Differentiability is packaged with Mathlib's HasDerivAt, so the argument never divides by $a'$ or assumes $H\neq 0$; only $G\neq 0$ and $a(t)\neq 0$ cancel the common prefactor $(8\pi G/3)a^2$.
proof idea
Differentiate both sides of Friedmann I at time $t$. The left side uses the chain rule on $(a')^2$ via ha'd.fun_pow 2; the right side multiplies the product rule for $\rho\cdot a^2$ by the constant $8\pi G/3$. Uniqueness of derivatives equates $2 a' a''$ to that right-hand derivative.
Substitute Friedmann II for $a''$ through the linear combination $2 a'\cdot(\mathrm{II})-a\cdot(\mathrm{eq})$. The result factors as $(8\pi G/3)a^2\cdot\bigl(a\rho'+3 a'(\rho+p)\bigr)=0$. Nonvanishing of $\pi$, $G$, and $a(t)^2$ kills the prefactor (mul_eq_zero.resolve_left), and linarith finishes the continuity identity. No division by $a'$ appears.
why it matters
Continuity is the first link in the module's derivation chain. Downstream, entropy_conserved_from_friedmann composes this result with the Euler relation $T s=\rho+p$ and Gibbs–Duhem $p'=s T'$ to obtain $d/dt(s a^3)=0$ without assuming continuity as an axiom: "Friedmann I + II plus the equilibrium identities give comoving entropy conservation directly."
That closes the adiabatic-expansion hypothesis that NeutrinoDilution previously took as a model input, so the classic ratios $(T_\nu/T_\gamma)^3=4/11$ and $g_{*s}=43/11$ rest on proved FRW calculus rather than postulates. Sibling results then upgrade pointwise vanishing derivatives to global constancy of $s a^3$ and $a T$ via the mean value theorem, and recover free-streaming redshift for decoupled radiation from continuity alone.
In the broader Recognition framework this is classical GR bookkeeping inside the cosmology layer, not a T0–T8 forcing step; its value is discharging scaffolding so entropy and dilution theorems sit on the same proved base as the rest of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.