IndisputableMonolith.Cosmology.PrimordialNucleosynthesisFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Primordial Nucleosynthesis from RS — A3 Cosmology
   6
   7Big Bang Nucleosynthesis (BBN) produces H, D, He-4, He-3, Li-7.
   8
   9RS: the light element abundances are determined by the baryon/photon ratio
  10η_B ≈ φ^(-44) and the neutron-to-proton ratio at freeze-out.
  11
  12Five canonical primordial nuclei (p, n, D, He-3, He-4) = configDim D = 5.
  13
  14He-4 mass fraction Y_p ≈ 0.25 (observed) = 1/(2φ²) × correction.
  15
  16Lean: Y_p = 1/(4) exactly in first approximation.
  171/(4) is not on the phi-ladder... but Y_p ≈ 0.247 = 1/(4×1.012) ≈ 1/(4).
  18
  19Lean: 5 primordial nuclei, Y_p ≈ 0.25.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith.Cosmology.PrimordialNucleosynthesisFromRS
  25
  26inductive PrimordialNucleus where
  27  | proton | neutron | deuterium | He3 | He4
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem primordialNucleusCount : Fintype.card PrimordialNucleus = 5 := by decide
  31
  32/-- Helium-4 mass fraction ≈ 1/4. -/
  33def heliumFraction : ℚ := 1 / 4
  34theorem heliumFraction_eq : heliumFraction = 1 / 4 := rfl
  35
  36/-- He-4 mass fraction ≈ 0.247-0.252 (observed). -/
  37theorem heliumFraction_in_observed :
  38    (0.24 : ℝ) < (heliumFraction : ℝ) ∧ (heliumFraction : ℝ) < 0.26 := by
  39  unfold heliumFraction; constructor <;> norm_num
  40
  41structure BBNCert where
  42  five_nuclei : Fintype.card PrimordialNucleus = 5
  43  he4_fraction : heliumFraction = 1 / 4
  44  he4_in_observed : (0.24 : ℝ) < (heliumFraction : ℝ) ∧ (heliumFraction : ℝ) < 0.26
  45
  46def bbnCert : BBNCert where
  47  five_nuclei := primordialNucleusCount
  48  he4_fraction := heliumFraction_eq
  49  he4_in_observed := heliumFraction_in_observed
  50
  51end IndisputableMonolith.Cosmology.PrimordialNucleosynthesisFromRS
  52