bbnReactions
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.