omega_lambda_bounded

formal source

  19namespace DarkEnergyEvolutionStructure
  20
  21/-- Baseline RS dark-energy density is positive and subunitary. -/
  22theorem omega_lambda_bounded :
  23    0 < EarlyUniverse.omega_lambda ∧ EarlyUniverse.omega_lambda < 1 :=
  24  EarlyUniverse.cosmological_constant_resolution
  25
  26/-- Structural placeholder for effective equation-of-state evolution. -/
  27def dark_energy_evolution_from_ledger : Prop :=
  28  0 < EarlyUniverse.omega_lambda ∧ EarlyUniverse.omega_lambda < 1
  29
  30theorem dark_energy_evolution_structure : dark_energy_evolution_from_ledger := omega_lambda_bounded
  31
  32/-- Dark-energy evolution structure enforces positivity of `Ω_Λ`. -/
  33theorem dark_energy_implies_positive (h : dark_energy_evolution_from_ledger) :
  34    0 < EarlyUniverse.omega_lambda :=
  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