IndisputableMonolith.Relativity.Cosmology.FRWFriedmann
Defines the flat FRW metric on the cosmological sector: diagonal components $g_{00}=-1$ and $g_{ii}=a(t)^2$, plus inverse, partials, Ricci, Einstein tensor, and perfect-fluid stress-energy. Cosmologists in the RS relativity stack cite it for Friedmann equation setup. The module is largely definitional component lemmas over Mathlib calculus.
claimOn a flat FRW background the metric is diagonal with $g_{00}=-1$ and $g_{ii}=a(t)^2$ (no sum), with inverse $g^{\mu\nu}$, Ricci and Einstein tensors, and a perfect-fluid $T_{\mu\nu}$ assembled so that the Einstein equations reduce to the Friedmann system for the scale factor $a(t)$.
background
Flat FRW cosmology is the homogeneous isotropic sector of GR: a single scale factor $a(t)$ multiplies the spatial metric while the time-time component stays Minkowski-normalized. The module works in coordinate components rather than abstract index calculus.
Sibling definitions introduce the metric gMetric, its inverse, coordinate partials, the Ricci tensor and scalar, the Einstein tensor, a perfect-fluid stress-energy Tmn, and the Einstein equation bundle. Auxiliary facts record $g_{00}$, spatial diagonals, vanishing off-diagonals, and the derivative of $a^2$.
The local setting is classical GR cosmology inside the RS relativity layer; only Mathlib is imported, so curvature identities are written out by hand at the component level.
proof idea
This is a definition module, not a theorem chain. Metric and inverse are declared componentwise; curvature and Einstein tensors are built from those components; short lemmas discharge the diagonal pattern ($g_{00}=-1$, spatial $a(t)^2$, off-diagonal zeros) and the product rule for $\partial_t(a^2)$. No deep forcing or Recognition-Composition steps appear here.
why it matters in Recognition Science
Supplies the geometric substrate for Friedmann dynamics in the RS relativity/cosmology stack. Downstream work that reduces Einstein equations to $\dot a$ and $\ddot a$ relations, or that matches RS mass-ladder or eight-tick timing onto an expanding background, needs these component definitions. It does not itself invoke T5–T8 or the J-cost; it is the classical GR side that later RS cosmology must interface with.
scope and limits
- Does not treat curved FRW ($k=\pm 1$) or anisotropic Bianchi metrics.
- Does not derive Friedmann ODEs as named theorems beyond component setup.
- Does not couple to RS J-cost, phi-ladder masses, or eight-tick discrete time.
- Does not prove existence/uniqueness of $a(t)$ for given equations of state.
- Does not include perturbation theory or CMB observables.
declarations in this module (33)
-
def
gMetric -
def
gInv -
def
pd -
def
RicciT -
def
RicciScalarT -
def
EinsteinT -
def
Tmn -
def
EinsteinEqns -
lemma
deriv_a_sq -
lemma
gMetric_00 -
lemma
gMetric_spatial -
lemma
gMetric_offdiag -
lemma
christoffel_0_00 -
theorem
christoffel_0_11 -
theorem
christoffel_0_22 -
theorem
christoffel_0_33 -
theorem
christoffel_1_01 -
theorem
christoffel_2_02 -
theorem
christoffel_3_03 -
theorem
christoffel_symm -
theorem
deriv_hubble -
theorem
deriv_a_adot -
theorem
ricci_00 -
lemma
christoffel_1_10 -
theorem
ricci_11 -
lemma
ricci_22 -
lemma
ricci_33 -
theorem
ricci_scalar_eq -
theorem
einstein_00 -
theorem
einstein_11 -
theorem
friedmann_I -
theorem
friedmann_II -
theorem
friedmannCert