bbnReactions

formal source

  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
  91
  92    After neutron decay before BBN:
  93    n/p ≈ 1/7
  94
  95    This determines ⁴He abundance! -/
  96noncomputable def neutron_proton_ratio : ℝ := 1/7
  97
  98/-- Helium-4 mass fraction calculation:
  99
 100    If n/p = 1/7, and all neutrons go to ⁴He:
 101
 102    2 neutrons + 2 protons → ⁴He
 103    For 1 neutron : 7 protons:
 104    1n + 1p → in He, 6p left free
 105