`lambdaRS_band`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.CosmologicalConstantFromRS
domain: Physics
line: 41 · 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 41.

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

  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
  59  lambda_pos : 0 < lambdaRS
  60  lambda_band : (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03
  61
  62noncomputable def cosmologicalConstantCert : CosmologicalConstantCert where
  63  phi5_val := phi5_eq
  64  lambda_pos := lambdaRS_pos
  65  lambda_band := lambdaRS_band
  66
  67end IndisputableMonolith.Physics.CosmologicalConstantFromRS

papers checked against this theorem

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