cos_pi_5_is_phi_2
plain-language theorem explainer
The identity states that cosine of pi over five equals half the golden ratio. Researchers deriving constants from discrete eight-fold symmetries or linking circular measures to self-similar ratios would cite it. The proof rewrites via the standard cosine evaluation at that angle together with the definition of phi, then reduces the equality algebraically.
Claim. $cos(π/5) = φ/2$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The module develops π from 8-tick geometry, where the circle arises as the continuous limit of eight discrete phases. Phi enters as the self-similar fixed point forced by the Recognition Composition Law and the J-uniqueness condition. The supplied doc-comment lists the exact pentagonal ties: golden angle 2π/φ², interior angle 3π/5, and the two cosine and sine identities that connect the circle directly to φ.
proof idea
One-line wrapper that applies the Mathlib identity for cosine at π/5, substitutes the definition of phi, and finishes with the ring tactic for algebraic simplification.
why it matters
The result supplies the exact geometric bridge between π and φ inside the MATH-002 development. It instantiates the eight-tick octave constraint (T7) and the forced appearance of φ (T6) by exhibiting a concrete pentagonal relation that any 8-tick model must satisfy. The declaration therefore anchors the claim that π emerges from the same discrete symmetry that produces the golden ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.