sin_pi_10_from_phi

formal source

 134  rw [Real.cos_pi_div_five, phi]
 135  ring
 136
 137theorem sin_pi_10_from_phi :
 138    Real.sin (π / 10) = (phi - 1) / 2 := by
 139  -- Use double-angle formula: cos(π/5) = 1 - 2sin²(π/10)
 140  -- So sin²(π/10) = (1 - cos(π/5))/2
 141  have h_cos : Real.cos (π / 5) = (1 + Real.sqrt 5) / 4 := Real.cos_pi_div_five
 142  -- First prove sin²(π/10) = (1 - cos(π/5))/2
 143  have h_sin_sq : Real.sin (π / 10)^2 = (1 - Real.cos (π / 5)) / 2 := by
 144    -- Use: cos(2θ) = 1 - 2sin²(θ), so sin²(θ) = (1 - cos(2θ))/2
 145    -- With θ = π/10, 2θ = π/5
 146    -- We have cos(π/5) = cos(2·(π/10)) = 1 - 2sin²(π/10)
 147    have h_cos_double : Real.cos (π / 5) = Real.cos (2 * (π / 10)) := by ring
 148    rw [h_cos_double]
 149    -- cos(2x) = 1 - 2sin²(x)
 150    have h_cos_formula : Real.cos (2 * (π / 10)) = 1 - 2 * Real.sin (π / 10)^2 := by
 151      -- cos(2x) = 2cos²(x) - 1, but we need 1 - 2sin²(x)
 152      -- Use Pythagorean: cos²(x) + sin²(x) = 1, so cos²(x) = 1 - sin²(x)
 153      -- Therefore: cos(2x) = 2(1 - sin²(x)) - 1 = 2 - 2sin²(x) - 1 = 1 - 2sin²(x)
 154      rw [Real.cos_two_mul]
 155      have h_pythag : Real.cos (π / 10)^2 + Real.sin (π / 10)^2 = 1 := Real.cos_sq_add_sin_sq (π / 10)
 156      have h_cos_sq : Real.cos (π / 10)^2 = 1 - Real.sin (π / 10)^2 := by linarith [h_pythag]
 157      rw [h_cos_sq]
 158      ring
 159    rw [h_cos_formula]
 160    -- Rearrange: 2sin²(π/10) = 1 - cos(π/5), so sin²(π/10) = (1 - cos(π/5))/2
 161    ring
 162  -- Now show sin²(π/10) = ((√5 - 1)/4)²
 163  have h_sq_eq : Real.sin (π / 10)^2 = ((Real.sqrt 5 - 1) / 4)^2 := by
 164    rw [h_sin_sq, h_cos]
 165    field_simp
 166    -- Left: (1 - (1 + √5)/4)/2 = (4 - 1 - √5)/(8) = (3 - √5)/8
 167    -- Right: ((√5 - 1)/4)² = (5 - 2√5 + 1)/16 = (6 - 2√5)/16 = (3 - √5)/8