summary
This definition supplies a five-point textual summary of Big Bang Nucleosynthesis abundances derived from Recognition Science. Cosmologists comparing early-universe yields to observations would cite the listed values for the baryon-to-photon ratio and helium fraction. The content is supplied directly as a hardcoded list of strings drawn from the module's RS perspective.
claimThe RS summary of BBN is the list containing $η ≈ 6×10^{-10}$ from the $φ$-ladder, $^4$He mass fraction ≈25% from the neutron-to-proton ratio at freeze-out, D/H as a sensitive probe of $η$, the $^7$Li problem possibly resolved by eight-tick nuclear structure, and confirmation that $N_ν=3$.
background
The Cosmology.Nucleosynthesis module derives light-element abundances from RS principles. The baryon-to-photon ratio $η$ is obtained from the $φ$-ladder, nuclear densities occupy discrete $φ$-tiers, and the fundamental time quantum is the tick constant $τ_0=1$. Upstream CostAlgebra.H reparametrizes the J-cost as $H(x)=J(x)+1$, satisfying the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. NucleosynthesisTiers.of structures nuclear densities and photon fluxes in $φ$-tiers.
proof idea
The declaration is a direct definition that populates a List String with five fixed summary statements. No lemmas or tactics are applied; the strings are supplied verbatim from the module doc-comment on BBN.
why it matters in Recognition Science
This definition supplies the high-level claims for the COS-012 module on BBN abundances. It connects the $φ$-ladder derivation of $η$ and the eight-tick octave to observed helium and deuterium yields. The module states that predictions match observations remarkably well, with the lithium problem flagged as potentially addressable by 8-tick insight. It touches the open question of whether the lithium discrepancy requires additional RS structure.
scope and limits
- Does not compute explicit reaction rates or solve the Boltzmann equations.
- Does not provide numerical integration for abundance evolution.
- Does not address post-BBN evolution or stellar processing.
- Does not derive the exact value of $η$ within this file.
formal statement (Lean)
207def summary : List String := [
proof body
Definition body.
208 "η ≈ 6×10⁻¹⁰ from φ-ladder",
209 "⁴He ≈ 25% from n/p ratio",
210 "D/H sensitive probe of η",
211 "Li problem may need 8-tick insight",
212 "N_ν = 3 confirmed"
213]
214
215/-! ## Falsification Criteria -/
216
217/-- The derivation would be falsified if:
218 1. η not φ-related
219 2. ⁴He abundance very different from 25%
220 3. BBN predictions don't match (except Li) -/