TheoremStatement: 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.

Certified Golub–Welsch intervals contain the Gaussian nodes and weights

Statement

Let admissible moment data $(a, b, m, r, μ)$ with $r \geq 2 m - 1$ and finite moment intervals satisfying the promise in Certified Gaussian nodes and weights by Golub–Welsch be given. If that algorithm returns certified with node intervals $N_{i}$ and weight intervals $W_{i}$ , then the Gaussian nodes $x_{i}$ and weights $w_{i}$ satisfy $x_{i} \in N_{i}$ and $w_{i} \in W_{i}$ for every $i = 1, \dots, m$ . An inconclusive return makes no claim.

Facts & Assumptions

Given: Admissible moment data, truthful moment enclosures through degree $2 m - 1$ , and a certified algorithm return.

[F1]

The uniform interval residual certifier is sound on success: on certified output, each supplied Hankel family has a unique solution and its coefficients lie in the reported error balls.

[F2]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: all finite outward interval expression DAGs contain the corresponding exact values.

[F3]

The Gauss orthogonal polynomial has simple roots inside the interval and The Jacobi matrix spectrum is the set of Gauss nodes: the true Jacobi matrix is real symmetric and its increasingly ordered eigenvalues are exactly the Gaussian nodes in $(a, b)$ .

[F4]

Certified Hermitian eigenvalue intervals from residual and Gram bounds and The residual and orthogonality certifier encloses the full ordered spectrum: success requires validated residual, Gram and norm bounds, and every increasingly ordered eigenvalue in the admitted Hermitian matrix family lies in its returned node interval.

[F5]

Gaussian weights equal the total mass times a Jacobi eigenvector's first-coordinate square: for a unit eigenvector $u_{i}$ at $x_{i}$ , $w_{i} = μ_{0} ∣ (u_{i})_{1} ∣^{2}$ .

[F6]

A residual and spectral gap bound a Gaussian weight error: a nonzero approximate eigenvector with norm lower bound $s$ , residual bound $ρ$ , and separation gap lower bound $g_{i}$ gives weight error at most $2 \sqrt{2} μ_{0} ρ / (s g_{i})$ .

Proof

1.1F1F2givenalgebra

Each coefficient solve in step 1 uses the full moment rectangle families, which contain the actual Hankel matrix and right-hand side by the moment promise. By [F1], successful uniform residual certification encloses the unique actual coefficient vector. The true Hankel matrices are positive definite by the support hypothesis and The polynomial moment pairing is a real inner product; thus these solutions are the coefficients of the monic orthogonal polynomials. By [F2], the arithmetic in step 2 encloses every true $h_{j}, α_{j}, β_{j}$ and hence the true Jacobi matrix.

2.1F2F3F5step 1.1algebra

If $m = 1$ , the true Jacobi matrix is the one-by-one matrix $[α_{0}]$ . By [F3] its sole eigenvalue is the sole Gaussian node $x_{1}$ , so $x_{1} = α_{0}$ . Its unit eigenvector is $(1)$ , and [F5] gives $w_{1} = μ_{0}$ . The outward interval $α_{0}$ and moment interval $I_{0}$ in step 3 of the algorithm contain these exact values by [F2].

2.2F3F4step 1.1

Assume $m \geq 2$ . By [F3], the eigenvalues of the true Jacobi matrix are precisely the Gaussian nodes. The matrix family in step 5 contains this matrix by step 1.1, and successful near-orthonormal certification gives $x_{i} \in N_{i}$ by [F4].

3.1F2F4step 2.2algebra

For column $v_{i}$ of $V$ , the accepted checks in step 5 and [F4] certify $∥ J v_{i} - θ_{i} v_{i} ∥_{2} \leq ρ$ and $∥ V^{*} V - I ∥_{2} \leq d < 1$ . Therefore $∥ v_{i} ∥_{2}^{2} \geq 1 - d$ , so the positive lower endpoint $s$ of the outward enclosure of $\sqrt{1 - d}$ is a lower bound on its norm. The disjoint ordered intervals in step 5 make $g_{i}$ in step 6 a positive lower bound for the distance from $θ_{i}$ to every other true node.

4.1F2F5F6step 3.1algebra

Apply [F6] to $(v_{i}, θ_{i})$ and the bounds of step 3.1. The interval $C_{i}$ contains $μ_{0} (v_{i})_{1}^{2} / ∥ v_{i} ∥_{2}^{2}$ and $R_{i}$ is at least the resulting error bound, because $\sup (I_{0}) \geq μ_{0}$ . Thus the exact Gaussian weight $w_{i}$ belongs to $C_{i} + [- R_{i}, R_{i}] = W_{i}$ by [F5].

5.1givenstep 2.1step 2.2step 4.1cases∎

The $m = 1$ case is step 2.1; for $m \geq 2$ , steps 2.2 and 4.1 give every node and weight enclosure. These cases exhaust $m \geq 1$ , proving the claim.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Certified Gaussian nodes and weights by Golub–Welsch.

Dependency tree · two levels

64 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

John A. Gubner, Gaussian Quadrature and the Eigenvalue Problem, §§2–5, 2020 (standard reference, not scraped)
MATH 373 Lecture Notes, Lecture 14: Gaussian Quadrature, §§10.2–10.5 (standard reference, not scraped)
Walter Gautschi, The Interplay Between Classical Analysis and (Numerical) Linear Algebra, §2.1 (standard reference, not scraped)