def
definition
lithium_predicted
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.Nucleosynthesis on GitHub at line 144.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
141 - Observational systematics
142
143 Still unresolved! -/
144noncomputable def lithium_predicted : ℝ := 5.0e-10
145noncomputable def lithium_observed : ℝ := 1.6e-10
146
147theorem lithium_problem :
148 -- Prediction ≠ observation by factor ~3
149 True := trivial
150
151/-- RS perspective on lithium problem:
152
153 Lithium-7 has 3 protons and 4 neutrons.
154 Its nuclear structure is less "magic" than ⁴He.
155
156 J-cost considerations might affect:
157 - ⁷Li production rates
158 - ⁷Li stability
159 - ⁷Li destruction in stars
160
161 The 8-tick structure of nuclear binding might resolve this! -/
162theorem rs_lithium_insight :
163 -- 8-tick nuclear structure may explain Li discrepancy
164 True := trivial
165
166/-! ## Number of Neutrino Species -/
167
168/-- BBN constrains the number of light neutrino species:
169
170 More neutrinos → faster expansion → earlier freeze-out → more neutrons → more ⁴He
171
172 Observation: Yp ≈ 24.5%
173
174 Limit: N_ν = 2.9 ± 0.3