rs_lithium_insight
plain-language theorem explainer
The declaration asserts that the eight-tick nuclear structure may explain the lithium-7 discrepancy in Big Bang nucleosynthesis. Cosmologists working within Recognition Science would cite it when discussing BBN anomalies. The proof is a one-line term-mode application of trivial that registers the insight as holding.
Claim. In Recognition Science the eight-tick nuclear binding structure may resolve the observed discrepancy between predicted and measured lithium-7 abundance in Big Bang nucleosynthesis.
background
The Cosmology.Nucleosynthesis module derives light-element abundances from RS principles under COS-012. It records observed values including ⁴He mass fraction ~24-25%, D/H ~2.5×10^{-5}, and ⁷Li/H ~1.6×10^{-10} (the lithium problem). RS supplies η ~ 10^{-10} from φ and nuclear magic numbers from the eight-tick structure. Upstream, Constants.tick supplies the fundamental time quantum τ₀ = 1 with one octave = 8 ticks; NucleosynthesisTiers.of supplies the structure of nuclear densities in discrete φ-tiers; PhiForcingDerived.of supplies the structure of J-cost.
proof idea
The proof is a term-mode one-line wrapper that applies trivial to the proposition True.
why it matters
The declaration places the eight-tick octave (T7 of the forcing chain) inside BBN, linking it to the lithium problem noted in the module doc-comment. It sits among sibling results on helium, deuterium, and eta but has no direct used_by edges. It touches the open question of whether J-cost adjustments can quantitatively close the lithium gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.