one_sub_phi_inv_eq_phi_inv_sq

formal source

  47  nlinarith
  48
  49/-- `1 - 1/φ = 1/φ²`, the golden complement relation. -/
  50theorem one_sub_phi_inv_eq_phi_inv_sq : 1 - phi⁻¹ = phi⁻¹ ^ 2 := by
  51  have hphi : phi ≠ 0 := phi_ne_zero
  52  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  53  field_simp [hphi]
  54  nlinarith [sq_pos_of_pos phi_pos, hphi_sq]
  55
  56/-- The two band boundaries sum to one. -/
  57theorem bandBoundaries_sum_to_one : rhoBandLower + rhoBandUpper = 1 := by
  58  unfold rhoBandLower rhoBandUpper
  59  have hphi : phi ≠ 0 := phi_ne_zero
  60  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
  61  field_simp [hphi]
  62  nlinarith [sq_pos_of_pos phi_pos, hphi_sq]
  63
  64theorem one_sub_rhoBandLower_eq_rhoBandUpper : 1 - rhoBandLower = rhoBandUpper := by
  65  linarith [bandBoundaries_sum_to_one]
  66
  67theorem one_sub_rhoBandUpper_eq_rhoBandLower : 1 - rhoBandUpper = rhoBandLower := by
  68  linarith [bandBoundaries_sum_to_one]
  69
  70/-- At the lower boundary, `ρ/(1-ρ) = 1/φ`. -/
  71theorem bandLower_ratio : rhoBandLower / (1 - rhoBandLower) = phi⁻¹ := by
  72  rw [one_sub_rhoBandLower_eq_rhoBandUpper]
  73  unfold rhoBandLower rhoBandUpper
  74  field_simp [phi_ne_zero]
  75
  76/-- At the upper boundary, `ρ/(1-ρ) = φ`. -/
  77theorem bandUpper_ratio : rhoBandUpper / (1 - rhoBandUpper) = phi := by
  78  rw [one_sub_rhoBandUpper_eq_rhoBandLower]
  79  unfold rhoBandLower rhoBandUpper
  80  field_simp [phi_ne_zero]