ricci_FRW_ij
plain-language theorem explainer
The definition supplies the spatial Ricci component for the FRW metric expressed through the scale factor a(t), its first logarithmic derivative H(t), and second derivative. Relativists and cosmologists would cite it when assembling curvature scalars for expanding spacetimes. The definition is a direct algebraic assembly of those derivatives with no external lemmas.
Claim. Let $a(t)>0$ be a scale factor. Set $H(t)=a'(t)/a(t)$ and let $a''(t)$ denote the second derivative. The spatial Ricci component equals $a(t)^2(a''(t)/a(t)+2H(t)^2)$.
background
ScaleFactor is the structure holding a strictly positive function a:ℝ→ℝ. The module builds the standard FRW line element and its curvature tensors inside the Recognition Science setting. Upstream ricci_FRW_00 supplies the time-time component as -3 a''(t)/a(t). The local H appearing here is the Hubble rate; it is unrelated to the shifted cost function H(x)=J(x)+1 defined in CostAlgebra.
proof idea
The definition is a direct term-mode construction. It first forms H as the logarithmic derivative of a at t, binds a_ddot to the second derivative of a at t, then returns the product a(t)^2 times (a_ddot/a(t) plus twice H squared). No tactics or lemmas intervene.
why it matters
Together with ricci_FRW_00 this definition supplies the two independent Ricci components needed for the FRW curvature. The module comment states the intended claim that both match the standard expressions used in cosmology. It therefore closes the geometric side of the FRW setup before any link to the phi-ladder or large-scale structure results is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.