IndisputableMonolith.Cosmology.BaryogenesisTrajectory

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Baryogenesis Dynamic Trajectory: η_B(t) on the Phi-Ladder
   6
   7The matter-consciousness duality (`Cosmology/MatterConsciousnessDualityTheorem`)
   8proves the equilibrium identity `η_B · Θ_crit = φ`, fixing the present
   9baryon-to-photon ratio at `η_B = φ⁻⁴⁴`. This module adds the dynamic
  10content: η_B falls from its GUT-scale unity value through the
  11electroweak transition by integer φ-step decrements per recognition
  12e-fold.
  13
  14The structural prediction: every e-fold of cosmic Z-aging drops the
  15log-η_B by exactly `log φ`, giving the trajectory
  16`η_B(N) = exp(-N · log φ)` where `N` is the number of recognition
  17e-folds since the GUT epoch. The 44-rung gap from rung 0 (GUT, η_B = 1)
  18to rung -44 (present, η_B = φ⁻⁴⁴) is the same gap-(consciousnessGap-1)
  19that sets the inflation e-fold count `N_e = 44`.
  20
  21Lean status: 0 sorry, 0 axiom.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Cosmology
  26namespace BaryogenesisTrajectory
  27
  28open Constants
  29
  30noncomputable section
  31
  32/-- η_B value at recognition e-fold `N` since the GUT epoch. -/
  33def etaBAt (N : ℕ) : ℝ := phi ^ (-(N : ℤ))
  34
  35/-- η_B is strictly positive at every e-fold. -/
  36theorem etaBAt_pos (N : ℕ) : 0 < etaBAt N := by
  37  unfold etaBAt
  38  exact zpow_pos Constants.phi_pos _
  39
  40/-- GUT-scale initial value: η_B(0) = 1. -/
  41theorem etaBAt_zero : etaBAt 0 = 1 := by
  42  unfold etaBAt
  43  simp
  44
  45/-- One e-fold cuts η_B by exactly 1/φ. -/
  46theorem etaBAt_succ_ratio (N : ℕ) :
  47    etaBAt (N + 1) = etaBAt N * phi⁻¹ := by
  48  unfold etaBAt
  49  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  50  have hzpow : phi ^ (-((N : ℤ) + 1)) = phi ^ (-(N : ℤ)) * phi⁻¹ := by
  51    rw [show (-((N : ℤ) + 1)) = -(N : ℤ) + (-1 : ℤ) by ring]
  52    rw [zpow_add₀ hphi_ne]
  53    simp
  54  have hcast : ((N + 1 : ℕ) : ℤ) = (N : ℤ) + 1 := by push_cast; ring
  55  rw [hcast, hzpow]
  56
  57/-- η_B is strictly monotone-decreasing in e-fold count. -/
  58theorem etaBAt_strictly_decreasing (N : ℕ) :
  59    etaBAt (N + 1) < etaBAt N := by
  60  rw [etaBAt_succ_ratio]
  61  have hk : 0 < etaBAt N := etaBAt_pos N
  62  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  63    have hphi_gt_one : (1 : ℝ) < phi := by
  64      have := Constants.phi_gt_onePointFive; linarith
  65    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  66  have : etaBAt N * phi⁻¹ < etaBAt N * 1 :=
  67    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  68  simpa using this
  69
  70/-- Adjacent-e-fold ratio is exactly 1/φ. -/
  71theorem etaBAt_adjacent_ratio (N : ℕ) :
  72    etaBAt (N + 1) / etaBAt N = phi⁻¹ := by
  73  rw [etaBAt_succ_ratio]
  74  have hpos : 0 < etaBAt N := etaBAt_pos N
  75  field_simp [hpos.ne']
  76
  77/-- η_B falls below the empirical band (≈ 6 × 10⁻¹⁰) after a finite
  78e-fold count: `etaBAt 44 = phi^(-44)` matches the existing equilibrium
  79identity at the present epoch. -/
  80theorem etaBAt_44 : etaBAt 44 = phi ^ (-(44 : ℤ)) := by
  81  unfold etaBAt
  82  norm_cast
  83
  84structure BaryogenesisTrajectoryCert where
  85  eta_pos : ∀ N, 0 < etaBAt N
  86  initial_unity : etaBAt 0 = 1
  87  one_step_ratio : ∀ N, etaBAt (N + 1) = etaBAt N * phi⁻¹
  88  strictly_decreasing : ∀ N, etaBAt (N + 1) < etaBAt N
  89  adjacent_ratio_eq_inv_phi :
  90    ∀ N, etaBAt (N + 1) / etaBAt N = phi⁻¹
  91  present_value : etaBAt 44 = phi ^ (-(44 : ℤ))
  92
  93/-- Baryogenesis trajectory certificate. -/
  94def baryogenesisTrajectoryCert : BaryogenesisTrajectoryCert where
  95  eta_pos := etaBAt_pos
  96  initial_unity := etaBAt_zero
  97  one_step_ratio := etaBAt_succ_ratio
  98  strictly_decreasing := etaBAt_strictly_decreasing
  99  adjacent_ratio_eq_inv_phi := etaBAt_adjacent_ratio
 100  present_value := etaBAt_44
 101
 102end
 103end BaryogenesisTrajectory
 104end Cosmology
 105end IndisputableMonolith
 106