dark_energy_base
plain-language theorem explainer
dark_energy_base sets the rational 11/16 as the uncorrected dark energy fraction from 11 passive edges over twice the 8 vertices of the three-cube. Researchers deriving Hubble tension predictions in Recognition Science cite it when forming Ω_Λ after the α/π correction. The definition is a bare assignment that downstream results unfold via simp and norm_num.
Claim. The base fraction for dark energy density is defined as $11/16$, the ratio of passive edges to twice the vertices of the three-cube.
background
The HubbleTension module derives cosmological predictions from ledger geometry under the Dual Metric Hypothesis. Dark energy density takes the form Ω_Λ = E_passive/(2 V_total) - α/π, where E_passive = 11 and V_total = 8 (vertices of Q_3). The base term isolates the geometric contribution before the small correction α/π ≈ 0.0023, producing the explicit fraction 11/16.
proof idea
The body is the direct assignment dark_energy_base := 11/16. No lemmas or tactics appear. Downstream theorems recover the geometric identity by simp only [dark_energy_base] followed by norm_num.
why it matters
This constant anchors the T13 predictions for dark energy. It is used by dark_energy_from_geometry to recover the edge-vertex ratio, by Omega_L_pred to subtract α/π, and by dark_energy_match to establish 1σ agreement with Planck data. The certificate theorem hubble_and_lambda_connected pairs it with the 13/12 Hubble ratio, showing both arise from the same D=3 cube structure. It thereby links the eight-tick octave and spatial dimension forcing to observable cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.