theorem
proved
tactic proof
phi_unique_positive
show as:
view Lean formalization →
formal statement (Lean)
58theorem phi_unique_positive : ∀ r : ℝ, r > 0 → IsSelfSimilar r → r = φ := by
proof body
Tactic-mode proof.
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. -/