critical_density
plain-language theorem explainer
The critical density is defined as ρ_c = 3 H_0² / (8 π G) with H_0 ≈ 2.3 × 10^{-18} s^{-1} and the RS-native gravitational constant. Cosmologists examining the flatness problem cite this value to quantify the observed Ω ≈ 1 and the required early-universe tuning. The definition is a direct numerical instantiation of the Friedmann critical-density formula using imported constants.
Claim. The critical density is given by ρ_c = 3 H_0² / (8 π G) where H_0 ≈ 2.3 × 10^{-18} s^{-1} is the present Hubble parameter and G is the gravitational constant.
background
The Cosmology.FlatnessProblem module addresses why the observed spatial curvature satisfies |Ω - 1| < 0.0002 today. In Recognition Science, Ω = 1 is the unique value consistent with ledger structure; deviations grow as |Ω - 1| ∝ a²(t) in radiation domination and ∝ a(t) in matter domination, so early fine-tuning appears required. The critical density supplies the reference scale ρ_c = 3 H² / (8 π G) against which observed density is compared.
proof idea
One-line definition that directly evaluates the standard Friedmann expression using the numerical H_0 and the imported G constant from Constants.
why it matters
This definition anchors the COS-005 flatness discussion by fixing the reference density that enters Ω = ρ / ρ_c. It supports the RS claim that critical density follows from J-cost minimization and that φ-constraints force flatness. The module uses it to contrast the unstable equilibrium of standard cosmology with the ledger-enforced stability in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.