def
definition
Omega_L_pred
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.HubbleTension on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
64noncomputable def H_late_pred : ℝ := H_early_exp * (hubble_ratio_topo : ℝ)
65
66/-- Predicted Dark Energy Density. -/
67noncomputable def Omega_L_pred : ℝ :=
68 (dark_energy_base : ℝ) - alpha / Real.pi
69
70/-! ## Geometric Derivation -/
71
72/-- The Hubble ratio 13/12 derives from ledger edge count (12) + time dimension (1). -/
73theorem hubble_ratio_from_ledger :
74 hubble_ratio_topo = (12 + 1) / 12 := by
75 simp only [hubble_ratio_topo]
76 norm_num
77
78/-- The Dark Energy base 11/16 derives from passive edges (11) over 2*vertices (16). -/
79theorem dark_energy_from_geometry :
80 dark_energy_base = 11 / (2 * 8) := by
81 simp only [dark_energy_base]
82 norm_num
83
84/-! ## Verification Theorems -/
85
86/-- Helper: 13/12 numerical bounds. -/
87theorem hubble_ratio_bounds :
88 (1.0833 : ℝ) < (hubble_ratio_topo : ℝ) ∧ (hubble_ratio_topo : ℝ) < (1.0834 : ℝ) := by
89 simp only [hubble_ratio_topo]
90 norm_num
91
92/-- Predicted late Hubble value. H_late_pred = 67.4 * (13/12) = 73.01666... -/
93theorem H_late_pred_value :
94 (73.01 : ℝ) < H_late_pred ∧ H_late_pred < (73.02 : ℝ) := by
95 simp only [H_late_pred, H_early_exp, hubble_ratio_topo]
96 norm_num
97