simplifiedCascadeCost_phi

formal source

  39  rw [phi_sq_eq]
  40  field_simp [hphi1]
  41
  42theorem simplifiedCascadeCost_phi : simplifiedCascadeCost phi = 0 := by
  43  unfold simplifiedCascadeCost
  44  rw [selfSimilarityDefect_phi]
  45  exact Jcost_one
  46
  47theorem selfSimilarityDefect_eq_one_iff {r : ℝ} (hr : 1 < r) :
  48    selfSimilarityDefect r = 1 ↔ r ^ 2 = r + 1 := by
  49  unfold selfSimilarityDefect
  50  have hr1 : r + 1 ≠ 0 := by linarith
  51  constructor
  52  · intro h
  53    field_simp [hr1] at h
  54    linarith
  55  · intro h
  56    rw [h]
  57    field_simp [hr1]
  58
  59theorem positive_root_unique_above_one {r : ℝ} (hr : 1 < r)
  60    (hroot : r ^ 2 = r + 1) : r = phi := by
  61  have hroot0 : r ^ 2 - r - 1 = 0 := by nlinarith [hroot]
  62  have hphi0 : phi ^ 2 - phi - 1 = 0 := by nlinarith [phi_sq_eq]
  63  by_contra hneq
  64  rcases lt_or_gt_of_ne hneq with hlt | hgt
  65  · have hmono : r ^ 2 - r - 1 < phi ^ 2 - phi - 1 := by
  66      nlinarith [hr, one_lt_phi, hlt]
  67    nlinarith
  68  · have hmono : phi ^ 2 - phi - 1 < r ^ 2 - r - 1 := by
  69      nlinarith [hr, one_lt_phi, hgt]
  70    nlinarith
  71
  72theorem simplifiedCascadeCost_eq_zero_iff {r : ℝ} (hr : 1 < r) :