pi_from_eight_quarters

formal source

 114
 115    This is almost tautological, but it shows π is
 116    "4 times the quarter-circle angle." -/
 117theorem pi_from_eight_quarters :
 118    8 * (π / 4) = 2 * π := by ring
 119
 120/-! ## π and φ Relationship -/
 121
 122/-- π and φ are related through geometry:
 123
 124    1. **Golden angle**: 2π/φ² ≈ 137.5° (phyllotaxis)
 125    2. **Pentagon**: Interior angle = 108° = 3π/5
 126    3. **cos(π/5) = φ/2** (exact!)
 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