selfSimilarityDefect_phi

formal source

  33  unfold selfSimilarityDefect
  34  positivity
  35
  36theorem selfSimilarityDefect_phi : selfSimilarityDefect phi = 1 := by
  37  unfold selfSimilarityDefect
  38  have hphi1 : phi + 1 ≠ 0 := by linarith [phi_pos]
  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]