sin_pi_10_from_phi

proof body

Tactic-mode proof.

 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
 168    have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
 169    have hsqrt_sq : (Real.sqrt 5)^2 = 5 := Real.sq_sqrt h5_pos
 170    -- Expand right side: ((√5 - 1)/4)²
 171    ring_nf
 172    -- Now: (3 - √5)/8 = (6 - 2√5)/16
 173    -- Multiply both sides by 16: 2(3 - √5) = 6 - 2√5
 174    -- Left: 6 - 2√5, Right: 6 - 2√5 ✓
 175    field_simp
 176    ring
 177    rw [hsqrt_sq]
 178    ring
 179  -- Since sin(π/10) > 0 and ((√5 - 1)/4) > 0, we can take square roots
 180  have h_pos : 0 < Real.sin (π / 10) := Real.sin_pos_of_pos_of_lt_pi (div_pos Real.pi_pos (by norm_num : (0 : ℝ) < 10)) (div_lt_self Real.pi_pos (by norm_num : (1 : ℝ) < 10))
 181  have h_rhs_pos : 0 < (Real.sqrt 5 - 1) / 4 := by
 182    have hsqrt5_gt1 : 1 < Real.sqrt 5 := by
 183      have h : (1 : ℝ)^2 < (5 : ℝ) := by norm_num
 184      have h1_pos : (0 : ℝ) ≤ 1 := by norm_num
 185      have h1_sq : Real.sqrt ((1 : ℝ)^2) = 1 := Real.sqrt_sq h1_pos
 186      rw [← h1_sq]
 187      exact Real.sqrt_lt_sqrt (by norm_num) h
 188    linarith
 189  -- sin(π/10) = (√5 - 1)/4
 190  -- Since both sides are positive and their squares are equal, they are equal
 191  have h_eq : Real.sin (π / 10) = (Real.sqrt 5 - 1) / 4 := by
 192    -- Use: if a² = b², then a = b or a = -b
 193    have h_or : Real.sin (π / 10) = (Real.sqrt 5 - 1) / 4 ∨ Real.sin (π / 10) = -((Real.sqrt 5 - 1) / 4) := by
 194      rw [← sq_eq_sq_iff_eq_or_eq_neg]
 195      exact h_sq_eq
 196    cases h_or with
 197    | inl h => exact h
 198    | inr h =>
 199      -- If sin(π/10) = -((√5 - 1)/4), this contradicts h_pos since -((√5 - 1)/4) < 0
 200      linarith [h_pos, h, h_rhs_pos]
 201  -- Now show (√5 - 1)/4 = (φ - 1)/2
 202  rw [h_eq, phi]
 203  -- φ = (1 + √5)/2, so φ - 1 = (1 + √5)/2 - 1 = (√5 - 1)/2
 204  -- Therefore (φ - 1)/2 = (√5 - 1)/4 ✓
 205  ring
 206
 207/-- The golden angle in radians:
 208
 209    θ_golden = 2π / φ² = 2π(1 - 1/φ) = 2π(φ-1)/φ
 210             ≈ 2.399 rad ≈ 137.5°
 211
 212    This is the angle between successive leaves on a stem. -/