`phi5_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.CosmologicalConstantFromRS
domain: Physics
line: 28 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.CosmologicalConstantFromRS on GitHub at line 28.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  56
  57structure CosmologicalConstantCert where
  58  phi5_val : phi ^ 5 = 5 * phi + 3

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.