pith. machine review for the scientific record. sign in
def definition def or abbrev high

lithium_observed

show as:
view Lean formalization →

The declaration supplies the numerical value for the observed primordial lithium-7 abundance in Recognition Science nucleosynthesis models. Cosmologists and RS theorists cite it when quantifying the lithium discrepancy against predicted ratios derived from phi-constrained eta. The definition consists of a direct numerical assignment with no derivation or lemmas.

claimThe observed primordial lithium-7 to hydrogen ratio equals $1.6 times 10^{-10}$.

background

The Cosmology.Nucleosynthesis module derives light-element abundances from RS principles, including the baryon-to-photon ratio eta obtained from phi and nuclear reaction rates fixed by the eight-tick structure. Observed values are listed for helium-4 mass fraction, deuterium ratio, helium-3 ratio, and lithium-7 ratio to permit direct comparison with RS predictions. The module documentation explicitly flags the lithium-7 entry as the site of the lithium problem.

proof idea

The definition is a direct numerical constant assignment with no lemmas applied and no tactics required.

why it matters in Recognition Science

This constant anchors comparisons between RS-predicted lithium abundances and empirical data inside the BBN framework of the module. It directly supports the lithium_problem sibling declaration by providing the benchmark value that RS mechanisms must address through phi-derived parameters. The entry closes the loop from T5 J-uniqueness and T6 phi fixed point to observable cosmology.

scope and limits

formal statement (Lean)

 145noncomputable def lithium_observed : ℝ := 1.6e-10

proof body

Definition body.

 146