dark_energy_match
plain-language theorem explainer
The geometric prediction for dark energy density matches the observed Planck value to within one sigma. Cosmologists examining ledger-based resolutions to the Hubble tension would cite this verification. The tactic proof obtains alpha/pi bounds, unfolds the three Omega_L definitions via simp, establishes tight interval bounds on the prediction with linarith, and reduces the absolute-value claim to two linear inequalities.
Claim. $| (11/16 - alpha/pi) - 0.6847 | < 0.0073$
background
Module T13 derives both the Hubble tension and dark energy density from ledger geometry. The dual-metric hypothesis supplies the ratio 13/12 between late and early Hubble parameters, while dark energy is obtained from the passive-field volume fraction 11/16 corrected by the fine-structure term alpha/pi. Omega_L_pred is defined as dark_energy_base minus alpha/Real.pi with dark_energy_base equal to the rational 11/16; Omega_L_exp and Omega_L_err are the fixed reals 0.6847 and 0.0073 respectively.
proof idea
The proof first invokes alpha_over_pi_bounds to obtain the interval (0.0023, 0.0024) for alpha/pi. It then applies simp to unfold Omega_L_pred, Omega_L_exp and Omega_L_err. Two auxiliary statements establish that Omega_L_pred lies strictly inside (0.6851, 0.6852) by combining the alpha/pi bounds with norm_num on 11/16 and linarith. The final step rewrites the absolute-value inequality as a pair of linear inequalities and discharges both with linarith.
why it matters
The result completes the T13 derivation by confirming that the ledger-derived Omega_Lambda lies inside the reported 1-sigma observational window. It rests on the dual-metric hypothesis for the Hubble ratio and on the alpha bounds imported from CKM geometry. Within the Recognition framework the match supplies a parameter-free account of dark energy that is consistent with the same geometric constants used for the fine-structure constant and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.