module module moderate

`IndisputableMonolith.Cosmology.DarkEnergy`

The Cosmology.DarkEnergy module defines the present-day Hubble parameter H₀ ≈ 2.2 × 10^{-18} s^{-1} together with Planck time, universe age, cosmic ratios, spacetime regions, balance conditions, densities, expansion tension, and the cosmological constant in RS-native units. It extends the Constants and Cost modules to cosmological scales for expansion and dark energy work. The module consists entirely of definitions with no theorems or proofs.

claim$H_0 ≈ 2.2 \times 10^{-18} \, \mathrm{s}^{-1}$ (today's Hubble parameter), $t_{\mathrm{planck}}$, $t_{\mathrm{universe}}$, cosmic ratio, SpacetimeRegion, isBalanced, entryDensity, costDensity, expansionTension, cosmologicalConstant, and $\Lambda > 0$.

background

The module imports IndisputableMonolith.Constants, whose doc states the fundamental RS time quantum τ₀ = 1 tick, and IndisputableMonolith.Cost. It introduces sibling definitions H0, t_planck, t_universe, cosmicRatio, cosmic_ratio_large, SpacetimeRegion, isBalanced, entryDensity, costDensity, expansionTension, cosmologicalConstant, and lambda_positive. These objects operate in the cosmology domain and apply the core RS time quantum and cost structures at large scales.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Hubble parameter and cosmological constant that support dark energy and expansion modeling in the Recognition Science framework. It connects the Constants and Cost modules to cosmological applications, enabling density and tension calculations. No downstream theorems are recorded in the dependency graph.

scope and limits

Does not derive H0 from the J-function or forcing chain.
Does not include observational comparisons or data fits.
Does not state the Friedmann equations or metric.
Does not address quantum corrections or higher-order terms.

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