goldenAngle
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.