frequencyRatioCost_unit

formal source

  33noncomputable def frequencyRatioCost (r : ℝ) : ℝ := Jcost r
  34
  35/-- J-cost of unit ratio is zero: equal frequencies have no cost. -/
  36theorem frequencyRatioCost_unit : frequencyRatioCost 1 = 0 := by
  37  unfold frequencyRatioCost Jcost; simp
  38
  39/-- J-cost is non-negative for positive ratios. -/
  40theorem frequencyRatioCost_nonneg {r : ℝ} (hr : 0 < r) :
  41    0 ≤ frequencyRatioCost r :=
  42  Jcost_nonneg hr
  43
  44/-! ## φ as Minimal-Cost Non-Trivial Ratio -/
  45
  46/-- A self-similar ratio satisfies r² = r + 1 (the defining equation of φ). -/
  47def IsSelfSimilarRatio (r : ℝ) : Prop := r ^ 2 = r + 1
  48
  49/-- φ is a self-similar ratio. -/
  50theorem phi_is_self_similar : IsSelfSimilarRatio phi := phi_sq_eq
  51
  52/-- φ is the UNIQUE positive self-similar ratio.
  53    Proof: r² = r + 1 and φ² = φ + 1 give (r−φ)(r+φ) = r−φ,
  54    so (r−φ)(r+φ−1) = 0. Since r > 0 and φ > 1, r+φ−1 > 0,
  55    so r = φ. -/
  56theorem phi_unique_self_similar {r : ℝ} (hr_pos : 0 < r)
  57    (hr_ss : IsSelfSimilarRatio r) : r = phi := by
  58  unfold IsSelfSimilarRatio at hr_ss
  59  have hphi_sq := phi_sq_eq
  60  have hphi_pos := phi_pos
  61  have hphi_gt1 := one_lt_phi
  62  have hdiff : (r - phi) * (r + phi - 1) = 0 := by nlinarith
  63  rcases mul_eq_zero.mp hdiff with h | h
  64  · linarith
  65  · exfalso; nlinarith
  66