dark_energy_base_value
plain-language theorem explainer
The theorem supplies the real-valued decimal for the dark energy base fraction derived from passive-field volume in the cube geometry. Cosmologists using the dual-metric account of the Hubble tension cite it to obtain the starting numerical value before the alpha/pi correction. The proof is a one-line term reduction that unfolds the rational definition and normalizes the arithmetic.
Claim. The dark energy base fraction, obtained as $E_{passive}/(2V_{total})$ with $E_{passive}=11$ and $V_{total}=8$, equals $0.6875$ when cast from rationals to reals.
background
The module derives dark energy density from ledger geometry via the formula $Omega_Lambda = E_{passive}/(2 V_{total}) - alpha/pi$, where the base term before correction is the rational 11/16. This supplies the numerical anchor for the T13 Hubble-tension prediction that matches Planck data after the small fine-structure correction. The upstream definition dark_energy_base : Q := 11/16 provides the exact rational, while alpha : R := 1/alphaInv supplies the correction term used downstream.
proof idea
The term proof first applies simp only [dark_energy_base] to replace the left-hand side by the definition 11/16, then invokes norm_num to confirm numeric equality with the decimal 0.6875. No external lemmas beyond the imported simplification and numeric tactics are required.
why it matters
The result closes the conversion step that turns the rational ledger fraction into real arithmetic for the T13 dark-energy prediction. It feeds the base value 0.6875 into the subsequent correction by alpha/pi that produces the forecast 0.6852, lying inside the Planck 1-sigma interval. The declaration therefore links the geometric ledger construction directly to observable cosmological parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.