  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 : ℕ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.