theorem
proved
hubble_formula_structure
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.CosmologicalPredictionsProved on GitHub at line 83.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
80 linarith
81
82/-- **CALCULATED**: Hubble constant formula structure. -/
83theorem hubble_formula_structure : ∃ (H0 : ℝ), H0 = Real.log phi / 8 := by
84 use Real.log phi / 8
85
86/-! ## Section: Phi Powers for Cosmology -/
87
88/-- **CALCULATED**: φ² bounds (useful for many calculations).
89
90 With 1.61 < φ < 1.62: 2.59 < φ² < 2.62 -/
91theorem phi_squared_bounds : (2.59 : ℝ) < phi^2 ∧ phi^2 < (2.62 : ℝ) := by
92 have h1 : phi ^ 2 = phi + 1 := phi_sq_eq
93 rw [h1]
94 have h2 : phi > (1.61 : ℝ) := phi_gt_onePointSixOne
95 have h3 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
96 constructor
97 · nlinarith
98 · nlinarith
99
100/-- **CALCULATED**: φ⁴ = (φ²)² bounds.
101
102 With 2.59 < φ² < 2.62: 6.7 < φ⁴ < 6.9 -/
103theorem phi_fourth_bounds : (6.7 : ℝ) < (phi : ℝ)^(4 : ℕ) ∧ (phi : ℝ)^(4 : ℕ) < (6.9 : ℝ) := by
104 have h1 : (phi : ℝ)^(4 : ℕ) = (phi ^ 2) ^ 2 := by ring
105 rw [h1]
106 have h2 : (2.59 : ℝ) < phi^2 := phi_squared_bounds.1
107 have h3 : phi^2 < (2.62 : ℝ) := phi_squared_bounds.2
108 constructor
109 · nlinarith
110 · nlinarith
111
112/-- **CALCULATED**: φ⁵ bounds (for BAO scale predictions).
113