pith. sign in
module module high

IndisputableMonolith.Cosmology.PrimordialNucleosynthesisFromRS

show as:
view Lean formalization →

This module establishes the helium-4 mass fraction from Recognition Science in the primordial nucleosynthesis setting. Cosmologists deriving BBN abundances from first-principles frameworks would cite it to link RS constants to the observed value. The module defines nucleus types and counts then derives the fraction algebraically from imported RS time quantum and constants.

claimThe helium-4 mass fraction satisfies $Y_{^4He} ≈ 1/4$.

background

The module sits in the cosmology section of Recognition Science and imports the fundamental RS time quantum τ₀ = 1 tick from Constants. It introduces sibling definitions for PrimordialNucleus, primordialNucleusCount, heliumFraction, and BBNCert to model early-universe abundances in RS-native units. The local setting connects the forcing chain constants (c=1, ħ=φ^{-5}) to observable light-element yields without external nuclear data.

proof idea

This is a definition module, no proofs. It structures the argument by declaring PrimordialNucleus, computing counts via RS parameters, stating heliumFraction_eq, and certifying the observed match through bbnCert.

why it matters in Recognition Science

This module supplies the helium-4 fraction that closes the BBN link in the Recognition Science cosmology chain. It feeds downstream cosmology models by converting the T0-T8 forcing sequence and RCL into a concrete observable that matches the measured ≈1/4 value, using the eight-tick octave and D=3 spatial dimensions.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)