pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.Cosmology.FRWMetric

show as:
view Lean formalization →

The FRWMetric module supplies the Friedmann-Robertson-Walker metric, scale factor, Christoffel symbols, and Ricci components for homogeneous isotropic cosmologies in Recognition Science. Researchers working on backreaction cancellation or optical rescaling cite these definitions when importing into Buchert or OpticalExtension. The module aggregates Calculus and Geometry primitives into explicit FRW expressions as a pure definition block with no internal proofs.

claimThe Friedmann-Robertson-Walker metric takes the form $ds^2 = -dt^2 + a(t)^2 (dr^2/(1-kr^2) + r^2 dΩ^2)$ with scale factor $a(t)$ and curvature parameter $k$; derived objects include the Christoffel symbols and the nonzero Ricci components $R_{00}$, $R_{ij}$.

background

This module resides in the Relativity.Cosmology section and re-exports geometry and calculus primitives to construct the standard FLRW line element. Upstream, the Geometry aggregator supplies the metric tensor and connection machinery while Calculus provides differentiation and curvature operators. The setting uses RS-native units with $c=1$ and prepares the metric for later use in backreaction and optical calculations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

These definitions feed the Buchert module for algebraic cancellation of the kinematical backreaction $Q_D$ under irrotational potential flow and the OpticalExtension module for the $Υ(a)$ rescaling of the Sachs focusing term. They also support the GW.ActionExpansion and TensorDecomposition modules. The block supplies the geometric foundation referenced in the Dark-Energy.tex paper for ILG cosmology propositions.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)