ScaleFactor
plain-language theorem explainer
The scale factor structure packages a positive real-valued function a(t) that scales spatial distances in homogeneous cosmologies. Workers deriving Christoffel symbols or Ricci tensors for FRW backgrounds cite this object as the single input parameter. The definition consists of a plain structure with one field and one positivity axiom, carrying no proof obligations.
Claim. A scale factor is a function $a : ℝ → ℝ$ such that $a(t) > 0$ for every real number $t$.
background
The FRWMetric module constructs the standard Friedmann-Robertson-Walker line element on a homogeneous isotropic background. The scale factor supplies the single time-dependent input that stretches the spatial sections while remaining strictly positive. All curvature quantities in the module are built by feeding an instance of this structure into the metric tensor, connection coefficients, and Ricci components. The module imports Geometry and Calculus but adds no further hypotheses on the function beyond the positivity axiom.
proof idea
The declaration is a structure definition. It introduces the field a of type ℝ → ℝ together with the field witnessing universal positivity, with no reduction, lemma application, or tactic script.
why it matters
This structure is the root object for the entire FRWMetric development. It is referenced by metric_FRW, christoffel_FRW, ricci_FRW_00, ricci_FRW_ij, and by the action expansions in the GW.ActionExpansion submodule. The structure therefore anchors all curvature and perturbation calculations performed on an expanding background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.