`lambdaRS_band`

proved

show as: view math explainer →

module: IndisputableMonolith.Cosmology.OmegaLambdaBITKernelBand
domain: Cosmology
line: 34 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.OmegaLambdaBITKernelBand on GitHub at line 34.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  31  nlinarith
  32
  33/-- Λ_RS ∈ (1.88, 2.03). -/
  34theorem lambdaRS_band :
  35    (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03 := by
  36  unfold lambdaRS
  37  have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
  38  have h1 := phi_gt_onePointSixOne
  39  have h2 := phi_lt_onePointSixTwo
  40  constructor
  41  · have : 8 * phi ^ 5 / 45 > 8 * (5 * 1.61 + 3) / 45 := by
  42      apply div_lt_div_of_pos_right _ (by norm_num)
  43      nlinarith
  44    linarith
  45  · have : 8 * phi ^ 5 / 45 < 8 * (5 * 1.62 + 3) / 45 := by
  46      apply div_lt_div_of_pos_right _ (by norm_num)
  47      nlinarith
  48    linarith
  49
  50/-- Λ_RS > 0. -/
  51theorem lambdaRS_pos : 0 < lambdaRS := by
  52  unfold lambdaRS
  53  apply div_pos _ (by norm_num)
  54  apply mul_pos (by norm_num)
  55  exact pow_pos phi_pos 5
  56
  57structure OmegaLambdaBandCert where
  58  phi5_value : phi ^ 5 = 5 * phi + 3
  59  lambda_band : (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03
  60  lambda_pos : 0 < lambdaRS
  61
  62noncomputable def omegaLambdaBandCert : OmegaLambdaBandCert where
  63  phi5_value := phi5_eq
  64  lambda_band := lambdaRS_band

papers checked against this theorem

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