`bitCorrectionBound`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkEnergyEquationOfState 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

formal source

  24def wLambda : ℝ := -1
  25
  26/-- BIT correction bound: |δw| ≤ J(φ). -/
  27noncomputable def bitCorrectionBound : ℝ := 1 / phi - 3 / 2 + 1  -- approximate J(φ) ≈ 0.118
  28
  29/-- Five dark energy models. -/
  30inductive DarkEnergyModel where
  31  | cosmologicalConstant | quintessence | phantom | quintom | holographic
  32  deriving DecidableEq, Repr, BEq, Fintype
  33
  34theorem darkEnergyModelCount : Fintype.card DarkEnergyModel = 5 := by decide
  35
  36structure DarkEnergyEoSCert where
  37  five_models : Fintype.card DarkEnergyModel = 5
  38  baseline_w : wLambda = -1
  39
  40def darkEnergyEoSCert : DarkEnergyEoSCert where
  41  five_models := darkEnergyModelCount
  42  baseline_w := rfl
  43
  44end IndisputableMonolith.Cosmology.DarkEnergyEquationOfState

papers checked against this theorem

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