Univariate rational polynomials: combining like terms, coefficient vectors, degree and the zero polynomial

Goal and scope

In ℚ[x], let p(x)=4x³+3x²−x+2−4x³+x, let q have coefficient vector [−1,1,0,0], and let r(x)=x²−x²+3, z(x)=5x−5x and t(x)=5x. Find the coefficients and degrees of p, q and r; show that z is the zero polynomial and distinguish it from r; compute p+q and p·q from coefficients and find their degrees; finally explain why p(1)=t(1) does not give p=t.

Uses only the MKO's representation: a formal variable x, rational coefficients, finite support, coefficient vectors from low to high power, trailing zeros not changing the polynomial, and the degree of the zero polynomial called undefined in this entry. Only these particular polynomials are computed; the degree rule deg(pq)=deg p+deg q is checked for this example only and not proved in general. Multivariate polynomials and other coefficient rings are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• add_assoc
• add_comm
• distributive
• finite_sum_rules
• numeric_evaluation

• G1 — Fix a formal variable x; a polynomial in ℚ[x] is given by rational coefficients a_k (k∈ℕ), only finitely many nonzero, with p(x)=Σ_k a_k x^k; coefficient vectors list coefficients from low to high power, coefficients beyond a vector are 0, and trailing zeros do not change the polynomial (MKO assumptions a1, a2).
• G2 — p(x)=4x³+3x²−x+2−4x³+x; q has coefficient vector [−1,1,0,0]; r(x)=x²−x²+3; z(x)=5x−5x; t(x)=5x.

• \mathbb{Q}[x] — all univariate polynomials with rational coefficients
• a_k — the coefficient of x^k; zero beyond the listed range
• [a_0,a_1,a_2] — a coefficient vector from low to high power
• \deg p — the largest index with a nonzero coefficient, for nonzero p
• c_k=\sum_{i+j=k}a_ib_j — the k-th coefficient of a product (finite convolution)
• p(c) — evaluation at x=c

Rules and sources

• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_polynomial · cited — A univariate polynomial in Q[x] is represented by finitely many rational coefficients a_k, with nonnegative integer exponents. The degree of a nonzero polynomial is the largest index with a nonzero coefficient; this entry calls the degree of the zero polynomial undefined. · mko-polynomial
• mko_poly_ops · cited — Addition adds coefficients power by power; multiplication collects by sums of exponents, and the resulting coefficients are a finite convolution. Substituting a number evaluates the same coefficient data, and equality of a single substituted value does not establish a polynomial identity. · mko-polynomial
• poly_eq_coeff · prerequisite — Two polynomials in ℚ[x] are equal exactly when, for every k, their coefficients of x^k are equal (coefficients not listed count as 0).
• like_terms · prerequisite — Combining like terms: c x^k+d x^k=(c+d)x^k (distributivity); terms of different powers are not combined.
• eval_hom · prerequisite — For c∈ℚ, evaluation p↦p(c)=Σ_k a_k c^k satisfies (p+q)(c)=p(c)+q(c) and (pq)(c)=p(c)q(c).

Main derivation

p\in\mathbb{Q}[x]

p=\sum_k a_k x^k,\quad p=q\iff a_k=b_k\ \text{for all}\ k,\quad \deg p=\max\{k\mid a_k\neq 0\}\ (p\neq 0)

4x^3+3x^2-x+2-4x^3+x

(4x^3-4x^3)+3x^2+(-x+x)+2

(4x^3-4x^3)+3x^2+(-x+x)+2

0\cdot x^3+3x^2+0\cdot x+2

0\cdot x^3+3x^2+0\cdot x+2

[2,0,3,0]=[2,0,3],\quad p=3x^2+2

a_2=3\neq 0,\ a_k=0\ (k\geq 3)

\deg p=2

q\leftrightarrow[-1,1,0,0]

q=x-1,\quad \deg q=1

x^2-x^2+3

(1-1)x^2+3=3,\quad [3],\quad \deg r=0

5x-5x

(5-5)x=0,\quad z=0\ \text{(zero polynomial)},\quad z\neq r

p+q=[2,0,3]+[-1,1]

[2+(-1),\,0+1,\,3+0]=[1,1,3],\quad p+q=3x^2+x+1

p\cdot q,\quad a=[2,0,3],\ b=[-1,1]

c=[-2,2,-3,3],\quad pq=3x^3-3x^2+2x-2

pq=3x^3-3x^2+2x-2

\deg(pq)=3=\deg p+\deg q

p(2),\ q(2),\ (pq)(2)

p(2)=14,\ q(2)=1,\ (pq)(2)=24-12+4-2=14=p(2)\,q(2)

p(1)=5=t(1)

p\neq t\quad([2,0,3]\neq[0,5])

p,q,r,z,p+q,pq,t

\deg p=2,\ \deg q=1,\ \deg r=0,\ z=0\ (\deg\ \text{undefined}),\ \deg(p+q)=2,\ \deg(pq)=3,\ p\neq t

Substeps and lemmas

c_0,\ c_1

c_0=a_0b_0=-2,\quad c_1=a_0b_1+a_1b_0=2+0=2

c_2,\ c_3,\ c_k\ (k\geq 4)

c_2=a_0b_2+a_1b_1+a_2b_0=0+0-3=-3,\quad c_3=a_2b_1=3,\quad c_k=0\ (k\geq 4)

Reverse audits

• S14 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S11, S13, and_intro_elim — Goal G: all the stated conclusions. Sufficient condition H: the separate conclusions of S05 to S13; H⇒G is just conjunction. H is proved forwards from coefficient computations; G is never used as a premise.
• S13 · premise_audit · poly_eq_coeff, mko_poly_ops, numeric_evaluation — One differing coefficient suffices for inequality (N14, N15); the converse inference from one equal value to an identity is explicitly rejected.
• S12 · premise_audit · eval_hom, numeric_evaluation — A consistency check can reveal an error but cannot confirm correctness; it is recomputable (N11 to N13).
• S11 · premise_audit · S10, mko_polynomial — Claimed for this example only; no general formula is inferred from one example.
• S10.2 · inverse_equivalence · finite_sum_rules, numeric_evaluation, mul_zero — The argument for k≥4 covers every such k at once rather than checking them one by one; the values are recomputable (N6, N7).
• S10.1 · inverse_equivalence · finite_sum_rules, numeric_evaluation — All index pairs with i+j=k are listed, none missing or repeated; the values are recomputable (N4, N5).
• S10 · inverse_equivalence · mko_poly_ops, poly_eq_coeff — The convolution formula gives every coefficient of the product, and the result agrees with pq power by power; N8 checks the whole identity on a grid with a degree bound.
• S09 · inverse_equivalence · mko_poly_ops, poly_eq_coeff, numeric_evaluation — Each coefficient is an exact rational sum and can be checked power by power (N3, N10); both sides are the same polynomial.
• S08 · premise_audit · like_terms, poly_eq_coeff, mko_polynomial — One differing coefficient is enough for inequality; 'undefined' is this entry's teaching convention and must be matched separately with Mathlib's degree (⊥) or natDegree (0).
• S07 · premise_audit · like_terms, mko_polynomial — x² appears literally, but its combined coefficient is 0; the degree is read from the combined data (N16).
• S06 · premise_audit · G1, mko_polynomial, poly_eq_coeff — The degree is decided by the largest nonzero coefficient, independent of the vector's length or trailing zeros.
• S05 · premise_audit · S04, mko_polynomial — The like terms must first be combined as in S03; reading the highest literal exponent would wrongly give 3.
• S04 · inverse_equivalence · poly_eq_coeff — The coefficients agree power by power, so by the definition of polynomial equality the step is two-way; a trailing zero may be added or removed.
• S03 · inverse_equivalence · like_terms, distributive, numeric_evaluation — Distributivity works both ways; 4−4=0 and −1+1=0 are recomputable (N1, N2); N9 checks the whole identity on a grid with a degree bound.
• S02 · inverse_equivalence · add_comm, add_assoc — Rearranging and restoring use only commutativity and associativity, so both forms are the same polynomial.
• S01 · premise_audit · G1, mko_polynomial, poly_eq_coeff — This step only states the definitions; the existence of the maximum uses finite support, and the zero polynomial is explicitly excluded from the degree definition.

Error controls and negative controls

Combine like terms before reading the degree

One error named in the MKO is taking the highest literal exponent before combining like terms. p shows 4x³ and −4x³ literally, but the combined x³ coefficient is 0 and deg p=2 (S03 to S05). Likewise r=x²−x²+3 is the constant 3 (S07).

Vector length and trailing zeros do not decide the degree

The other error named in the MKO is deciding the degree from the vector length or trailing zeros. [−1,1,0,0] has length 4 but is x−1, of degree 1 (S06); [2,0,3,0] and [2,0,3] are the same polynomial (S04).

The zero polynomial is not of degree zero

Every coefficient of z=5x−5x is 0, and this entry calls its degree undefined; r=3 is a nonzero constant of degree 0. Their constant coefficients 0 and 3 differ, so z≠r (S08). Mathlib's degree gives the zero polynomial ⊥ and natDegree gives 0; the two must not be mixed when matching.

Equal at one point is not an identity

p(1)=t(1)=5, but p and t have different coefficients, and p(0)=2≠0=t(0) (S13). The agreement at x=2 in S12 is likewise only a consistency check; the product is determined by the coefficient convolution.

• p=4x³+3x²−x+2−4x³+x has degree 3 because 4x³ appears in it → reject — After combining, the x³ coefficient is 4−4=0, so p=3x²+2 of degree 2.
• The coefficient vector [−1,1,0,0] has length 4, so q has degree 3 → reject — The largest index with a nonzero coefficient is 1, so q=x−1 of degree 1.
• z=5x−5x is a polynomial of degree 0, just like the constant 3 → reject — z is the zero polynomial, whose degree is undefined in this entry; moreover its constant coefficient 0≠3, so z≠3.
• Since p(1)=t(1)=5, p=t → reject — p(0)=2≠0=t(0), so the constant coefficients differ; equality at one point does not establish an identity.

Result and limitations

After combining like terms p=3x²+2 and deg p=2 (not the literal 3); q=[−1,1,0,0]=x−1 with deg q=1 (not the vector length minus one); r=3 is a constant of degree 0; z=5x−5x is the zero polynomial, with undefined degree and z≠r; p+q=3x²+x+1; pq=3x³−3x²+2x−2 of degree 3; and p(1)=t(1)=5 while p≠t.

• The degree rule deg(pq)=deg p+deg q for nonzero polynomials is checked only for this example (S11); its general proof is outside this guide.
• N8 to N10, N16 and N17 are degree checks: both sides are compared at the integers 0 up to the degree bound, which decides an identity of univariate polynomials within that bound; this relies on a nonzero polynomial having no more roots than its degree, which this guide does not prove.

Verification and source binding

17 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7aed146fa53618c3b3b6c889910ca918859436792d1f15685287e4d47d9dee02
• original source SHA-256: 7aed146fa53618c3b3b6c889910ca918859436792d1f15685287e4d47d9dee02
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)