Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21
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.

Finite sums of the sine harmonics

Statement

Let N be a positive integer. If x2πZ, then

n=1Nsin(nx)=cos(x/2)cos((N+1/2)x)2sin(x/2).

If x2πZ, then for every positive integer N, n=1Nsin(nx)1/sin(x/2).

If x2πZ, every summand is zero and the sum is zero.

Facts & Assumptions

Given: A real x and a positive integer N.

[L1]
[L2]

The sine and cosine addition formulas hold for all real arguments (The addition formulas for sine and cosine).

[L3]

sint=0 exactly at the integer multiples of π, and sine and cosine have period 2π (The zero sets of sine and cosine and the least positive common period 2 pi).

[L5]

Finite sums start with the empty sum and satisfy the recursive addition law (Finite sums and finite products, by recursion).

[L6]

For every real t, cost1 (Parity and the Pythagorean identity for sine and cosine).

[L7]

For all complex z,w, exp(z+w)=expzexpw (exp(z+w)=expzexpw, and the complex exponential extends the real exponential).

Proof

technique · cases
1.1

For the nonperiodic case, assume x2πZ and define the auxiliary complex sums recursively by S0=0 and Sj+1=Sj+ei(j+1)x. Multiplication by 1eix and the exponential addition law [L7] telescope directly to (1eix)SN=eixei(N+1)x. The half-angle identity 1eix=2ieix/2sin(x/2) and [L3] show that the multiplier is nonzero.

assume-case nonperiodicL1L2L3L7algebra
1.2

For the periodic case, assume x2πZ. Then every nx is a multiple of 2π, so sin(nx)=0 by [L3] and the finite sine sum is zero.

assume-case periodicL3L5
2.1

For the nonperiodic case, divide the identity in step 1.1 by its nonzero multiplier and use [L1] and [L2] to obtain SN=ei(N+1)x/2sin(Nx/2)sin(x/2).

step 1.1L1L2algebra
3.1

For the nonperiodic case, take imaginary parts in step 2.1 and apply the product-to-sum consequence of [L2] to get n=1Nsin(nx)=cos(x/2)cos((N+1/2)x)2sin(x/2).

step 2.1L1L2algebra
4.1

For the nonperiodic case, [L6] bounds the numerator in step 3.1 by 2, so the absolute value of the sum is at most 1/sin(x/2).

step 3.1L4L6algebra
5.1

The nonperiodic branch gives the displayed formula and bound by steps 3.1 and 4.1, while the periodic branch gives the separate zero value by step 1.2; the two cases exhaust all real x.

step 1.2step 3.1step 4.1cases-exhaustive

Depends on

Used by

Dependency tree · two levels

43 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