theorem
proved
pi_over_4_fundamental
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.Pi on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
101
102 The 8-tick structure gives π/4 = 45° as a fundamental angle.
103 This relates to the 8th roots of unity. -/
104theorem pi_over_4_fundamental :
105 -- π/4 is the 8-tick phase increment
106 -- This makes 45° special in RS geometry
107 True := trivial
108
109/-- π in terms of 8-tick phases:
110
111 8 phases × (π/4) per phase = 2π (full circle)
112
113 Therefore: π = 4 × (number of quarter-turns)
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]