christoffel_FRW
plain-language theorem explainer
Defines the Christoffel symbols for the flat FRW metric via case analysis on indices using the scale factor a(t). Cosmologists deriving curvature or geodesics in expanding universes would reference this when working inside the Recognition Science framework. The definition computes the Hubble parameter as the logarithmic derivative of a and returns H a squared for the temporal-spatial components or H for the mixed terms.
Claim. The Christoffel symbol $Γ^μ_{ρσ}(t)$ for the FRW metric equals $H(t) [a(t)]^2$ when $μ=0$ and $ρ=σ>0$, equals $H(t)$ when $μ>0$ and either ($ρ=0$, $σ=μ$) or ($ρ=μ$, $σ=0$), and equals zero otherwise, where $H(t)=ȧ(t)/a(t)$ and $a$ satisfies $a>0$.
background
ScaleFactor is the structure holding a map $a:ℝ→ℝ$ together with the axiom that $a(t)>0$ for all $t$. The FRWMetric module imports geometry and calculus to support metric and connection computations in the Recognition Science cosmology setting. Upstream results include the shifted cost $H(x)=J(x)+1$ from CostAlgebra, which converts the Recognition Composition Law into the d'Alembert equation, and the scale function $phi^k$ from LargeScaleStructureFromRS.
proof idea
One-line wrapper that computes the Hubble parameter locally as the logarithmic derivative of the scale factor, then branches on the four indices to select the standard non-zero FRW components or returns zero.
why it matters
Supplies the connection coefficients required for curvature calculations in the FRW sector of Recognition Science cosmology. It directly precedes the Ricci tensor definitions ricci_FRW_00 and ricci_FRW_ij inside the same module and aligns with the phi-ladder expansion and eight-tick octave structure. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.