`dark_energy_implies_subunit`

proved

show as: view math explainer →

module: IndisputableMonolith.Cosmology.DarkEnergyEvolutionStructure
domain: Cosmology
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkEnergyEvolutionStructure on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  35  h.1
  36
  37/-- Dark-energy evolution structure enforces the subunit upper bound. -/
  38theorem dark_energy_implies_subunit (h : dark_energy_evolution_from_ledger) :
  39    EarlyUniverse.omega_lambda < 1 :=
  40  h.2
  41
  42/-- Dark-energy structure excludes the degenerate `Ω_Λ = 0` endpoint. -/
  43theorem dark_energy_implies_ne_zero (h : dark_energy_evolution_from_ledger) :
  44    EarlyUniverse.omega_lambda ≠ 0 :=
  45  ne_of_gt h.1
  46
  47/-- Dark-energy structure excludes the degenerate `Ω_Λ = 1` endpoint. -/
  48theorem dark_energy_implies_ne_one (h : dark_energy_evolution_from_ledger) :
  49    EarlyUniverse.omega_lambda ≠ 1 :=
  50  ne_of_lt h.2
  51
  52end DarkEnergyEvolutionStructure
  53end Cosmology
  54end IndisputableMonolith

papers checked against this theorem

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