IndisputableMonolith.Relativity.Cosmology.FRWComponentsProbe
Defines the diagonal components of the flat Friedmann–Robertson–Walker metric in coordinates where the lapse is unity: time–time entry −1 and spatial diagonal entries a(t)². Cosmologists and RS relativity developers cite it when assembling the line element, inverse metric, or scale-factor derivatives. The module is definitional scaffolding over Mathlib, not a proved theorem.
claimOn a flat FRW background the metric is diagonal with $g_{00}=-1$ and $g_{ii}=a(t)^2$ (no sum), with vanishing off-diagonal entries; the module also records the inverse metric and elementary derivatives of $a(t)^2$.
background
Flat FRW spacetime is the homogeneous isotropic cosmology with vanishing spatial curvature. In synchronous gauge the line element is $ds^2=-dt^2+a(t)^2,d\mathbf{x}^2$, so the only nontrivial data are the scale factor $a(t)$ and the signature convention $g_{00}=-1$.
This module packages those components as named Lean objects (metric, inverse, partial derivatives, spatial and off-diagonal projections, and $d/dt,a^2$). It sits in the Relativity.Cosmology layer of the Recognition Science monolith and imports only Mathlib, so it supplies raw geometric ingredients rather than RS-specific forcing results (T0–T8, RCL, or the phi ladder).
proof idea
This is a definition module: it introduces metric component abbreviations and elementary derivative identities. There is no substantive proof obligation beyond whatever trivial equalities Mathlib discharges for diagonal matrices and calculus on $a(t)^2$.
why it matters in Recognition Science
Supplies the concrete $g_{\mu\nu}$ data that any later FRW curvature, geodesic, or stress-energy calculation in the RS relativity stack must quote. Downstream cosmology or gravitational lemmas that expand Christoffel symbols, Einstein tensors, or Hubble-flow identities on a flat background are expected to import these components rather than restate $g_{00}=-1$ and $g_{ii}=a^2$ ad hoc. No parent theorem is wired in the current graph (used_by empty); the module is infrastructure for that layer.
scope and limits
- Does not prove the Einstein equations or Friedmann equations on this background.
- Does not treat curved FRW ($k=\pm 1$) or nonzero shift/lapse.
- Does not derive $a(t)$ from RS forcing, phi-ladder, or matter content.
- Does not define curvature tensors, geodesics, or stress-energy.
- Does not assert physical units or RS-native constants ($c$, $\hbar$, $G$).