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

A finite product of monic linear factors is monic

Statement

For every $n \in N$ and reals $r_{0}, \dots, r_{n - 1}$ , the function $P_{n} (X) = \prod_{k < n} (X - r_{k})$ is the evaluation of a formal real polynomial of degree exactly $n$ with leading coefficient $1$ . For $n = 0$ the product is empty and equals $1$ .

Facts & Assumptions

Given: A natural $n$ and the indicated finite list of real roots.

[F1]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: a finite coefficient list defines its evaluation, degree, and leading coefficient.

[F2]

Finite sums and finite products, by recursion and Laws of finite sums and finite products: finite sums obey the recursive last-term rule, addition and scalar multiplication.

[F3]

Laws of integer exponents: powers satisfy $X^{k + 1} = X^{k} X$ and the usual exponent identities.

[F4]

The reals form a field: real multiplication distributes over addition and has additive inverses.

[F5]

The principle of mathematical induction: induction holds on $N$ .

Proof

technique · induction

1.1basegivenF1F2construct

At $n = 0$ , the empty product is $1$ , the evaluation of the one-term polynomial $(1)$ , which is monic of degree zero.

1.2givenF1F2F3F4algebraihconstruct

Suppose $P_{n} (X) = \sum_{k = 0}^{n} a_{k} X^{k}$ with $a_{n} = 1$ , as supplied by the induction hypothesis. Multiplication by the next factor gives $P_{n} (X) (X - r_{n}) = \sum_{k = 0}^{n} a_{k} X^{k + 1} - \sum_{k = 0}^{n} r_{n} a_{k} X^{k} .$ By the finite-sum and field laws [F2, F4], this is represented by the coefficient list $b_{0} = - r_{n} a_{0}$ , $b_{k} = a_{k - 1} - r_{n} a_{k}$ for $1 \leq k \leq n$ , and $b_{n + 1} = a_{n} = 1$ . This list is a formal polynomial by [F1]; its last coefficient is $1$ , so its degree is $n + 1$ and it is monic.

2.1step 1.1step 1.2F5discharge-induction∎

Induction [F5] proves the claim for every finite list length, including the empty product case.

Depends on

Used by

Dependency tree · two levels

34 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 1 (standard reference, not scraped)
Jean-Paul Berrut and Lloyd N. Trefethen, Barycentric Lagrange Interpolation (standard reference, not scraped)