LemmaStatement: Literature-sourcedProof: 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.

The highest derivative of a polynomial

Statement

Let $m \in N$ , $m \geq 1$ , and let $p : R \to R$ be the evaluation function of a formal real polynomial of degree at most $m$ , or the zero polynomial. Write its actual coefficient list through its degree and extend that list by zeros to $a_{0}, \dots, a_{m}$ (all zero for the zero polynomial); this is an evaluation vector, not a change to the formal polynomial object. Define iterated derivatives as in Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ and write $m!_{R} : = \prod_{j < m} (j + 1)$ , with each natural factor read as its canonical real image under The canonical natural $ι (n) = n \cdot 1_{F}$ of a field. Then $p^{(m)} (x) = a_{m} m!_{R}$ for every $x \in R$ . In particular, this derivative is zero if $\deg p < m$ , and it is $m!_{R}$ if $p$ is monic of degree $m$ .

Facts & Assumptions

Given: A natural number $m \geq 1$ and the evaluation function and padded coefficient vector of a formal polynomial of degree at most $m$ , or of the zero polynomial with its all-zero evaluation vector.

[F1]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: a nonzero formal real polynomial is a finite coefficient list with nonzero final coefficient, and its evaluation is the corresponding finite sum of coefficients times powers. The zero polynomial is a separate formal object with no degree.

[F2]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : $p^{(0)} = p$ and, wherever $p^{(r)}$ is differentiable, $p^{(r + 1)} = (p^{(r)})^{'}$ .

[F3]

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 The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: every finite polynomial sum is differentiable term by term; $x^{k}$ has derivative $k x^{k - 1}$ for $k \geq 1$ , where the natural coefficient is its canonical real image, and $x^{0}$ is constant with derivative $0$ .

[F4]

The principle of mathematical induction: a property true at $0$ and inherited by successors holds for every natural number.

[F5]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: a natural number used as a real scalar denotes its canonical real image; the image of a successor is the image of its predecessor plus $1$ .

[F6]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ : the full falling product $m (m - 1) \dots 1$ is the natural factorial $m!$ , which is also the natural product $\prod_{j < m} (j + 1)$ .

[F7]

Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ : the canonical real image of a finite natural product is the corresponding product of real images, so the product representation of $m!$ in [F6] becomes the stated $m!_{R}$ .

Proof

1.1givenF1F5construct

For a nonzero formal polynomial, [F1] gives $p (X) = \sum_{k = 0}^{m} a_{k} X^{k}$ , since zero padding adds only zero terms. For the zero polynomial, $p \equiv 0$ and the given evaluation vector is all zero, so the same identity holds without representing the formal object by a coefficient list. For $0 \leq r \leq m$ , define the real function $Q_{r} (X) = \sum_{k = r}^{m} a_{k} (\prod_{s = 0}^{r - 1} (k - s)) X^{k - r}$ , with the empty product equal to $1$ ; each factor $k - s$ is natural because $k \geq r > s$ .

2.1basegivenstep 1.1F2F3F7ihalgebra

At $r = 0$ , $Q_{0} = p = p^{(0)}$ by [F2]. If $r < m$ and $p^{(r)} = Q_{r}$ , termwise differentiation in [F3] kills the $k = r$ constant term and multiplies each term with $k > r$ by its exponent $k - r$ ; for each $k > r$ , the resulting real coefficient is $a_{k} (\prod_{s = 0}^{r - 1} (k - s)) (k - r) = a_{k} \prod_{s = 0}^{r} (k - s)$ . Indeed the finite natural product extends by its last factor, and [F7] carries that natural identity to the product of canonical real images. The new exponent is $(k - r) - 1 = k - (r + 1)$ , so the differentiated sum is exactly $Q_{r + 1}$ . Hence $p^{(r + 1)} = Q_{r + 1}$ .

3.1step 1.1step 2.1F4ihdischarge-induction

Apply [F4] to the property $P (r)$ that $r \leq m$ implies $p^{(r)} = Q_{r}$ . Step 2.1 proves $P (0)$ . If $P (r)$ holds and $r + 1 \leq m$ , then $r < m$ and step 2.1 proves $p^{(r + 1)} = Q_{r + 1}$ ; if $r + 1 > m$ , $P (r + 1)$ is vacuous. Thus $P (m)$ holds.

4.1step 3.1givenF6F7discharge-inductionalgebra∎

At $r = m$ , the sum defining $Q_{m}$ contains only $k = m$ and equals $a_{m} \prod_{s = 0}^{m - 1} (m - s) = a_{m} m!_{R}$ : [F6] identifies the natural falling product with $m!$ , and [F7] carries it to the real product in the statement. This proves the stated derivative and both special cases.

Depends on

Used by

Dependency tree · two levels

43 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

Mark Embree, Lecture Notes on Numerical Analysis, lecture 3 (standard reference, not scraped)
Jean-Paul Berrut and Lloyd N. Trefethen, Barycentric Lagrange Interpolation (standard reference, not scraped)