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