Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact sine and cosine values at π/10\pi/10, π/5\pi/5, and 2π/52\pi/5

Example

Writing φ=(1+5)/2\varphi=(1+\sqrt5)/2, one has cos⁡(π/5)=φ/2,sin⁡(π/10)=(5−1)/4,cos⁡(2π/5)=(5−1)/4,\cos(\pi/5)=\varphi/2,\quad \sin(\pi/10)=(\sqrt5-1)/4,\quad \cos(2\pi/5)=(\sqrt5-1)/4, with the complementary sine values determined by positive square roots. The conventions and prerequisite facts used below are recorded in Tn(cos⁡θ)=cos⁡(nθ)T_n(\cos\theta)=\cos(n\theta) and Un(cos⁡θ)sin⁡θ=sin⁡((n+1)θ)U_n(\cos\theta)\sin\theta=\sin((n+1)\theta) for every n∈Nn\in\mathbb N, Double-angle and quadratic power-reduction identities, Square roots exist: a unique a≥0\sqrt{a} \ge 0 with (a)2=a(\sqrt{a})^2 = a; the positives are {x2:x≠0}\{x^2 : x \neq 0\}, Signs, monotonicity intervals, and ranges of sine and cosine.

Facts & Assumptions

Given: 5(π/5)=π5(\pi/5)=\pi and the sign ranges on the first quadrant.

Verification

1.1

By the defining recurrence for TnT_n, T5(t)=16t5−20t3+5tT_5(t)=16t^5-20t^3+5t. Put c=cos⁡(π/5)c=\cos(\pi/5). The multiple-angle identity gives T5(c)=cos⁡π=−1T_5(c)=\cos\pi=-1; factoring 16c5−20c3+5c+1=(c+1)(4c2−2c−1)216c^5-20c^3+5c+1=(c+1)(4c^2-2c-1)^2 and using 0<c<10<c<1 yields 4c2−2c−1=04c^2-2c-1=0.

givenalgebra
2.1

The positive solution is c=(1+5)/4=φ/2c=(1+\sqrt5)/4=\varphi/2. The double-angle identity gives cos⁡(2π/5)=2c2−1=(5−1)/4\cos(2\pi/5)=2c^2-1=(\sqrt5-1)/4, and power reduction at π/10\pi/10 gives sin⁡(π/10)=(1−cos⁡(π/5))/2=(5−1)/4\sin(\pi/10)=\sqrt{(1-\cos(\pi/5))/2}=(\sqrt5-1)/4. The signs are positive because the angles lie in the first quadrant.

step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources