module module high

`IndisputableMonolith.Cosmology.DarkEnergy`

The Cosmology.DarkEnergy module supplies RS-native definitions for cosmological observables including the present Hubble parameter H0, Planck time, universe age, and density ratios. Researchers modeling expansion history or dark energy within the Recognition Science framework would cite these quantities. The module is purely definitional, importing the RS time quantum and cost functions to express all values in natural units.

claimThe module defines the present Hubble parameter $H_0$ in natural units together with Planck time $t_mathrm{Planck}$, cosmic age $t_mathrm{universe}$, cosmic density ratio, entry density, cost density, expansion tension, and the positive cosmological constant $Lambda$.

background

Recognition Science derives all constants from the functional equation and the time quantum $tau_0 = 1$ tick supplied by the Constants module. The Cost module provides the J-cost function and defect measures used to construct densities. This module applies those primitives to cosmology by defining a SpacetimeRegion, the isBalanced predicate, and derived quantities such as expansionTension and cosmologicalConstant.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the cosmological inputs required by any downstream dark-energy or expansion calculation in the Recognition framework. It translates the fundamental time quantum and phi-ladder into observable scales, supporting later derivations of the cosmological constant from the eight-tick octave and RCL.

scope and limits

Does not derive H0 from the forcing chain or RCL.
Does not contain dynamical Friedmann equations.
Does not address quantum corrections or inflation.
Does not compute numerical values beyond the supplied approximations.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (27)

def H0 L54
def t_planck L57
def t_universe L60
def cosmicRatio L63
theorem cosmic_ratio_large L66
structure SpacetimeRegion L73
def isBalanced L84
def entryDensity L87
def costDensity L90
def expansionTension L96
def cosmologicalConstant L100
theorem lambda_positive L106
def criticalDensity L113
def omegaLambda L116
def darkEnergyDensity L119
theorem dark_energy_dominates L122
def lambdaFromJCost L136
theorem lambda_order_of_magnitude L140
theorem lambda_smallness_natural L152
theorem no_fine_tuning L159
def equationOfState L167
theorem dark_energy_eos L170
theorem constant_energy_density L175
structure DarkEnergyPredictions L187
def rsPredictions L196
structure DarkEnergyFalsifier L209
theorem current_observations_consistent L220