Omega_L_err
plain-language theorem explainer
Omega_L_err supplies the fixed numerical tolerance 0.0073 that certifies the ledger-derived dark energy density lies inside the one-sigma Planck interval. Cosmologists examining the dual-metric resolution of the Hubble tension cite this constant when they close the verification |Omega_L_pred - Omega_L_exp| < Omega_L_err. The declaration is a direct constant assignment with no reduction steps.
Claim. The error tolerance on the dark energy density parameter is defined by the constant assignment $0.0073$.
background
The module derives both the Hubble tension and the dark energy density from ledger geometry under the dual-metric hypothesis. The hypothesis states that the ratio of late to early Hubble constants equals 13/12, the ratio of the dynamic ledger (12 edges plus one time dimension) to the static ledger (12 edges). Dark energy density is obtained from the fractional volume of the passive field geometry: Omega_Lambda equals E_passive over 2 V_total minus alpha over pi, where E_passive equals 11 and V_total equals 8 (the vertices of Q3). This produces the base value 11/16 = 0.6875, which is then corrected by the alpha/pi term approximately 0.0023 to reach the prediction 0.6852.
proof idea
Direct constant definition that assigns the real number 0.0073 with no lemmas or tactics applied.
why it matters
The constant supplies the tolerance that lets the downstream theorem dark_energy_match conclude that the geometric prediction matches observation inside one sigma. It thereby completes the verification step of the T13 derivation of dark energy from the passive-field volume relative to the Q3 vertex basis. The parent result dark_energy_match invokes alpha_over_pi_bounds together with this tolerance to obtain the final inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.