theorem
proved
lithium_problem
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.Nucleosynthesis on GitHub at line 147.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
175
176 Matches the known 3 neutrino species! -/
177noncomputable def neutrino_species_from_bbn : ℝ := 2.9