cos_pi_5_is_phi_2

formal source

 127    4. **sin(π/10) = (φ-1)/2 = 1/(2φ)** (exact!)
 128
 129    These connect the circle (π) to the golden ratio (φ). -/
 130theorem cos_pi_5_is_phi_2 :
 131    Real.cos (π / 5) = phi / 2 := by
 132  -- cos(π/5) = (1 + √5)/4 (Mathlib)
 133  -- φ = (1 + √5)/2, so φ/2 = (1 + √5)/4
 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