ExampleConstruction: Literature-sourcedVerification: 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.

The two-node Gauss–Legendre rule is exact through degree three

Example

Assume the Axiom of Countable Choice and take Lebesgue measure restricted to the relative Borel sets of $[- 1, 1]$ . Its relative support is all of $[- 1, 1]$ , so it gives order-three moment data for $m = 2$ . The moments are $μ_{0} = 2$ , $μ_{1} = 0$ , $μ_{2} = 2 / 3$ , and $μ_{3} = 0$ . The monic orthogonal polynomials through degree two are $p_{0} = 1$ , $p_{1} = X$ , and $p_{2} = X^{2} - 1 / 3$ . Thus the Gaussian nodes are $x_{1} = - 1 / \sqrt{3}$ and $x_{2} = 1 / \sqrt{3}$ .

The Jacobi matrix is $J_{2} = (\begin{array}{cc} 0 & 1 / \sqrt{3} \\ 1 / \sqrt{3} & 0 \end{array}) .$ Its unit eigenvectors $(1, - 1) / \sqrt{2}$ and $(1, 1) / \sqrt{2}$ give weights $w_{1} = w_{2} = μ_{0} / 2 = 1$ . Therefore $Q_{2} (f) = f (- 1 / \sqrt{3}) + f (1 / \sqrt{3})$ is exact for every real polynomial of degree at most three.

Facts & Assumptions

Given: Countable choice and Lebesgue measure on $[- 1, 1]$ restricted to relative Borel sets.

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the Axiom of Countable Choice is assumed for the Lebesgue measure and Riemann–Lebesgue results used in this example.

[F1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ), Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, and Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable: under countable choice, the restriction is a positive measure on the relative Borel sets.

[F2]

A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included: a closed interval has measure its length; every positive-length subinterval of $[- 1, 1]$ has positive measure.

[F3]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, and A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: under countable choice, the Lebesgue moments of $1, x, x^{2}, x^{3}$ equal their ordinary integrals, which can be evaluated by polynomial primitives.

[F4]

Monic orthogonal polynomials exist uniquely through the quadrature order: checking the orthogonality equations identifies the monic polynomials uniquely.

[F5]

Monic orthogonal polynomials satisfy a three-term recurrence: the normalized recurrence coefficients form the displayed symmetric Jacobi matrix.

[F6]

The Jacobi matrix spectrum is the set of Gauss nodes: its eigenvalues are the Gaussian nodes.

[F7]

Gaussian weights equal the total mass times a Jacobi eigenvector's first-coordinate square: a unit eigenvector at a node gives weight $μ_{0}$ times the square of its first coordinate.

[F8]

Gaussian quadrature is exact through degree 2m−1 and has positive weights: the two-node rule is exact through degree $3$ .

[F9]

The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace and The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement: the usual real topology is its absolute-value metric topology, and every relative open neighborhood contains the intersection of $[- 1, 1]$ with an open metric ball about its point.

[F10]

The Borel sigma-algebra of a subspace is the trace of the ambient Borel sigma-algebra: every relative Borel set of $[- 1, 1]$ is $B \cap [- 1, 1]$ for an ambient real Borel set $B$ .

[F11]

Nonnegative real square roots exist uniquely: every positive real has a unique positive square root.

Proof

1.1A1F1F2F9F10choosealgebra

By [F10], every relative Borel set is $B \cap [- 1, 1]$ for ambient Borel $B$ . The interval is closed, hence ambient Borel, so this intersection is ambient Borel and is Lebesgue measurable by [F1]. Restricting Lebesgue measure to this sigma-algebra therefore defines the asserted positive measure; disjoint relative Borel unions are the same ambient measurable unions, so countable additivity is inherited. For $x \in [- 1, 1]$ , [F9] gives an $ε > 0$ such that $(x - ε, x + ε) \cap [- 1, 1]$ lies in any chosen relative open neighborhood $U$ of $x$ . Choose a closed interval $I$ of positive length inside that intersection, using a one-sided interval when $x$ is an endpoint. Then $I$ is relative Borel and [F2] gives $μ (I) > 0$ . Since $U = I ⊔ (U ∖ I)$ and both sets are relative Borel, countable additivity and nonnegativity from [F1] imply $μ (U) \geq μ (I) > 0$ . Thus every $x$ lies in the relative support, which has at least three points.

1.2A1F3algebra

The functions $1, x, x^{2}, x^{3}$ are continuous, hence Riemann integrable by [F3]. Their primitives $x, x^{2} / 2, x^{3} / 3, x^{4} / 4$ , evaluated at $- 1$ and $1$ , give respectively $2, 0, 2 / 3, 0$ . The Riemann–Lebesgue equality in [F3] gives the stated moment values.

2.1F3F4F11step 1.2algebra

The monic polynomials $1$ and $X$ are orthogonal in the required degrees: $\int x d μ = 0$ . The monic polynomial $X^{2} - 1 / 3$ is orthogonal to $1$ because $μ_{2} - (1 / 3) μ_{0} = 0$ , and to $X$ because $μ_{3} - (1 / 3) μ_{1} = 0$ . Uniqueness [F4] identifies $p_{0}, p_{1}, p_{2}$ as stated. By [F11], $\sqrt{3} > 0$ exists uniquely. The identity $X^{2} - 1 / 3 = (X - 1 / \sqrt{3}) (X + 1 / \sqrt{3})$ gives exactly the two roots $\pm 1 / \sqrt{3}$ .

2.2F3F5step 1.2algebra

Here $h_{0} = μ_{0} = 2$ , $h_{1} = \int x^{2} d μ = 2 / 3$ , and both recurrence diagonal entries are zero by the odd moments. Hence $β_{1} = h_{1} / h_{0} = 1 / 3$ , and [F5] gives the displayed $J_{2}$ . Direct multiplication shows its two displayed unit eigenvectors have eigenvalues $- 1 / \sqrt{3}$ and $1 / \sqrt{3}$ ; [F6] identifies those as the Gaussian nodes.

3.1F7F8step 1.2step 2.2algebra∎

For either unit eigenvector, the first-coordinate square is $1 / 2$ . Applying [F7] with $μ_{0} = 2$ gives each weight as $1$ . Exactness through degree three is [F8], proving the stated rule.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

124 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)