module module high

`IndisputableMonolith.Cosmology.CosmologicalConstantDerivation`

The module defines the RS prediction for the cosmological constant density parameter as 11/16 minus alpha over pi, with the geometric seed drawn from the D=3 ledger and the correction from registry predictions. Cosmologists addressing dark energy or the Hubble tension would cite it for its parameter-free form inside Recognition Science. The module assembles definitions and bounds from upstream constants and proved registry items without internal proofs.

claim$Ω_Λ = 11/16 - α/π$, where 11/16 is the geometric seed from the D=3 ledger and α/π supplies the fine-structure correction.

background

Recognition Science obtains cosmological parameters from the forcing chain that terminates in D=3 spatial dimensions. The module imports the fundamental RS time quantum τ₀ from Constants and the calculated proofs for registry predictions from RegistryPredictionsProved. It introduces the geometric seed 11/16 for the dark energy fraction together with the α/π correction term.

proof idea

This is a definition module containing no proofs; it assembles the C-010 prediction from imported constants and registry items.

why it matters in Recognition Science

The module supplies the C-010 definition that feeds the Hubble tension resolution in the downstream HubbleTensionCertificate module. It closes the cosmological constant prediction inside the T-001 registry item by giving the explicit formula derived from the D=3 geometric seed.

scope and limits

Does not derive the numerical value of the fine-structure constant.
Does not incorporate quantum gravity corrections.
Does not compute the Hubble constant directly.
Does not perform comparison against observational datasets.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.HubbleTensionCertificate module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Unification.RegistryPredictionsProved module_import

declarations in this module (12)

def Omega_Lambda_RS L85
theorem Omega_Lambda_RS_well_defined L88
theorem Omega_Lambda_lt_upper_bound L93
theorem Omega_Lambda_positive L100
theorem Omega_Lambda_bounds L107
def geometric_seed L121
theorem geometric_seed_pos L124
theorem alpha_over_pi_small L134
theorem Lambda_not_planck_scale L145
theorem Lambda_no_fine_tuning L151
theorem Hubble_from_Omega_Lambda L162
def C010_certificate L183