lambdaFromJCost
plain-language theorem explainer
The definition supplies the cosmological constant as the J-cost evaluated at the golden ratio multiplied by the square of the present Hubble parameter and divided by the cube of the golden ratio. Cosmologists modeling dark energy as residual ledger tension during expansion cite this expression to link Recognition Science costs to the observed acceleration scale. It is realized as a direct algebraic combination of the J-cost function with the Hubble parameter.
Claim. $Λ = J(φ) ⋅ H₀² / φ³$, where $J$ is the J-cost function, $φ$ the golden ratio, and $H₀$ the Hubble parameter today.
background
The Cosmology.DarkEnergy module treats dark energy as ledger tension per unit volume. Expansion creates new 3D cells that require fresh ledger entries; the J-cost of maintaining global balance across these entries supplies the residual energy density. Upstream, ObserverForcing.cost states that the cost of a recognition event equals the J-cost of its state, while PhiForcingDerived.of supplies the underlying J-cost structure and H0 defines the Hubble parameter as 2.2 × 10^{-18} s^{-1} in natural units.
proof idea
This is a one-line definition that multiplies the J-cost at phi by H0 squared and divides by phi cubed, drawing directly on the cost function from ObserverForcing and the H0 constant.
why it matters
The definition realizes the core step of COS-006 by expressing Λ as ledger tension per unit volume. It connects to the J-uniqueness and phi fixed-point steps in the forcing chain and supplies the input for sibling definitions such as cosmologicalConstant and lambda_positive. The construction uses the phi-ladder to relate the Planck scale to the Hubble scale without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.