Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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, π/5, and 2π/5

Example

Writing φ=(1+5)/2, one has cos⁡(π/5)=φ/2,sin⁡(π/10)=(5−1)/4,cos⁡(2π/5)=(5−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θ) and Un(cos⁡θ)sin⁡θ=sin⁡((n+1)θ) for every n∈N, Double-angle and quadratic power-reduction identities, Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}, Signs, monotonicity intervals, and ranges of sine and cosine.

Facts & Assumptions

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

Verification

1.1

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

givenalgebra
2.1

The positive solution is c=(1+5)/4=φ/2. The double-angle identity gives cos⁡(2π/5)=2c2−1=(5−1)/4, and power reduction at π/10 gives sin⁡(π/10)=(1−cos⁡(π/5))/2=(5−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 · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources