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 be a positive integer. If , then
If , then for every positive integer , .
If , every summand is zero and the sum is zero.
Facts & Assumptions
Given: A real and a positive integer .
For real , and (, , and ).
The sine and cosine addition formulas hold for all real arguments (The addition formulas for sine and cosine).
exactly at the integer multiples of , and sine and cosine have period (The zero sets of sine and cosine and the least positive common period 2 pi).
Complex modulus is multiplicative and satisfies the triangle inequality (Conjugation is an involutive real-field automorphism, , and modulus is definite, multiplicative, and subadditive).
Finite sums start with the empty sum and satisfy the recursive addition law (Finite sums and finite products, by recursion).
For every real , (Parity and the Pythagorean identity for sine and cosine).
For all complex , (, and the complex exponential extends the real exponential).
Proof
For the nonperiodic case, assume and define the auxiliary complex sums recursively by and . Multiplication by and the exponential addition law [L7] telescope directly to . The half-angle identity and [L3] show that the multiplier is nonzero.
For the periodic case, assume . Then every is a multiple of , so by [L3] and the finite sine sum is zero.
For the nonperiodic case, divide the identity in step 1.1 by its nonzero multiplier and use [L1] and [L2] to obtain
For the nonperiodic case, take imaginary parts in step 2.1 and apply the product-to-sum consequence of [L2] to get
For the nonperiodic case, [L6] bounds the numerator in step 3.1 by , so the absolute value of the sum is at most .
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 .
Depends on
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- $\exp(z+w)=\exp z\,\exp w$, and the complex exponential extends the real exponential
- Finite sums and finite products, by recursion
- The addition formulas for sine and cosine
- The zero sets of sine and cosine and the least positive common period 2 pi
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
- Parity and the Pythagorean identity for sine and cosine
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
- Jiří Lebl, Basic Analysis II, §11.8.4 (standard reference, not scraped)