ricci_FRW_00
plain-language theorem explainer
The (0,0) component of the Ricci tensor for the Friedmann-Robertson-Walker metric equals minus three times the second time derivative of the scale factor divided by the scale factor itself. Cosmologists reducing the Einstein equations to ordinary differential equations for cosmic expansion cite this expression inside the Recognition Science program. The implementation is a direct one-line definition that applies the second-derivative operator to the scale-factor function and normalizes the result.
Claim. The (0,0) component of the Ricci tensor for an FRW spacetime is given by $R_{00}(t) = -3 a''(t)/a(t)$, where $a:ℝ→ℝ$ is any positive scale factor.
background
The ScaleFactor structure packages a function a from the reals to the reals together with the axiom that a(t) > 0 for every real t. In the FRWMetric module this structure parametrizes the homogeneous isotropic line element used throughout Recognition Science cosmology. The upstream scale definition constructs concrete instances a(t) = phi^k for natural numbers k, automatically satisfying the positivity requirement.
proof idea
The definition is a one-line wrapper that applies the second-derivative operator to the scale-factor component, divides the result by a(t), and multiplies by -3. No lemmas or tactics are required beyond the derivative primitives imported from the Calculus module.
why it matters
This definition supplies the R_{00} term that the downstream ricci_FRW_ij definition combines with the Hubble parameter and second-derivative terms to obtain the spatial Ricci components. Within the Recognition Science framework it supports reduction of the Einstein tensor to the Friedmann equations, thereby connecting the phi-ladder and Recognition Composition Law to the eight-tick octave and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.