LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Weighted cosine orthogonality on the Lobatto grid

Statement

For $n \in N$ with $n \geq 1$ and $k, ℓ \in N$ with $0 \leq k, ℓ \leq n$ , define $S_{k ℓ} : = \frac{1}{2} \cos (0) + \sum_{j = 1}^{n - 1} \cos ⁣ (\frac{j k π}{n}) \cos ⁣ (\frac{j ℓ π}{n}) + \frac{1}{2} (- 1)^{k + ℓ} .$ Then $S_{k ℓ} = n$ when $k = ℓ = 0$ or $k = ℓ = n$ , $S_{k ℓ} = n / 2$ when $k = ℓ$ is strictly between $0$ and $n$ , and $S_{k ℓ} = 0$ when $k \neq ℓ$ . The half-endpoint convention is the one used by the DCT-I of Type-I cosine transform for Chebyshev–Lobatto data.

Facts & Assumptions

Given: A natural $n \geq 1$ and naturals $0 \leq k, ℓ \leq n$ .

[A1]

The grid size is $n + 1$ with $n \geq 1$ , and $0 \leq k, ℓ \leq n$ in the natural-number order.

[F1]

Type-I cosine transform for Chebyshev–Lobatto data fixes the Lobatto angles $j k π / n$ , the canonical real-image convention, and the half-weighted endpoint convention.

[F2]

The addition formulas for sine and cosine and The subtraction formulas for sine and cosine give the sine-difference telescoping identity and the cosine product-to-sum identity.

[F3]

Quarter-turn values and shifts by pi/2 and pi gives the shifts by $π / 2$ and the quarter-turn values. Iterating its shift identities by induction on the natural $m$ gives $\sin (m π / 2) = 0$ for even $m$ , $∣ \sin (m π / 2) ∣ = 1$ for odd $m$ , and $\cos (m π / 2) = 0$ for odd $m$ (The principle of mathematical induction).

[F4]

Signs, monotonicity intervals, and ranges of sine and cosine gives strict increase of sine on $[0, π / 2]$ and strict decrease on $[π / 2, π]$ ; with $\sin 0 = \sin π = 0$ from Quarter-turn values and shifts by pi/2 and pi, this implies $\sin θ > 0$ for $0 < θ < π$ .

Proof

1.1givenA1F1F2F4algebra

For the $n$ in [A1], and any natural frequency $m$ with $1 \leq m < 2 n$ , put $α : = m π / n$ and $C_{m} : = \sum_{j = 0}^{n - 1} \cos (j α)$ . Positivity of canonical naturals gives $n > 0$ , and $1 \leq m < 2 n$ gives $0 < α / 2 < π$ ; hence $\sin (α / 2) > 0$ by [F4]. The half-weighted endpoints are the DCT-I convention fixed by [F1]. By [F2], $2 \sin (α / 2) C_{m} = \sum_{j = 0}^{n - 1} (\sin ((j + \frac{1}{2}) α) - \sin ((j - \frac{1}{2}) α)) = \sin ((n - \frac{1}{2}) α) + \sin (α / 2) = 2 \sin (n α / 2) \cos ((n - 1) α / 2) .$ Since $\sin (α / 2) > 0$ , this gives $C_{m} = \sin (m π / 2) \cos ((n - 1) m π / (2 n)) / \sin (m π / (2 n))$ .

1.2givenF2F3algebra

If $m$ is even, the numerator factor $\sin (m π / 2)$ is $0$ by [F3], so $C_{m} = 0$ for $1 \leq m < 2 n$ . If $m$ is odd, write $(n - 1) m π / (2 n) = m π / 2 - m π / (2 n)$ ; the addition formulas and $\cos (m π / 2) = 0$ give $\cos ((n - 1) m π / (2 n)) = \sin (m π / 2) \sin (m π / (2 n))$ , hence $C_{m} = 1$ . For $m = 0$ and $m = 2 n$ , direct evaluation gives $C_{m} = n$ .

2.1step 1.2algebra

Define $D_{m} : = \frac{1}{2} + \sum_{j = 1}^{n - 1} \cos (j m π / n) + \frac{1}{2} (- 1)^{m}$ . Since $C_{m} = 1 + \sum_{j = 1}^{n - 1} \cos (j m π / n)$ , step 1.2 gives $D_{m} = 0$ for $1 \leq m < 2 n$ and $D_{0} = D_{2 n} = n$ .

3.1givenA1F1F2step 2.1algebra∎

For $k, ℓ$ in [A1], [F2] makes each product in $S_{k ℓ}$ one half the sum of the cosine terms with natural frequency indices $∣ k - ℓ ∣$ and $k + ℓ$ , so $S_{k ℓ} = \frac{1}{2} (D_{∣ k - ℓ ∣} + D_{k + ℓ})$ . If $k \neq ℓ$ , then $1 \leq ∣ k - ℓ ∣ < 2 n$ and $1 \leq k + ℓ < 2 n$ except the impossible distinct-endpoint case $k + ℓ = 2 n$ , so both terms vanish by step 2.1. If $k = ℓ = 0$ or $k = ℓ = n$ , both indices are $0$ or $2 n$ , giving $S_{k ℓ} = n$ . If $k = ℓ$ is interior, the indices are $0$ and $2 k$ with $1 \leq 2 k < 2 n$ , giving $S_{k ℓ} = n / 2$ . These cases prove the statement.

Depends on

Used by

DCT-I coefficients of the Chebyshev–Lobatto interpolant Theorem

Dependency tree · two levels

24 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

Lloyd N. Trefethen, Is Gauss Quadrature Better than Clenshaw–Curtis?, §2 (standard reference, not scraped)
L. Ridgway Scott, Numerical Analysis, 2nd ed., §13.4.1 (standard reference, not scraped)