`InflatonRegime`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.InflatonPotentialStructural on GitHub at line 23.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  20namespace IndisputableMonolith.Cosmology.InflatonPotentialStructural
  21open Constants
  22
  23inductive InflatonRegime where
  24  | slowRollPlateau
  25  | slowRollSlope
  26  | hilltopDecline
  27  | reheating
  28  | radiationEra
  29  deriving DecidableEq, Repr, BEq, Fintype
  30
  31theorem inflatonRegime_count : Fintype.card InflatonRegime = 5 := by decide
  32
  33/-- e-fold count N_e = 44 (gap-45 ladder). -/
  34def efoldCount : ℕ := 44
  35theorem efoldCount_eq : efoldCount = 44 := rfl
  36
  37/-- Slow-roll parameter ε = 1/(2φ⁵). -/
  38noncomputable def slowRollEpsilon : ℝ := 1 / (2 * phi ^ 5)
  39
  40/-- Slow-roll parameter η = 1/φ⁵. -/
  41noncomputable def slowRollEta : ℝ := 1 / phi ^ 5
  42
  43/-- φ⁵ = 5φ + 3 (Fibonacci identity). -/
  44theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
  45  have h2 := phi_sq_eq
  46  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  47  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  48  nlinarith
  49
  50theorem slowRollEpsilon_pos : 0 < slowRollEpsilon := by
  51  unfold slowRollEpsilon
  52  apply div_pos one_pos
  53  exact mul_pos (by norm_num) (pow_pos phi_pos 5)

papers checked against this theorem

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