`InflationModel`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.CosmicInflationFromJCost on GitHub at line 23.

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

  20namespace IndisputableMonolith.Cosmology.CosmicInflationFromJCost
  21open Common.CanonicalJBand
  22
  23inductive InflationModel where
  24  | chaotic | natural | starobinsky | higgsInflation | axionMonodromy
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem inflationModelCount : Fintype.card InflationModel = 5 := by decide
  28
  29/-- Inflation ends when J-cost crosses the canonical threshold. -/
  30theorem inflation_ends_at_threshold : J 1 = 0 := J_one
  31
  32structure CosmicInflationCert where
  33  five_models : Fintype.card InflationModel = 5
  34  reheating_condition : J 1 = 0
  35  threshold : CanonicalCert
  36
  37noncomputable def cosmicInflationCert : CosmicInflationCert where
  38  five_models := inflationModelCount
  39  reheating_condition := inflation_ends_at_threshold
  40  threshold := cert
  41
  42end IndisputableMonolith.Cosmology.CosmicInflationFromJCost

papers checked against this theorem

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