darkEnergyDensity
plain-language theorem explainer
Defines dark energy density as the product of the observed density parameter 0.68 and the critical density 3 H0 squared over 8 pi. Cosmologists working inside the Recognition Science ledger-tension model cite this when they need the numerical energy density that drives acceleration. The declaration is a direct one-line multiplication of two sibling definitions.
Claim. The dark energy density is given by $ρ_Λ = Ω_Λ ρ_c$, where $Ω_Λ = 0.68$ is the dark energy density parameter and $ρ_c = 3 H_0^2 / (8 π)$ is the critical density.
background
Module COS-006 derives the cosmological constant from ledger tension: the global J-cost balance requirement conflicts with the creation of new spacetime volume during expansion, leaving a residual energy density identified with Λ. Critical density is defined as $3 H_0^2 / (8 π)$ and the density parameter omegaLambda is set to the observed value 0.68. The upstream CosmologicalConstant module supplies the equivalent expression $λ c^2 / (8 π G)$ that this definition is intended to match numerically.
proof idea
One-line definition that multiplies the sibling definition omegaLambda by the sibling definition criticalDensity.
why it matters
Supplies the concrete dark energy density value that the CosmologicalConstant module consumes to reach the observed 70 percent of critical density. It realizes the COS-006 ledger-tension derivation and connects the abstract J-cost balance to the measured acceleration, consistent with the eight-tick octave and phi-ladder structure of the larger framework. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.