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.

Exact weights and degree-nine exactness of the eight-panel rule

Statement

For the nodes $x_{j} = - 1 + j / 4$ and rule $Q_{8}$ of Closed Newton–Cotes rule on eight equal panels, the weights are the integrals of the degree-eight Lagrange cardinal polynomials. Interpreting polynomial inputs by their evaluation functions, the rule is exact for the zero polynomial and every nonzero formal polynomial of degree at most $9$ .

Facts & Assumptions

Given: The nine equally spaced nodes $x_{j} = - 1 + j / 4$ , their weights $w_{j}$ , and the finite rule $Q_{8}$ .

[F1]

Closed Newton–Cotes rule on eight equal panels: $Q_{8} (f) = \sum_{j = 0}^{8} w_{j} f (x_{j})$ with the displayed symmetric rational weights.

[F2]

Cardinal-polynomial interpolation and Cardinal interpolation functions are polynomials of the stated degrees: each cardinal polynomial $ℓ_{j}$ has degree $8$ , equals $1$ at $x_{j}$ , equals $0$ at the other eight nodes, and is $\prod_{m \neq j} (x - x_{m}) / (x_{j} - x_{m})$ ; every finite cardinal sum is zero or has degree at most $8$ .

[F3]

Existence and uniqueness of the cardinal-polynomial interpolant and A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots: the degree-at-most-eight interpolant at nine distinct nodes is unique; equivalently, two such polynomials agreeing at all nine nodes are equal.

[F4]

Monotone change of variable for Riemann-integrable functions: under $t = 4 (x + 1)$ , $\int_{- 1}^{1} ℓ_{j} (x) d x = \frac{1}{4} \int_{0}^{8} ℓ_{j} ((t - 4) / 4) d t$ .

[F5]

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, 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)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, and Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ : each polynomial monomial is integrable, its integral is obtained from its power antiderivative, and finite sums integrate termwise.

Proof

1.1givenF2F4algebra

Put $P_{j} (t) = \prod_{0 \leq m \leq 8, m \neq j} (t - m)$ and $D_{j} = \prod_{m \neq j} (j - m)$ . Substituting $t = 4 (x + 1)$ into [F2] cancels the eight factors $1 / 4$ between numerator and denominator, giving $ℓ_{j} ((t - 4) / 4) = P_{j} (t) / D_{j}$ . For $j = 0, 1, 2, 3, 4$ , the pairs $(D_{j}; coefficients of P_{j} (t) from t^{0} upward)$ are $(40320; [40320, - 109584, 118124, - 67284, 22449, - 4536, 546, - 36, 1])$ , $(- 5040; [0, - 40320, 69264, - 48860, 18424, - 4025, 511, - 35, 1])$ , $(1440; [0, - 20160, 44712, - 36706, 15289, - 3580, 478, - 34, 1])$ , $(- 720; [0, - 13440, 32048, - 28692, 12864, - 3195, 447, - 33, 1])$ , and $(576; [0, - 10080, 24876, - 23312, 10993, - 2864, 418, - 32, 1])$ . These coefficients follow by multiplying the eight factors, and each denominator is the product of the corresponding integer differences.

2.1givenF1F2F4F5step 1.1algebra

Integrating each coefficient list by [F5] gives $\int_{0}^{8} P_{j} (t) / D_{j} d t = (3956, 23552, - 3712, 41984, - 18160)_{j} / 14175$ for $j = 0, 1, 2, 3, 4$ . The factor $1 / 4$ in [F4] therefore gives $\int_{- 1}^{1} ℓ_{j} (x) d x = (989, 5888, - 928, 10496, - 4540)_{j} / 14175$ , exactly the first five weights in [F1]. Reflection $x \mapsto - x$ sends node $x_{j}$ to $x_{8 - j}$ and, by the product formula in [F2], sends $ℓ_{j}$ to $ℓ_{8 - j}$ ; the substitution preserves the integral. Thus the remaining four cardinal integrals equal the corresponding symmetric weights in [F1].

3.1givenF1F2F3F5step 2.1algebra

For the zero polynomial and every nonzero formal polynomial $p$ of degree at most $8$ , its cardinal interpolant $\sum_{j = 0}^{8} p (x_{j}) ℓ_{j}$ is the evaluation of a formal polynomial of degree at most $8$ or is zero, and it agrees with the evaluation function of $p$ at all nine nodes by [F2]. Uniqueness [F3] makes the two evaluation functions equal. Integrating this finite identity and using step 2.1 and [F5] yields $\int_{- 1}^{1} p = \sum_{j} p (x_{j}) \int_{- 1}^{1} ℓ_{j} = Q_{8} (p)$ .

4.1givenF1F5step 3.1algebra∎

The nodes and weights in [F1] occur in equal pairs under $x \mapsto - x$ , so $Q_{8} (x^{9}) = 0$ by cancellation of the paired terms and the zero central term. The integral of the odd polynomial $x^{9}$ over $[- 1, 1]$ is zero by the same substitution. The zero polynomial, and each nonzero formal polynomial of degree at most $9$ , has the form $p + c X^{9}$ for a zero polynomial or nonzero formal polynomial $p$ of degree at most $8$ and a scalar $c$ ; step 3.1 and linearity therefore prove exactness through degree $9$ .

Depends on

Used by

Dependency tree · two levels

65 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

L. Ridgway Scott, Numerical Analysis, 2nd ed., §13.1.1 (standard reference, not scraped)
NIST Digital Library of Mathematical Functions, §3.5(iv), Interpolatory Quadrature Rules (standard reference, not scraped)