Tmn
plain-language theorem explainer
Defines the comoving perfect-fluid stress-energy tensor on flat FRW in component form: energy density on the time-time slot, pressure times a squared on spatial diagonals, zeros off-diagonal. Cosmologists deriving Friedmann I/II from Einstein equations on this background cite it as the matter side. The body is a three-branch piecewise definition matching T_{μν}=(ρ+p)u_μ u_ν+p g_{μν} with u=∂_t.
Claim. For scale factor $a$, energy density $\rho$, and pressure $p$ (functions of cosmic time), the stress-energy components $T_{\mu\nu}(t)$ on the flat FRW background are $T_{00}=\rho(t)$, $T_{ii}=p(t)\,a(t)^2$ for spatial indices $i$, and $T_{\mu\nu}=0$ when $\mu\neq\nu$. Equivalently $T_{\mu\nu}=(\rho+p)u_\mu u_\nu+p g_{\mu\nu}$ with four-velocity $u=\partial_t$ in signature $(-,+,+,+)$.
background
The module builds Friedmann equations from componentwise flat FRW geometry (Target C skeleton). Layer 1 is pure geometry: metric, Christoffels, Ricci, Einstein tensor as finite Fin-4 sums of time derivatives. Layer 2 feeds a named Einstein-equation premise plus a comoving perfect fluid, so Friedmann I and II become theorems rather than bare Props.
Conventions: signature $(-,+,+,+)$, $c=1$, spatial curvature $k=0$, coupling $\kappa=8\pi G$. The metric is diagonal with $g_{00}=-1$ and spatial entries $a(t)^2$. For a perfect fluid at rest in comoving coordinates, the only nonzero stress-energy pieces are energy density on the time-time component and isotropic pressure on the spatial diagonals, scaled by the metric factor $a^2$.
Upstream constants supply the RS-native $G$ used later in $\kappa$, but this definition itself is classical GR kinematics of $T_{\mu\nu}$; it does not invoke the J-cost or forcing chain.
proof idea
Definition, not a proof. The body is a pure piecewise function of the index pair $(\mu,\nu)\in\mathrm{Fin},4$: if both indices are the time slot then return $\rho(t)$; else if the indices are equal (spatial diagonal) return $p(t),a(t)^2$; else return $0$. No lemmas are applied. Downstream proofs simply simp this definition when specializing Einstein equations to the $00$ or $ii$ components.
why it matters
This is the matter input for the module's Layer-2 field equations. The named premise EinsteinEqns equates the geometric Einstein tensor componentwise to $\kappa$ times these $T_{\mu\nu}$ values. From that premise, friedmann_I extracts $(\dot a/a)^2=\kappa\rho/3$ via the $00$ slot, and friedmann_II extracts $\ddot a/a=-\kappa(\rho+3p)/6$ from the spatial diagonals together with the $00$ relation.
In the Recognition Science cosmo chain this upgrades earlier bare Friedmann Props to derived consequences of Einstein equations on FRW. The Einstein equations themselves remain an honest MODEL premise until forced upstream; the stress-energy shape is the standard perfect-fluid ansatz that makes that derivation classical and checkable. No T0–T8 landmark is claimed here: the declaration is GR scaffolding inside the relativity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.