theorem
proved
tactic proof
C_kernel_eq_two_minus_phi
show as:
view Lean formalization →
formal statement (Lean)
98theorem C_kernel_eq_two_minus_phi : C_kernel = 2 - phi := by
proof body
Tactic-mode proof.
99 unfold C_kernel
100 have h_phi_pos := phi_pos
101 have h_sq : phi ^ 2 = phi + 1 := phi_sq_eq
102 have h_phi_p1_pos : 0 < phi + 1 := by linarith
103 -- Step 1: phi^(-2 : ℝ) = (phi^2)⁻¹ via rpow_neg and rpow_natCast
104 have hpow : phi ^ (-(2 : ℝ)) = (phi ^ (2 : ℕ))⁻¹ := by
105 rw [Real.rpow_neg h_phi_pos.le]
106 congr 1
107 rw [show ((2 : ℝ)) = ((2 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]
108 -- Step 2: (phi^2)⁻¹ = (phi+1)⁻¹ via phi^2 = phi + 1
109 rw [hpow, h_sq]
110 -- Step 3: (phi+1)⁻¹ = 2 - phi via the product identity (phi+1)(2-phi) = 1
111 have key : (phi + 1) * (2 - phi) = 1 := by nlinarith [h_sq]
112 exact inv_eq_of_mul_eq_one_right key
113
114/-- `C` is positive. -/