`eta`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.Nucleosynthesis
domain: Cosmology
line: 60 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.Nucleosynthesis on GitHub at line 60.

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

  57noncomputable def lithium7_ratio : ℝ := 1.6e-10
  58
  59/-- The baryon-to-photon ratio. -/
  60noncomputable def eta : ℝ := 6.1e-10
  61
  62/-! ## The BBN Chain -/
  63
  64/-- The nuclear reaction chain in BBN:
  65
  66    1. n + p → D + γ (deuterium formation)
  67    2. D + D → ³He + n (and other branches)
  68    3. D + D → ³H + p
  69    4. ³He + n → ³H + p
  70    5. ³H + D → ⁴He + n
  71    6. ³He + D → ⁴He + p
  72    7. ⁴He + ³H → ⁷Li + γ
  73
  74    Most neutrons end up in ⁴He! -/
  75def bbnReactions : List String := [
  76  "n + p → D + γ",
  77  "D + D → ³He + n",
  78  "D + D → ³H + p",
  79  "³He + n → ³H + p",
  80  "³H + D → ⁴He + n",
  81  "³He + D → ⁴He + p",
  82  "⁴He + ³H → ⁷Li + γ"
  83]
  84
  85/-! ## Key Physics -/
  86
  87/-- The neutron-to-proton ratio at freeze-out:
  88
  89    When the weak interaction rate drops below expansion rate:
  90    n/p ~ exp(-Δm/T_freeze) ≈ 1/6

papers checked against this theorem

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