etaBAt_adjacent_ratio

formal source

  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