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

A real coefficient list of degree d has at most d real roots

Statement

Let $d \in N$ and let $a_{0}, a_{1}, \dots, a_{d}$ be real numbers with $a_{d} \neq 0$ (Complete ordered field (least-upper-bound property)). Using the finite sums of Finite sums and finite products, by recursion and the natural powers $x^{k}$ of Integer powers $a^{m}$ , put

$P (x) = \sum_{k = 0}^{d} a_{k} x^{k} (x \in R),$

the list always being read as the sequence that is $a_{k}$ for $k \leq d$ and $0$ for $k > d$ . Let $Z = Z (P) = {x \in R : P (x) = 0}$ . Then $Z$ is finite of cardinality at most $d$ : there is $m \in N$ with $m \leq d$ and $Z \approx m$ (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ). For $d = 0$ this says $Z = \emptyset$ .

This is a statement about finite coefficient lists and their evaluations: it requires neither a polynomial-ring construction nor any choice axiom. Only field arithmetic, finite sums and induction are used, and if $Z \neq \emptyset$ one single root is instantiated existentially, never a family of choices. It is the local prerequisite for the algebraic-number example on this page.

Facts & Assumptions

Given: A natural number $d$ , reals $a_{0}, \dots, a_{d}$ with $a_{d} \neq 0$ , and the sequence $c$ with $c_{k} = a_{k}$ for $k < σ (d)$ and $c_{k} = 0$ otherwise; $R$ is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field, Field), with finite sums $\sum_{k < n}$ as in Finite sums and finite products, by recursion and powers as in Integer powers $a^{m}$ . We prove, by strong induction on $d$ , the claim

$C (d) : for every list a_{0}, \dots, a_{d} with a_{d} \neq 0, there is m \in N, m \leq d, with Z \approx m .$

[F1]

Field arithmetic: $a b = 0$ implies $a = 0$ or $b = 0$ (A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ ); $0 \cdot a = 0$ (Multiplication by zero: $0 \cdot a = 0$ ); addition, subtraction and multiplication obey the usual distributivity and associativity laws, and $a - b = 0$ implies $a = b$ .

[F2]

Finite sums (Finite sums and finite products, by recursion): $\sum_{k < 0} u_{k} = 0$ , $\sum_{k < σ (n)} u_{k} = \sum_{k < n} u_{k} + u_{n}$ , and a general block is $\sum_{k = m}^{n} u_{k} = \sum_{j < d^{'}} u_{m + j}$ for $d^{'} = n + 1 - m$ , the empty block being $0$ . Powers: $x^{0} = 1$ and $x^{n + 1} = x^{n} \cdot x$ .

[F3]

Finite sum laws (Laws of finite sums and finite products): additivity $\sum_{k < n} (u_{k} + v_{k}) = \sum_{k < n} u_{k} + \sum_{k < n} v_{k}$ , scaling $\sum_{k < n} λ u_{k} = λ \sum_{k < n} u_{k}$ , splitting $\sum_{k < n} u_{k} = \sum_{k < m} u_{k} + \sum_{k = m}^{n - 1} u_{k}$ for $m \leq n$ , and products of sums in $x$ distribute over addition in the standard way used below.

[F4]

Strong induction (Strong (complete) induction).

[F5]

Naturals (The natural numbers $N$ (von Neumann), Addition of natural numbers, Order on the natural numbers, On $N$ the order is membership: $m < n ⟺ m \in n$ , Discreteness: $σ (n)$ is the immediate successor, Every natural number is a transitive set and is not a member of itself, $\leq$ is a linear order on $N$ ): $σ (j) = j \cup {j}$ ; $m < n ⟺ m \in n$ and $n = {m \in N : m < n}$ ; $m \leq n ⟺ m \subseteq n$ ; $m < n ⟺ σ (m) \leq n$ ; $j < σ (j)$ ; $m \notin m$ ; $\leq$ is reflexive, antisymmetric and transitive, so $\leq$ composes and $m^{''} \leq m^{'} \leq e$ gives $m^{''} \leq e$ ; and $m \leq e$ gives $σ (m) \leq σ (e)$ , because $m + k = e$ implies $σ (m) + k = σ (m + k) = σ (e)$ .

[F6]

Finite sets and cardinality (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection): $A$ is finite when $A \approx n$ for some $n \in N$ ; $\approx$ is symmetric and transitive; the restriction of a bijection to a subset is a bijection onto the image of that subset; and $\emptyset \approx 0$ .

[F7]

Set notation (Subset $x \subseteq y$ , proper subset $x ⊊ y$ , and the separation notation ${z \in x : φ (z)}$ , The difference $a ∖ b$ , the symmetric difference $a △ b$ , and the complement $X ∖ a$ relative to a set $X$ ): $u \in S ∖ T$ exactly when $u \in S$ and $u \notin T$ , and $S \subseteq T$ means every element of $S$ lies in $T$ .

Proof

technique · induction

1.1F4F5F6F7

Subsets of a natural number, with a cardinal bound. For every $m \in N$ and every $S \subseteq m$ there is $m^{''} \in N$ with $m^{''} \leq m$ and $S \approx m^{''}$ . By strong induction on $m$ : for $m = 0$ we have $S \subseteq \emptyset$ , so $S = \emptyset \approx 0$ and $0 \leq 0$ . For $m = σ (j)$ , assume the claim for every $j^{'} < m$ and let $S \subseteq σ (j) = j \cup {j}$ . If $j \notin S$ then $S \subseteq j$ , so the hypothesis at $j$ gives $m^{''} \leq j$ with $S \approx m^{''}$ , and $m^{''} \leq j < σ (j) = m$ composes to $m^{''} \leq m$ . If $j \in S$ , then $T : = S ∖ {j} \subseteq j$ , so the hypothesis at $j$ gives $m^{''} \leq j$ and a bijection $u : T \to m^{''}$ . Extend $u$ to $u^{'} : S \to σ (m^{''})$ by $u^{'} (j) = m^{''}$ and $u^{'} (s) = u (s)$ for $s \neq j$ : the values of $u$ all lie in $m^{''}$ while $m^{''} \notin m^{''}$ , so $m^{''}$ is a new value and the extension is injective, and it is onto $m^{''} \cup {m^{''}} = σ (m^{''})$ , so $S \approx σ (m^{''})$ ; moreover $m^{''} \leq j$ gives $σ (m^{''}) \leq σ (j) = m$ . In both cases $S$ has the required cardinal bound, so the claim holds by strong induction.

1.2F1F2F6base

Base case $C (0)$ . Let $a_{0} \neq 0$ . Since $x^{0} = 1$ , the recursion for finite sums gives $\sum_{k < 1} c_{k} x^{k} = \sum_{k < 0} c_{k} x^{k} + c_{0} x^{0} = 0 + a_{0} = a_{0}$ for every $x$ , and $a_{0} \neq 0$ . Hence $Z = \emptyset \approx 0$ with $0 \leq 0$ , which is $C (0)$ .

1.3F1F2F3

The divided coefficients. Assume now $d = σ (e)$ , so $d \geq 1$ , and fix $r \in Z$ , so that $P (r) = 0$ ; write $b_{m} : = \sum_{j = 0}^{e - m} a_{m + 1 + j} r^{j}$ for $m < d$ , a finite sum of reals, and $Q (x) : = \sum_{m < d} b_{m} x^{m}$ . Then (i) $b_{d - 1} = b_{e} = \sum_{j = 0}^{0} a_{e + 1 + j} r^{j} = a_{d} r^{0} = a_{d} \neq 0$ ; and (ii) for $1 \leq k \leq e$ , splitting the sum $b_{k - 1} = \sum_{j = 0}^{e - k + 1} a_{k + j} r^{j} = a_{k} + \sum_{j = 1}^{e - k + 1} a_{k + j} r^{j} = a_{k} + r \sum_{i = 0}^{e - k} a_{k + 1 + i} r^{i} = a_{k} + r b_{k}$ , using scaling and the definition of the block sums. So $Q$ is again of the displayed form, with an explicit coefficient list of degree $e$ whose top coefficient $b_{e} = a_{d}$ is nonzero.

2.1step 1.3F1F2F3

The constant term. Scaling (ii) of step 1.3 by $r$ or, directly from the definition, $r b_{0} = \sum_{j = 0}^{e} r a_{1 + j} r^{j} = \sum_{j = 0}^{e} a_{1 + j} r^{j + 1} = \sum_{k = 1}^{d} a_{k} r^{k}$ . Adding $a_{0}$ and using the splitting of $\sum_{k < d + 1}$ at $k = 1$ gives $a_{0} + r b_{0} = \sum_{k = 0}^{d} a_{k} r^{k} = P (r) = 0$ , that is $r b_{0} = - a_{0}$ .

2.2step 1.3F4ih

Induction hypothesis for $Q$ . The coefficient list $b_{0}, \dots, b_{e}$ has $b_{e} = a_{d} \neq 0$ by step 1.3, so the strong induction hypothesis $C (e)$ at $e < d$ applies to it: the zero set $W : = {x \in R : Q (x) = 0}$ satisfies $W \approx m^{'}$ for some $m^{'} \in N$ with $m^{'} \leq e = d - 1$ .

3.1step 1.3step 2.1F1F2F3

The factorisation $P (x) = (x - r) Q (x)$ . Because $d = σ (e) = e + 1$ , splitting each sum at its last index gives $\sum_{m < d} b_{m} x^{m + 1} = \sum_{m < e} b_{m} x^{m + 1} + b_{e} x^{e + 1}$ and $\sum_{m < d} r b_{m} x^{m} = r b_{0} + \sum_{m = 1}^{e} r b_{m} x^{m}$ . Therefore, by scaling, additivity and subtraction, $(x - r) Q (x) = b_{e} x^{d} + \sum_{m < e} b_{m} x^{m + 1} - r b_{0} - \sum_{m = 1}^{e} r b_{m} x^{m}$ . Replacing $m$ by $m - 1$ in the first trailing block, $\sum_{m < e} b_{m} x^{m + 1} = \sum_{m = 1}^{e} b_{m - 1} x^{m}$ , so the two trailing blocks combine into $\sum_{m = 1}^{e} (b_{m - 1} - r b_{m}) x^{m} = \sum_{m = 1}^{e} a_{m} x^{m}$ by step 1.3(ii); and $b_{e} = a_{d}$ by step 1.3(i) while $r b_{0} = - a_{0}$ by step 2.1. Hence $(x - r) Q (x) = a_{d} x^{d} + \sum_{m = 1}^{e} a_{m} x^{m} + a_{0} = \sum_{k = 0}^{d} a_{k} x^{k} = P (x)$ , again by splitting.

4.1step 3.1F1F7

Every root of $P$ other than $r$ is a root of $Q$ . If $x \in Z$ and $x \neq r$ , then $(x - r) Q (x) = P (x) = 0$ by step 3.1, and $x - r \neq 0$ , so $Q (x) = 0$ by [F1]. Hence $x \in W$ , i.e. $Z ∖ {r} \subseteq W$ .

5.1step 4.1F7

$Z$ sits in $W$ together with possibly $r$ . By step 4.1, every $x \in Z$ either equals $r$ or lies in $W$ ; that is, $Z \subseteq {r} \cup W$ .

6.1step 1.1step 2.2step 5.1F5F6

Case $r \in W$ . Then ${r} \cup W = W$ , so $Z \subseteq W$ by step 5.1. Transport along a bijection $u : W \to m^{'}$ from step 2.2: the image $u [Z] \subseteq m^{'}$ satisfies $u [Z] \approx Z$ by restriction of $u$ , and step 1.1 applied to $u [Z] \subseteq m^{'}$ gives $m^{''} \leq m^{'}$ with $u [Z] \approx m^{''}$ ; then $Z \approx m^{''}$ by transitivity, and $m^{''} \leq m^{'} \leq e = d - 1 < d$ , so $m^{''} \leq d$ .

6.2step 1.1step 2.2step 5.1F5F6F7

Case $r \notin W$ . Extend a bijection $u : W \to m^{'}$ from step 2.2 to $u^{'} : W \cup {r} \to σ (m^{'})$ by $u^{'} (r) = m^{'}$ and $u^{'} (w) = u (w)$ for $w \in W$ : the values of $u$ all lie in $m^{'}$ while $m^{'} \notin m^{'}$ , so $u^{'}$ is injective, and it is onto $m^{'} \cup {m^{'}} = σ (m^{'})$ . Hence $W \cup {r} \approx σ (m^{'})$ , and $Z \subseteq {r} \cup W = W \cup {r}$ by step 5.1; restriction of $u^{'}$ to $Z$ gives $Z \approx u^{'} [Z]$ with $u^{'} [Z] \subseteq σ (m^{'})$ , and step 1.1 applied at $σ (m^{'})$ gives $m^{''} \leq σ (m^{'})$ with $u^{'} [Z] \approx m^{''}$ , so $Z \approx m^{''}$ ; finally $m^{'} \leq e$ gives $σ (m^{'}) \leq σ (e) = d$ by [F5], so $m^{''} \leq d$ .

7.1step 6.1step 6.2

Since $r \in W$ or $r \notin W$ , steps 6.1 and 6.2 give: for the fixed $r \in Z$ there is $m \in N$ with $m \leq d$ and $Z \approx m$ .

8.1step 7.1F6

The induction step $C (e) \Rightarrow C (d)$ . Let $d = σ (e)$ and let $a_{0}, \dots, a_{d}$ with $a_{d} \neq 0$ be a list, with zero set $Z$ . If $Z = \emptyset$ then $Z \approx 0$ and $0 \leq d$ , so $C (d)$ holds for this list. Otherwise $Z \neq \emptyset$ ; instantiating one $r \in Z$ existentially, the construction of steps 1.3 through 7.1 produces $m \leq d$ with $Z \approx m$ . In both cases $C (d)$ holds.

9.1step 1.2step 8.1F4discharge-induction: base step 1.2 and induction step 8.1∎

Conclusion. $C (0)$ is step 1.2, and $C (e) \Rightarrow C (σ (e))$ for every $e$ is step 8.1, so by strong induction $C (d)$ holds for every $d$ ; applied to the given list, the zero set $Z$ of $P$ is finite of cardinality at most $d$ , as claimed. If $d = 0$ the hypothesis $a_{d} \neq 0$ reads $a_{0} \neq 0$ and step 1.2 gives $Z = \emptyset$ . No step selects from a family: at most one root is instantiated, and all coefficients $b_{m}$ are given by explicit finite sums.

Remarks

The division is honest synthetic division. Writing the coefficients from the top down, $b_{e} = a_{d}$ and $b_{k - 1} = a_{k} + r b_{k}$ , the identity $(x - r) Q (x) = P (x)$ with $Q (x) = \sum_{m < d} b_{m} x^{m}$ holds for every $x$ , not only at $x = r$ , and the case $r = 0$ needs no division: step 2.1 uses only multiplication by $r$ .
The final count is explicit rather than decreed. Step 1.1 shows by induction that a subset of a natural number $m$ is equinumerous with some $m^{''} \leq m$ , which is exactly what the two case counts in steps 6.1 and 6.2 consume; no separate appeal to a counting principle is needed.

Depends on

Used by

Real algebraic numbers are countably infinite, without choice Example

Dependency tree · two levels

55 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

Jiri Lebl, Basic Analysis I, Volume I (complete author-hosted textbook) (standard reference, not scraped)