cycleDuration

formal source

  21namespace IndisputableMonolith.Economics.BusinessCycleFromPhiLadder
  22open Constants
  23
  24noncomputable def cycleDuration (k : ℕ) : ℝ := 4 * phi ^ (2 * k)
  25
  26theorem cycleDuration_pos (k : ℕ) : 0 < cycleDuration k := by
  27  unfold cycleDuration; exact mul_pos (by norm_num) (pow_pos phi_pos _)
  28
  29theorem cycleDuration_succ_ratio (k : ℕ) :
  30    cycleDuration (k + 1) / cycleDuration k = phi ^ 2 := by
  31  unfold cycleDuration
  32  have hphi_ne := phi_ne_zero
  33  have hphi_pos := phi_pos
  34  have h4phi : (4 * phi ^ (2 * k)) ≠ 0 := by
  35    exact (mul_pos (by norm_num) (pow_pos phi_pos _)).ne'
  36  rw [div_eq_iff h4phi]
  37  ring
  38
  39structure BusinessCycleCert where
  40  duration_pos : ∀ k, 0 < cycleDuration k
  41  phi_sq_ratio : ∀ k, cycleDuration (k + 1) / cycleDuration k = phi ^ 2
  42
  43noncomputable def businessCycleCert : BusinessCycleCert where
  44  duration_pos := cycleDuration_pos
  45  phi_sq_ratio := cycleDuration_succ_ratio
  46
  47end IndisputableMonolith.Economics.BusinessCycleFromPhiLadder