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 diagonals a(t)². Cosmologists and RS relativity developers cite it when assembling the line element, inverse metric, and scale-factor derivatives. The module is definitional scaffolding over Mathlib, not a theorem pack.
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 identities for $\partial_t(a^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\delta_{ij}dx^i dx^j$, so the only dynamical geometric datum is the scale factor $a(t)>0$.
This module isolates the component functions of that metric and its inverse: $g_{00}=-1$, spatial diagonals $a(t)^2$, and all off-diagonal slots zero. Companion definitions cover partial derivatives and the elementary identity for the time derivative of $a^2$, which feed Christoffel and curvature calculations downstream in the Relativity.Cosmology layer.
The local setting is pure differential-geometry bookkeeping inside Recognition Science’s relativity stack; no forcing-chain or J-cost material appears here.
proof idea
This is a definition module, no proofs. It introduces named component maps (metric, inverse, partials, spatial and off-diagonal projectors, and a derivative identity for $a^2$) as plain Lean definitions over Mathlib, ready for later curvature and Einstein-equation lemmas.
why it matters in Recognition Science
Supplies the concrete $g_{\mu\nu}$ data that any FRW curvature, geodesic, or stress-energy calculation in the RS relativity layer must quote. Parent consumers are not yet wired in the graph (no used_by edges), but the natural landing sites are Friedmann-equation derivations, luminosity-distance integrals, and comparisons of RS-modified expansion histories against the classical $a(t)$ background. Within the broader framework it is infrastructure only: it does not touch T0–T8, the Recognition Composition Law, or the phi-ladder mass formula.
scope and limits
- Does not prove the Einstein equations or Friedmann equations on this background.
- Does not treat curved ($k=\pm 1$) FRW metrics or nonzero shift/lapse.
- Does not define Christoffel symbols, Ricci, or stress-energy tensors.
- Does not assert any Recognition Science forcing or mass-ladder claim.
- Does not normalize units of $a(t)$ or fix an initial condition $a(t_0)$.