`inflatonCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.InflatonPotentialStructural
domain: Cosmology
line: 72 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.InflatonPotentialStructural on GitHub at line 72.

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

formal source

  69  eta_pos : 0 < slowRollEta
  70  spectral_index_in_band : ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ))
  71
  72noncomputable def inflatonCert : InflatonCert where
  73  five_regimes := inflatonRegime_count
  74  efolds := efoldCount_eq
  75  phi5_fibonacci := phi5_eq
  76  epsilon_pos := slowRollEpsilon_pos
  77  eta_pos := slowRollEta_pos
  78  spectral_index_in_band := spectralIndex_band
  79
  80end IndisputableMonolith.Cosmology.InflatonPotentialStructural

papers checked against this theorem

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