goldenAngle
open lean source
IndisputableMonolith.Mathematics.Pi on GitHub at line 213.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The golden angle is defined as 2π divided by the square of the golden ratio φ. RS theorists and botanists cite it for phyllotaxis models of leaf placement on stems. The definition is a direct equating of the angle to the 8-tick circle limit without further reduction steps.
Claim. The golden angle is defined by $θ_g = 2π / φ²$ where $φ = (1 + √5)/2$ is the golden ratio, yielding approximately 2.399 radians or 137.5 degrees.
background
The Mathematics.Pi module targets derivation of π from RS 8-tick geometry, in which the circle is discretized into eight phases whose continuous limit fixes the circumference-to-diameter ratio. The golden angle appears as the angular step that arises once φ is forced as the self-similar fixed point of the J-cost function. Upstream constants supply tick as the fundamental time quantum τ₀ = 1 and the eight-tick octave period; PhiForcingDerived supplies the J-cost structure whose fixed point yields φ.
proof idea
This is a one-line definition that directly substitutes the imported constants π and φ into the expression 2 * π / phi^2.
why it matters
The definition embeds the golden angle inside the 8-tick geometric derivation of π (T7 eight-tick octave) and supplies the angular unit used in leaf-arrangement models. It fills the explicit step θ_golden = 2π / φ² stated in the module doc-comment. No downstream theorems are listed, leaving open whether series representations of π can be recovered from the same 8-tick structure.
depends on
formal source
210 ≈ 2.399 rad ≈ 137.5°
211
212 This is the angle between successive leaves on a stem. -/
213noncomputable def goldenAngle : ℝ := 2 * π / phi^2
214
215/-! ## Series Representations -/
216
217/-- π has many series representations:
218
219 1. Leibniz: π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
220 2. Wallis: π/2 = (2/1)(2/3)(4/3)(4/5)(6/5)(6/7)...
221 3. Machin: π/4 = 4 arctan(1/5) - arctan(1/239)
222
223 Can any of these be derived from 8-tick structure? -/
224def piSeries : List String := [
225 "Leibniz: π/4 = Σ (-1)^n/(2n+1)",
226 "Wallis: π/2 = Π (2k)²/((2k-1)(2k+1))",
227 "Machin: π/4 = 4·arctan(1/5) - arctan(1/239)",
228 "Chudnovsky: Fastest known algorithm"
229]
230
231/-- The Leibniz series and 8-tick:
232
233 π/4 = 1 - 1/3 + 1/5 - 1/7 + ...
234
235 8 terms: 1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
236 ≈ 0.7604
237 π/4 ≈ 0.7854
238
239 Error ≈ 3% with 8 terms. The 8-tick gives a natural truncation. -/
240noncomputable def leibniz_8_terms : ℝ :=
241 1 - 1/3 + 1/5 - 1/7 + 1/9 - 1/11 + 1/13 - 1/15
242
243theorem leibniz_8_approximates :