theorem
proved
tactic proof
phi_fixed_point
show as:
view Lean formalization →
formal statement (Lean)
40theorem phi_fixed_point : Constants.phi = 1 + 1 / Constants.phi := by
proof body
Tactic-mode proof.
41 have h_sq : Constants.phi ^ 2 = Constants.phi + 1 := phi_squared
42 have h_ne_zero : Constants.phi ≠ 0 := phi_ne_zero
43 calc
44 Constants.phi = (Constants.phi ^ 2) / Constants.phi := by
45 rw [pow_two, mul_div_cancel_left₀ _ h_ne_zero]
46 _ = (Constants.phi + 1) / Constants.phi := by rw [h_sq]
47 _ = Constants.phi / Constants.phi + 1 / Constants.phi := by rw [add_div]
48 _ = 1 + 1 / Constants.phi := by
49 have : Constants.phi / Constants.phi = 1 := div_self h_ne_zero
50 rw [this]
51
52/-- Uniqueness: if x > 0 and x² = x + 1, then x = φ. -/
53 theorem phi_unique_pos_root (x : ℝ) : (x ^ 2 = x + 1 ∧ 0 < x) ↔ x = Constants.phi := by
54 constructor
55 · intro hx
56 have hx2 : x ^ 2 = x + 1 := hx.left
57 -- (2x−1)^2 = 5
58 have hquad : (2 * x - 1) ^ 2 = 5 := by
59 calc
60 (2 * x - 1) ^ 2 = 4 * x ^ 2 - 4 * x + 1 := by ring
61 _ = 4 * (x + 1) - 4 * x + 1 := by simpa [hx2]
62 _ = 5 := by ring
63 -- From x>0 and x(x−1)=1, get x>1 hence 2x−1>0
64 have hx_nonzero : x ≠ 0 := ne_of_gt hx.right
65 have hx_sub : x ^ 2 - x = 1 := by
66 have := congrArg (fun t => t - x) hx.left
67 simpa [sub_eq_add_neg] using this
68 have hx_mul : x * (x - 1) = 1 := by
69 have hfac : x ^ 2 - x = x * (x - 1) := by ring
70 simpa [hfac] using hx_sub
71 have hx1_pos : 0 < x - 1 := by
72 -- divide by positive x
73 have := congrArg (fun t : ℝ => t / x) hx_mul
74 have hdiv : x - 1 = 1 / x := by
75 simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, hx_nonzero] using this
76 simpa [hdiv] using (one_div_pos.mpr hx.right)
77 have hx_pos : 0 < 2 * x - 1 := by linarith
78 -- Take square root
79 have hsqroot : Real.sqrt ((2 * x - 1) ^ 2) = Real.sqrt 5 := by
80 simpa [hquad]
81 have hsqabs : Real.sqrt ((2 * x - 1) ^ 2) = |2 * x - 1| := by
82 exact Real.sqrt_sq_eq_abs (2 * x - 1)
83 have habs : |2 * x - 1| = Real.sqrt 5 := by
84 -- rewrite the left side of hsqroot via sqrt(sq)=|·|
85 simpa [hsqabs] using hsqroot
86 have hlin : 2 * x - 1 = Real.sqrt 5 := by
87 have hnonneg : 0 ≤ 2 * x - 1 := le_of_lt hx_pos
88 have hdrop : |2 * x - 1| = 2 * x - 1 := abs_of_nonneg hnonneg
89 simpa [hdrop] using habs
90 have h2x : 2 * x = 1 + Real.sqrt 5 := by linarith
91 have hx_eq : x = (1 + Real.sqrt 5) / 2 := by
92 have h2 : (2 : ℝ) ≠ 0 := by norm_num
93 -- x = (1+√5)/2 ↔ 2*x = 1+√5
94 exact (eq_div_iff_mul_eq h2).2 (by simpa [mul_comm] using h2x)
95 simpa [Constants.phi] using hx_eq
96 · intro hx; subst hx
97 exact And.intro phi_squared (lt_trans (by norm_num) one_lt_phi)
98
99/-- **Phase 3 Derivation**: Model-independent exclusivity of φ.
100 The golden ratio is the unique positive solution to the self-similarity constraint. -/