Omega_L_exp
plain-language theorem explainer
This definition supplies the Planck-observed dark energy density parameter as the numerical constant 0.6847 for direct comparison in the Hubble Tension module. Cosmologists testing Recognition Science ledger predictions against data would cite it as the experimental anchor. It is a direct numerical assignment with no lemmas or reduction steps.
Claim. $Omega_Lambda^{exp} := 0.6847$
background
The module derives the Hubble Tension from the Dual Metric Hypothesis, where the late-to-early Hubble ratio equals 13/12 from the dynamic ledger (12 edges plus time) versus the static ledger (12 edges). Dark energy density follows from the passive field geometry fraction: Omega_Lambda equals E_passive over 2 V_total minus alpha over pi, with E_passive set to 11 and V_total to 8 (vertices of Q_3), giving base value 11/16 = 0.6875 before the alpha/pi correction of approximately 0.0023.
proof idea
Direct definition that assigns the constant 0.6847 to Omega_L_exp. No lemmas are applied and no tactics are invoked.
why it matters
It provides the observational benchmark that the dark_energy_match theorem uses to confirm the RS-derived Omega_L_pred lies within one sigma of experiment. The module doc positions this as the empirical closure for the T13 Hubble Tension resolution, linking the passive-field volume fraction to the alpha band and phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.