Omega_L_pred
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.