pith. machine review for the scientific record. sign in
def definition def or abbrev high

bbnReactions

show as:
view Lean formalization →

The list of dominant nuclear reactions in Big Bang nucleosynthesis is supplied as a fixed enumeration of seven processes. Cosmologists working within Recognition Science cite it when linking the phi-derived baryon-to-photon ratio to observed light-element yields. The definition is a direct static list with no computation or lemmas applied.

claimThe nuclear reaction chain for Big Bang nucleosynthesis is the list $n + p → D + γ$, $D + D → {}^3He + n$, $D + D → {}^3H + p$, ${}^3He + n → {}^3H + p$, ${}^3H + D → {}^4He + n$, ${}^3He + D → {}^4He + p$, ${}^4He + {}^3H → {}^7Li + γ$.

background

In the Recognition Science treatment of Big Bang nucleosynthesis, light elements form in the first minutes after the Big Bang with abundances controlled by the baryon-to-photon ratio eta (derived from phi) and nuclear rates tied to the eight-tick structure. The module sets the target of deriving helium-4, deuterium, and lithium-7 yields from these RS-constrained parameters. Upstream, the shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y), while the before relation orders snapshots by tick index to enforce temporal monotonicity of defects.

proof idea

The definition constructs the list by direct enumeration of the seven reaction strings. No lemmas from CostAlgebra or TimeEmergence are invoked inside this declaration; it is a static data definition.

why it matters in Recognition Science

This supplies the reaction network required by downstream abundance calculations such as helium4_mass_fraction and lithium_predicted. It advances the COS-012 goal of matching observed yields (helium ~24-25 percent, lithium problem at 1.6e-10) using eta from phi and rates from the eight-tick octave (T7). The list therefore bridges the phi-ladder mass formula to concrete BBN observables.

scope and limits

formal statement (Lean)

  75def bbnReactions : List String := [

proof body

Definition body.

  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! -/

depends on (3)

Lean names referenced from this declaration's body.