def
definition
lambdaRS
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CosmologicalConstantFromRS on GitHub at line 25.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
22open Constants
23
24/-- Λ_RS = 8φ⁵/45. -/
25noncomputable def lambdaRS : ℝ := 8 * phi ^ 5 / 45
26
27/-- φ⁵ = 5φ + 3 (Fibonacci identity). -/
28theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
29 have h2 := phi_sq_eq
30 have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
31 have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
32 nlinarith
33
34/-- Λ_RS > 0. -/
35theorem lambdaRS_pos : 0 < lambdaRS := by
36 unfold lambdaRS
37 apply div_pos _ (by norm_num)
38 apply mul_pos (by norm_num) (pow_pos phi_pos 5)
39
40/-- Λ_RS ∈ (1.88, 2.03). -/
41theorem lambdaRS_band : (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03 := by
42 unfold lambdaRS
43 have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
44 have h1 := phi_gt_onePointSixOne
45 have h2 := phi_lt_onePointSixTwo
46 rw [h5]
47 constructor
48 · have : 8 * (5 * phi + 3) / 45 > 8 * (5 * 1.61 + 3) / 45 := by
49 apply div_lt_div_of_pos_right _ (by norm_num)
50 nlinarith
51 linarith
52 · have : 8 * (5 * phi + 3) / 45 < 8 * (5 * 1.62 + 3) / 45 := by
53 apply div_lt_div_of_pos_right _ (by norm_num)
54 nlinarith
55 linarith