Omega_L_pred
Omega_L_pred computes the predicted dark energy density as the base fraction 11/16 minus alpha over pi. Cosmologists examining the Hubble tension in Recognition Science cite this when matching ledger-derived predictions to Planck observations. The definition is a direct one-line subtraction combining the passive-field base with the fine-structure correction.
claim$Ω_Λ^pred = 11/16 - α/π$
background
The HubbleTension module derives dark energy from the fractional volume of the passive field geometry relative to the Q3 vertex basis, giving the base term 11/16. Alpha is the fine-structure constant imported from Constants.Alpha. Upstream, dark_energy_base supplies the rational 11/16 while the from theorem in PrimitiveDistinction encodes the passage from seven axioms to four structural conditions.
proof idea
The definition subtracts alpha divided by Real.pi from the dark_energy_base value. It is a one-line arithmetic wrapper that applies the dark_energy_base definition and the alpha constant.
why it matters in Recognition Science
Omega_L_pred supplies the left-hand side for the dark_energy_match theorem, which verifies agreement with observed Omega_Lambda to within 1 sigma, and for alpha_over_pi_bounds, which constrains the correction interval. It realizes the dark energy formula stated in the module doc-comment for the T13 Hubble Tension derivation.
scope and limits
- Does not derive the 11/16 base fraction from the phi-ladder.
- Does not incorporate measurement uncertainties or error propagation.
- Does not compute the Hubble constant values H_early or H_late.
Lean usage
simp only [Omega_L_pred, dark_energy_base]formal statement (Lean)
67noncomputable def Omega_L_pred : ℝ :=
proof body
Definition body.
68 (dark_energy_base : ℝ) - alpha / Real.pi
69
70/-! ## Geometric Derivation -/
71
72/-- The Hubble ratio 13/12 derives from ledger edge count (12) + time dimension (1). -/