phi_unique_positive

formal source

  55/-! ## Uniqueness of φ -/
  56
  57/-- **THEOREM**: φ is the unique positive solution to r² = r + 1. -/
  58theorem phi_unique_positive : ∀ r : ℝ, r > 0 → IsSelfSimilar r → r = φ := by
  59  intro r hr h_self
  60  unfold IsSelfSimilar at h_self
  61  -- Both r and φ satisfy x² = x + 1
  62  have h_phi_ss := phi_is_self_similar
  63  unfold IsSelfSimilar at h_phi_ss
  64  -- From r² = r + 1 and φ² = φ + 1, we get r² - φ² = r - φ
  65  have h_diff_sq : r^2 - φ^2 = r - φ := by linarith
  66  -- (r - φ)(r + φ) = r² - φ² = r - φ
  67  have h_factor : (r - φ) * (r + φ) = r - φ := by nlinarith [sq_nonneg r, sq_nonneg φ]
  68  -- So (r - φ)(r + φ - 1) = 0
  69  have h_zero : (r - φ) * (r + φ - 1) = 0 := by nlinarith
  70  -- By zero product property
  71  rcases mul_eq_zero.mp h_zero with h_case | h_case
  72  · -- Case: r - φ = 0, so r = φ
  73    linarith
  74  · -- Case: r + φ - 1 = 0, so r = 1 - φ
  75    -- But φ > 1, so 1 - φ < 0, contradicting r > 0
  76    have h_r_eq : r = 1 - φ := by linarith
  77    have h_phi_gt_one := phi_gt_one
  78    linarith
  79
  80/-! ## The φ-Ladder -/
  81
  82/-- The φ-ladder: all stable positions are φ^n for integer n. -/
  83def PhiLadder : Set ℝ := { x | ∃ n : ℤ, x = φ^n }
  84
  85/-- φ^n is always positive for any integer n -/
  86theorem phi_pow_pos (n : ℤ) : φ^n > 0 := by
  87  exact zpow_pos phi_pos n
  88