metric_FRW
plain-language theorem explainer
The metric_FRW definition assembles the standard diagonal FRW line element from a supplied positive scale-factor function a(t). Cosmologists working inside the Recognition Science framework cite it when embedding the phi-ladder scale into spacetime geometry for later curvature calculations. The construction is a direct index-case definition of the component function together with an exhaustive case-analysis proof of symmetry.
Claim. The FRW metric tensor is the symmetric bilinear form whose components are $g_{00}=-1$, $g_{ii}=a(t)^2$ for $i=1,2,3$, and $g_{ij}=0$ otherwise, where $t=x^0$ and $a$ is any positive real-valued function of time.
background
ScaleFactor is the structure consisting of a map $a:ℝ→ℝ$ together with the positivity axiom $a(t)>0$ for every $t$. MetricTensor is the interface that packages a component map $g$ from spacetime points and index pairs into reals, plus the symmetry requirement $g(x,μ,ν)=g(x,ν,μ)$. The module imports the geometry and calculus packages that supply the underlying index and bilinear-form types. Upstream, the scale definition from LargeScaleStructureFromRS supplies concrete values $a(t)=ϕ^k$ drawn from the Recognition Science ladder.
proof idea
The definition directly encodes the component function by testing whether the lowered indices are both zero (time-time entry), equal and positive (spatial diagonal), or neither (off-diagonal zero). Symmetry is discharged by four nested by_cases on the equality and positivity predicates, each branch collapsing to reflexivity or a single simplification step.
why it matters
This definition supplies the geometric substrate for the sibling Christoffel and Ricci computations inside the same module. It realizes the homogeneous isotropic metric presupposed by the Recognition Science cosmology layer, directly tying the scale factor to the phi-based forcing chain (T5–T8). No open scaffolding questions are attached to the declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.