sin_pi_10_from_phi
plain-language theorem explainer
The equality sin(π/10) = (phi - 1)/2 holds, with phi the golden ratio. Workers connecting trigonometric identities to the phi-ladder in discrete geometric models reference this step. The proof applies the double-angle cosine identity to reduce to the known algebraic value of cos(π/5), equates the squares, extracts the positive root, and rewrites the result via the definition of phi.
Claim. $sin(π/10) = (φ - 1)/2$, where φ = (1 + √5)/2 denotes the golden ratio.
background
The module Mathematics.Pi develops π from 8-tick geometry: the 8-fold discrete phases of the Recognition Science circle constrain the continuous ratio of circumference to diameter. Phi is the self-similar fixed point forced at T6 of the unified forcing chain. The proof imports the standard identity cos(π/5) = (1 + √5)/4 and the double-angle relation cos(2x) = 1 - 2 sin²(x) from the real-number library.
proof idea
The tactic proof first invokes the double-angle formula to obtain sin²(π/10) = (1 - cos(π/5))/2, substitutes the explicit value of cos(π/5), and verifies the resulting algebraic expressions are identical after clearing denominators. It then proves both sides positive, applies the square-root extraction lemma for positive reals, and finishes with a ring simplification that rewrites the right-hand side in terms of phi.
why it matters
This result supplies the explicit trigonometric link to phi required for the 8-tick derivation of π bounds in the module. It sits alongside the sibling identity cos(π/5) = phi/2 and feeds the octagon-perimeter approximations that close the continuous limit. The step directly instantiates the eight-tick octave (T7) and the emergence of D = 3 spatial dimensions from the same geometric scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.