pith. sign in
module module moderate

IndisputableMonolith.Cosmology.PrimordialNucleosynthesisFromRS

show as:
view Lean formalization →

The module derives the helium-4 mass fraction of approximately one quarter as a direct consequence of the Recognition Science constants and forcing chain. Cosmologists testing early-universe predictions against observed abundances would cite these results. The derivations compose the J-cost function with the phi-ladder mass assignments and the eight-tick octave to fix the baryon density that yields the standard 25 percent helium fraction.

claim$Y_{^4He} = 1/4$ follows from the RS time quantum $τ_0 = 1$ tick together with the self-similar fixed point $ϕ$ and the Recognition Composition Law applied to the primordial baryon-to-photon ratio.

background

The module resides in the cosmology domain and imports the RS time quantum $τ_0 = 1$ tick from Constants. It introduces PrimordialNucleus as the basic objects, primordialNucleusCount for their abundances, and heliumFraction together with its equality theorem. The local setting is the early universe whose expansion and mass assignments are governed by the phi-ladder and the eight-tick period fixed by the forcing chain T7-T8.

proof idea

This module organizes definitions for nuclei and counts followed by equality theorems; the heliumFraction_eq and heliumFraction_in_observed results reduce the fraction via the J-uniqueness property and the phi-ladder mass formula already established upstream.

why it matters in Recognition Science

The module supplies the BBNCert certification that links RS constants to observed light-element abundances. It thereby supports the claim that the framework reproduces standard BBN outcomes from the single functional equation without extra parameters. It touches the T8 step that fixes D = 3 spatial dimensions and therefore the early-universe expansion rate.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)