LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Legendre-Gauss-Lobatto nodes are distinct and interior critical points are simple

Statement

For every integer $p \geq 1$ , the Legendre polynomial $P_{p}$ has exactly $p$ simple roots in $(- 1, 1)$ , and $P_{p}^{'}$ has exactly $p - 1$ simple roots in $(- 1, 1)$ , one between each consecutive pair of roots of $P_{p}$ . Consequently, the $p + 1$ nodes consisting of $- 1$ , $1$ , and the roots of $P_{p}^{'}$ are pairwise distinct.

Facts & Assumptions

Given: An integer $p \geq 1$ and the Legendre polynomials $P_{n}$ .

[F1]

Legendre polynomials by Rodrigues' formula and their unweighted pairing: $P_{p}$ is a nonzero degree- $p$ polynomial.

[F2]

Legendre polynomials have explicit norms and weighted derivative orthogonality: $P_{p}$ is orthogonal in unweighted $L^{2} (- 1, 1)$ to every polynomial of degree less than $p$ .

[F3]

Rolle's theorem: if $a < b$ , $f$ is continuous on $[a, b]$ , differentiable at every point of $(a, b)$ , and $f (a) = f (b)$ , then $f^{'} (c) = 0$ for some $c \in (a, b)$ : between two distinct zeros of a differentiable real function there is a zero of its derivative.

Proof

1.1F1F2givenalgebra

Suppose $P_{p}$ has only $m < p$ sign-changing roots $r_{1}, \dots, r_{m}$ in $(- 1, 1)$ and set $q (x) = \prod_{j = 1}^{m} (x - r_{j})$ , with $q = 1$ if $m = 0$ . At each sign-changing root both $P_{p}$ and $q$ change sign, while at every other real root $P_{p}$ does not change sign; therefore $P_{p} q$ has one constant sign on $(- 1, 1)$ and is not identically zero. It is continuous and nonzero on some open interval, so its integral is nonzero. But $\deg q = m < p$ , and [F2] gives $\int_{- 1}^{1} P_{p} q = 0$ , a contradiction. Thus $P_{p}$ has at least $p$ sign-changing roots in the open interval.

2.1F1F3step 1.1givenalgebra∎

A degree- $p$ polynomial cannot have more than $p$ distinct roots. The $p$ roots obtained in step 1.1 therefore exhaust its degree; each has multiplicity one and there are no other roots. Rolle's theorem [F3] between consecutive roots gives $p - 1$ distinct roots of $P_{p}^{'}$ in $(- 1, 1)$ . Since $P_{p}^{'}$ has degree $p - 1$ , these are all its roots and each is simple. None equals an endpoint, so adjoining $- 1$ and $1$ gives $p + 1$ distinct nodes, including the case $p = 1$ where there are no interior critical points.

Depends on

Used by

Legendre-Gauss-Lobatto nodes, weights, and tensor quadrature Definition

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

Joachim Schöberl, Numerical Methods for Partial Differential Equations, p-version FEM (standard reference, not scraped)
Lloyd N. Trefethen, Short note on the mass matrix for Gauss-Lobatto grid points (standard reference, not scraped)