ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

Chebyshev–Lobatto nodes cluster quadratically at the endpoints

Example

For $x_{j} = \cos (j π / N)$ , the endpoint gap $x_{0} - x_{1}$ is at most $π^{2} / (2 N^{2})$ , whereas a central adjacent-node gap is at least $\sqrt{2} / N$ . Their ratio tends to zero, and the smallest spacing has quadratic endpoint scale. The mesh is nonuniform for $N \geq 3$ ; for $N = 2$ the nodes $1, 0, - 1$ are equally spaced.

Facts & Assumptions

Given: An integer $N \geq 2$ and the decreasing Chebyshev–Gauss–Lobatto nodes $x_{j}$ .

[F1]

Chebyshev–Gauss–Lobatto collocation grid: $x_{j} = \cos (j π / N)$ for $0 \leq j \leq N$ .

[F2]

The subtraction formulas for sine and cosine and The addition formulas for sine and cosine: cosine differences reduce to products of sine factors, $\sin (a + b) = \sin a \cos b + \cos a \sin b$ , and $\cos (2 t) = \cos^{2} t - \sin^{2} t$ .

[F3]

Sine chord and Lipschitz bounds: $\sin t \geq 2 t / π$ for $0 \leq t \leq π / 2$ and $∣ \sin u - \sin v ∣ \leq ∣ u - v ∣$ for all real $u, v$ .

[F4]

Signs, monotonicity intervals, and ranges of sine and cosine and Quarter-turn values and shifts by pi/2 and pi: sine is strictly increasing on $[0, π / 2]$ and $\sin (π / 2) = 1$ .

[F5]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : each nonnegative real has a unique nonnegative square root.

[F6]

For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ : for every $ε > 0$ there is an integer $n \geq 1$ with $1 / n < ε$ . Canonical naturals are positive and strictly increasing: canonical positive naturals are positive and strictly increasing. Inverses of positives are positive, and reciprocation reverses order: reciprocation reverses strict order on positive reals. Algebra of limits: sums, scalar multiples, products and quotients: a fixed real multiple of a sequence converging to zero also converges to zero.

Verification

1.1F1F2F3algebra

The subtraction and addition identities [F2] give $x_{j} - x_{j + 1} = 2 \sin (\frac{(2 j + 1) π}{2 N}) \sin (\frac{π}{2 N}), x_{0} - x_{1} = 2 \sin^{2} (\frac{π}{2 N}) .$ By [F3], $\sin (π / (2 N)) \leq π / (2 N)$ , hence $x_{0} - x_{1} \leq π^{2} / (2 N^{2})$ .

2.1givenF2F3F4F5step 1.1algebra

If $N$ is odd, choose $j = (N - 1) / 2$ ; then $(2 j + 1) π / (2 N) = π / 2$ and [F4] gives sine equal to $1$ , so the gap formula in step 1.1 and [F3] give a central gap at least $2 / N \geq \sqrt{2} / N$ . If $N$ is even, choose $j = N / 2 - 1$ and write $t = π / 2 - π / (2 N) \geq π / 4$ . The addition and subtraction formulas [F2] give $\sin (π / 4) = \cos (π / 4)$ and $2 \sin (π / 4) \cos (π / 4) = \sin (π / 2) = 1$ . Thus $\sin^{2} (π / 4) = 1 / 2$ ; the chord bound [F3] gives $\sin (π / 4) \geq 1 / 2 > 0$ , so uniqueness of the nonnegative square root [F5] gives $\sin (π / 4) = \sqrt{2} / 2$ . Monotonicity [F4] now gives $\sin t \geq \sqrt{2} / 2$ . In either parity, [F3] also gives $\sin (π / (2 N)) \geq 1 / N$ , so the selected central gap in step 1.1 is at least $\sqrt{2} / N$ .

3.1F2F3F4F6step 1.1step 2.1algebra∎

Put $a = π / (2 N)$ . Every adjacent gap has the form $2 \sin ((2 j + 1) a) \sin a$ , with $a \leq (2 j + 1) a \leq π - a$ . Reflecting about $π / 2$ and using monotonicity [F4] gives $\sin ((2 j + 1) a) \geq \sin a$ ; equality occurs at $j = 0$ and $j = N - 1$ . Hence the smallest spacing is exactly $2 \sin^{2} a$ , and [F3] bounds it by $2 / N^{2} \leq 2 \sin^{2} a \leq π^{2} / (2 N^{2})$ . For every $ε > 0$ , [F6] supplies an integer $n \geq 1$ with $1 / n < ε$ ; for every integer $N \geq \max {2, n}$ , positivity and monotonicity of the canonical naturals and reciprocal order give $0 < 1 / N \leq 1 / n < ε$ . Thus $1 / N \to 0$ , and the endpoint-to-central-gap ratio is at most $π^{2} / (2 N)$ , which tends to zero by the fixed-multiple limit law in [F6]. For $N \geq 3$ , the selected central angle, reflected into $[0, π / 2]$ if necessary, is strictly larger than $a$ ; strict monotonicity in [F4] makes its gap larger than the endpoint gap. For $N = 2$ , the nodes are $1, 0, - 1$ and both gaps equal $1$ . This proves the quadratic endpoint scale with its stated nonuniformity exception.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

Jie Shen and Tao Tang, Spectral and High-Order Methods with Applications, Ch. 2 (standard reference, not scraped)
Lloyd N. Trefethen, Finite Difference and Spectral Methods for Ordinary and Partial Differential Equations, Ch. 8 (standard reference, not scraped)