pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Cosmology.Nucleosynthesis

show as:
view Lean formalization →

The Cosmology.Nucleosynthesis module assembles RS-native definitions for Big Bang nucleosynthesis abundances including the helium-4 mass fraction Yp. Cosmologists testing early-universe models against observed light-element ratios would cite these values. The module organizes its content as a collection of explicit definitions and calculated observables built directly from the imported constants and phi-forcing results.

claimThe module defines the helium-4 mass fraction $Y_p$, deuterium-to-hydrogen ratio, helium-3 ratio, lithium-7 ratio, baryon-to-photon ratio $eta$, neutron-proton ratio, and related BBN observables in the Recognition Science framework.

background

Recognition Science derives all structure from a discrete ledger carrying J-cost, with the upstream PhiForcing module proving that self-similarity forces the golden ratio $phi$ as the unique fixed point satisfying $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The Constants module supplies the fundamental time quantum $tau_0 = 1$ tick. This nucleosynthesis module applies those foundations to the early universe under the eight-tick octave and three-dimensional spatial structure, introducing explicit definitions for the listed abundance ratios and the lithium problem.

proof idea

This is a definition module, no proofs. It collects the nucleosynthesis quantities as direct definitions or calculations from the imported constants and forcing results, with each sibling declaration standing as an independent observable.

why it matters in Recognition Science

The module supplies the BBN observables that test the Recognition Science mass formula and phi-ladder against measured abundances, feeding the broader cosmology claims that close the loop from the T0-T8 forcing chain to observable predictions. It directly addresses the lithium problem and the eta window inside the alpha inverse band.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)