一元有理係數多項式：合併同次項、係數向量、次數與零多項式

目標與範圍

在 ℚ[x] 中，設 p(x)=4x³+3x²−x+2−4x³+x，q 的係數向量為 [−1,1,0,0]，r(x)=x²−x²+3，z(x)=5x−5x，t(x)=5x。求 p、q、r 的係數與次數，判定 z 是零多項式並區分 z 與 r；以係數計算 p+q 與 p·q 並求次數；最後說明 p(1)=t(1) 不能推出 p=t。

只用 MKO 的表示：形式變數 x、有理係數、有限支撐，係數向量由低次到高次，尾端零不改變多項式，零多項式的次數在本條目記為未定義。只計算這些具體多項式；次數乘法公式 deg(pq)=deg p+deg q 只在本例核對，不作一般證明。不處理多元多項式或其他係數環；不改動 canonical MKO 或英文 edition。

已知條件與符號

• add_assoc
• add_comm
• distributive
• finite_sum_rules
• numeric_evaluation

• G1 — 固定形式變數 x；ℚ[x] 的多項式由有理係數 a_k（k∈ℕ）給出，只有有限個非零，p(x)=Σ_k a_k x^k；係數向量由低次到高次列出，超出向量的係數為 0，尾端零不改變多項式（MKO 假設 a1、a2）。
• G2 — p(x)=4x³+3x²−x+2−4x³+x；q 的係數向量 [−1,1,0,0]；r(x)=x²−x²+3；z(x)=5x−5x；t(x)=5x。

• \mathbb{Q}[x] — 有理係數的一元多項式全體
• a_k — x^k 的係數；超出列出範圍者為 0
• [a_0,a_1,a_2] — 由低次到高次的係數向量
• \deg p — 非零多項式中係數非零的最大指數
• c_k=\sum_{i+j=k}a_ib_j — 乘積的第 k 個係數（有限卷積）
• p(c) — 在 x=c 求值

規則與來源

• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• finite_sum_rules · prerequisite — 有限和：Σ_{i=1}^{0} a_i=0、Σ_{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 — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_polynomial · cited — Q[x] 的一元多項式以有限個有理係數 a_k 表示，指數均為非負整數。非零多項式的次數為最大非零係數的索引；本條目把零多項式的次數記為未定義。 · mko-polynomial
• mko_poly_ops · cited — 加法逐次相加係數；乘法按指數和合併，所得係數是有限卷積。代入一個數值是對同一份係數資料求值，單個代入值相等不建立多項式恆等式。 · mko-polynomial
• poly_eq_coeff · prerequisite — ℚ[x] 中兩個多項式相等，當且僅當對每個 k，x^k 的係數都相等（未列出的係數視為 0）。
• like_terms · prerequisite — 合併同次項：c x^k+d x^k=(c+d)x^k（分配律）；不同次的項不能合併。
• eval_hom · prerequisite — 對 c∈ℚ，求值 p↦p(c)=Σ_k a_k c^k 滿足 (p+q)(c)=p(c)+q(c) 與 (pq)(c)=p(c)q(c)。

逐步主鏈

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

局部子步與引理

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)

逐步反向審查

• S14 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S11, S13, and_intro_elim — 目標 G：各項結論。足夠條件 H：S05 至 S13 的各別結論；H⇒G 只是合取。H 由係數計算正向證成，沒有把 G 當作前提。
• S13 · premise_audit · poly_eq_coeff, mko_poly_ops, numeric_evaluation — 一個係數不同即足以推出不等（N14、N15）；反向「一點相等推出恆等」被明確拒絕。
• S12 · premise_audit · eval_hom, numeric_evaluation — 一致性檢查只能發現錯誤，不能確認正確；可重算（N11 至 N13）。
• S11 · premise_audit · S10, mko_polynomial — 只對本例宣稱；不從一個例子推出一般公式。
• S10.2 · inverse_equivalence · finite_sum_rules, numeric_evaluation, mul_zero — k≥4 的論證對所有 k 成立，不是逐一檢查；數值可重算（N6、N7）。
• S10.1 · inverse_equivalence · finite_sum_rules, numeric_evaluation — 列出所有 i+j=k 的指數對，不遺漏也不重複；數值可重算（N4、N5）。
• S10 · inverse_equivalence · mko_poly_ops, poly_eq_coeff — 卷積公式給出乘積的每個係數，結果與 pq 逐次相同；N8 在格點上以次數界核對整個恆等式。
• S09 · inverse_equivalence · mko_poly_ops, poly_eq_coeff, numeric_evaluation — 每個係數都是精確的有理數加法，可逐次核對（N3、N10），兩邊是同一個多項式。
• S08 · premise_audit · like_terms, poly_eq_coeff, mko_polynomial — 一個係數不同就足以推出不等；「未定義」是本條目的教學慣例，與 Mathlib 的 degree（⊥）或 natDegree（0）需要另外對應。
• S07 · premise_audit · like_terms, mko_polynomial — 字面上有 x²，但合併後係數為 0；次數由合併後的資料決定（N16）。
• S06 · premise_audit · G1, mko_polynomial, poly_eq_coeff — 次數由最大非零係數決定，與向量長度或尾端零無關。
• S05 · premise_audit · S04, mko_polynomial — 需要先合併（S03）；若直接讀最高字面指數，會誤得 3。
• S04 · inverse_equivalence · poly_eq_coeff — 係數逐次相同，依多項式相等的定義雙向成立；尾端零可加可去。
• S03 · inverse_equivalence · like_terms, distributive, numeric_evaluation — 分配律雙向成立；4−4=0、−1+1=0 可重算（N1、N2）；N9 以次數界在格點上核對整個恆等式。
• S02 · inverse_equivalence · add_comm, add_assoc — 重排與還原都只用交換律與結合律，兩式是同一個多項式。
• S01 · premise_audit · G1, mko_polynomial, poly_eq_coeff — 此步只寫出定義；「最大值存在」用到有限支撐，零多項式被明確排除在次數定義之外。

錯誤控制與反例

先合併同次項再讀次數

MKO 指出的誤解之一是未合併同次項就取最高字面指數。p 字面上有 4x³ 與 −4x³，合併後 x³ 的係數為 0，deg p=2（S03 至 S05）。r=x²−x²+3 同理是常數 3（S07）。

向量長度與尾端零不決定次數

MKO 指出的另一個誤解是用向量長度或尾端零決定次數。[−1,1,0,0] 長度為 4，但它就是 x−1，次數 1（S06）；[2,0,3,0] 與 [2,0,3] 是同一個多項式（S04）。

零多項式不是零次

z=5x−5x 的所有係數都是 0，本條目記其次數為未定義；r=3 則是次數 0 的非零常數。兩者常數項 0 與 3 不同，所以 z≠r（S08）。Mathlib 的 degree 給零多項式 ⊥、natDegree 給 0，對應時不可混用。

一點相等不是恆等

p(1)=t(1)=5，但 p 與 t 的係數不同，p(0)=2≠0=t(0)（S13）。S12 在 x=2 的吻合也只是一致性檢查，乘積由係數卷積確定。

• p=4x³+3x²−x+2−4x³+x 的次數是 3，因為式中出現 4x³ → reject — 合併後 x³ 的係數是 4−4=0，p=3x²+2，次數 2。
• 係數向量 [−1,1,0,0] 長度為 4，所以 q 的次數是 3 → reject — 最大非零係數的索引是 1，q=x−1，次數 1。
• z=5x−5x 和常數 3 一樣是零次多項式 → reject — z 是零多項式，本條目中次數未定義；而且 z 的常數項 0≠3，z≠3。
• 因為 p(1)=t(1)=5，所以 p=t → reject — p(0)=2≠0=t(0)，常數項不同；單點相等不建立恆等式。

結論與限制

合併同次項後 p=3x²+2，deg p=2（不是字面上的 3）；q=[−1,1,0,0]=x−1，deg q=1（不是向量長度減一）；r=3 是零次常數；z=5x−5x 是零多項式，次數未定義且 z≠r；p+q=3x²+x+1；pq=3x³−3x²+2x−2，次數 3；p(1)=t(1)=5 但 p≠t。

• 非零多項式乘積的次數公式 deg(pq)=deg p+deg q 只在本例核對（S11），一般證明不在本稿範圍。
• N8 至 N10、N16、N17 是 degree 型核對：在 {0,1,至 degree} 的整數格點上比較兩邊，對次數不超過該界的一元多項式足以判定恆等；這依賴「非零多項式根的個數不超過次數」，本稿沒有證明它。

驗證及來源綁定

17 個本稿宣告算術檢查；只支持所列算式。

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）