IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Baryon Asymmetry η_B from Phi-Ladder — A3 Baryogenesis
   6
   7RS prediction: η_B ≈ φ^(-44).
   8
   9φ^44 > 10^8 (large number bound).
  10
  11Lean status: 0 sorry, 0 axiom.
  12-/
  13
  14namespace IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder
  15open Constants
  16
  17def baryonRung : ℕ := 44
  18theorem baryonRung_gap45 : baryonRung = 44 := rfl
  19
  20noncomputable def etaB_RS : ℝ := (phi ^ baryonRung)⁻¹
  21
  22theorem etaB_pos : 0 < etaB_RS :=
  23  inv_pos.mpr (pow_pos phi_pos baryonRung)
  24
  25/-- φ^8 = 21φ + 13 > 46. -/
  26theorem phi8_val : phi ^ 8 = 21 * phi + 13 := by
  27  have h2 := phi_sq_eq
  28  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  29  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  30  nlinarith [sq_nonneg (phi^4)]
  31
  32theorem phi8_gt_46 : phi ^ 8 > 46 := by
  33  rw [phi8_val]; linarith [phi_gt_onePointSixOne]
  34
  35/-- φ^16 > 2000. -/
  36theorem phi16_gt_2000 : phi ^ 16 > 2000 := by
  37  have h : phi ^ 16 = (phi ^ 8) ^ 2 := by ring
  38  rw [h]; nlinarith [phi8_gt_46, sq_nonneg (phi^8 - 46)]
  39
  40/-- φ^32 > 4000000. -/
  41theorem phi32_gt_4M : phi ^ 32 > 4000000 := by
  42  have h : phi ^ 32 = (phi ^ 16) ^ 2 := by ring
  43  rw [h]; nlinarith [phi16_gt_2000, sq_nonneg (phi^16 - 2000)]
  44
  45/-- φ^44 > 10^8. -/
  46theorem phi44_gt_1e8 : phi ^ 44 > (10:ℝ)^8 := by
  47  have h12 : phi ^ 12 > 321 := by
  48    have h2 := phi_sq_eq
  49    have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  50    have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  51    have h5 : phi ^ 5 = 5 * phi + 3 := by nlinarith
  52    have h6 : phi ^ 6 = 8 * phi + 5 := by nlinarith
  53    have h8 := phi8_val
  54    have h12v : phi ^ 12 = phi ^ 6 * phi ^ 6 := by ring
  55    rw [h12v]; nlinarith [phi_gt_onePointSixOne]
  56  have h44 : phi ^ 44 = phi ^ 32 * phi ^ 12 := by ring
  57  rw [h44]
  58  norm_num
  59  nlinarith [mul_pos (by linarith [phi32_gt_4M] : (0:ℝ) < phi^32) (by linarith : (0:ℝ) < phi^12),
  60             phi32_gt_4M, h12]
  61
  62/-- η_B < 10^(-8). -/
  63theorem etaB_small : etaB_RS * (10:ℝ)^8 < 1 := by
  64  unfold etaB_RS baryonRung
  65  rw [inv_mul_lt_iff₀ (pow_pos phi_pos 44)]
  66  simp only [mul_one]
  67  exact phi44_gt_1e8
  68
  69structure BaryonAsymmetryCert where
  70  rung : baryonRung = 44
  71  eta_pos : 0 < etaB_RS
  72  phi44_large : phi ^ 44 > (10:ℝ)^8
  73  eta_small : etaB_RS * (10:ℝ)^8 < 1
  74
  75noncomputable def baryonAsymmetryCert : BaryonAsymmetryCert where
  76  rung := baryonRung_gap45
  77  eta_pos := etaB_pos
  78  phi44_large := phi44_gt_1e8
  79  eta_small := etaB_small
  80
  81end IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder
  82