`lambdaRS_pos`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.OmegaLambdaBITKernelBand on GitHub at line 51.

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

  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
  65  lambda_pos := lambdaRS_pos
  66
  67end IndisputableMonolith.Cosmology.OmegaLambdaBITKernelBand

papers checked against this theorem

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