`inflationModelCount`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.CosmicInflationFromJCost on GitHub at line 27.

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

  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.