# 一元有理係數多項式：合併同次項、係數向量、次數與零多項式 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-polynomial/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-polynomial-01 · production-20261019-adopted-96 ## 目標與範圍 在 ℚ[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)。 ## 逐步主鏈 S01 · definition操作前 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) 條件：\text{finitely many}\ a_k\neq 0 規則：mko_polynomial · 依賴：G1 葉節點依據：mko_polynomial + poly_eq_coeff + def_intro 依 MKO，多項式就是它的係數資料：相等逐次比較係數，次數是係數非零的最大指數，零多項式（所有係數為 0）的次數在本條目記為未定義。因為只有有限個係數非零，最大值存在。之後的判斷都由係數決定，不由字面上寫了哪些項決定。 S02 · equivalent操作前 4x^3+3x^2-x+2-4x^3+x 操作後 (4x^3-4x^3)+3x^2+(-x+x)+2 條件：無 規則：add_comm · 依賴：G2, add_comm, add_assoc 葉節點依據：add_comm + add_assoc 依加法交換律與結合律，把 p 的各項按 x 的次方重新排列分組：x³ 項放在一起，x 項放在一起。此步只重排，還沒有合併。 S03 · equivalent操作前 (4x^3-4x^3)+3x^2+(-x+x)+2 操作後 0\cdot x^3+3x^2+0\cdot x+2 條件：無 規則：like_terms · 依賴：S02, like_terms 葉節點依據：like_terms + distributive + numeric_evaluation 合併同次項：4x³−4x³=(4−4)x³=0·x³，−x+x=(−1+1)x=0·x。這正是 MKO 要求「相同次冪的係數要先相加」。 S04 · equivalent操作前 0\cdot x^3+3x^2+0\cdot x+2 操作後 [2,0,3,0]=[2,0,3],\quad p=3x^2+2 條件：無 規則：poly_eq_coeff · 依賴：S03, poly_eq_coeff 葉節點依據：poly_eq_coeff + def_unfold 由低次到高次讀出係數：a_0=2、a_1=0、a_2=3、a_3=0，所有 k≥4 的係數為 0。向量 [2,0,3,0] 與 [2,0,3] 在每個次方的係數都相同（索引 3 的係數在兩者中都是 0），所以表示同一個多項式 p=3x²+2。 S05 · implies操作前 a_2=3\neq 0,\ a_k=0\ (k\geq 3) 操作後 \deg p=2 條件：p\neq 0 規則：mko_polynomial · 依賴：S01, S04 葉節點依據：mko_polynomial + def_unfold p 不是零多項式（a_2=3≠0），所以次數有定義。係數非零的指數只有 0 與 2，最大是 2，故 deg p=2。原式字面上出現 x³，但它的係數合併後是 0，不影響次數。 S06 · implies操作前 q\leftrightarrow[-1,1,0,0] 操作後 q=x-1,\quad \deg q=1 條件：無 規則：mko_polynomial · 依賴：G1, G2, S01 葉節點依據：mko_polynomial + poly_eq_coeff 向量 [−1,1,0,0] 表示 b_0=−1、b_1=1、b_2=b_3=0，所以 q=−1+x=x−1，與 [−1,1] 是同一個多項式。係數非零的最大指數是 1，deg q=1；向量長度 4 不代表次數 3。 S07 · implies操作前 x^2-x^2+3 操作後 (1-1)x^2+3=3,\quad [3],\quad \deg r=0 條件：無 規則：like_terms · 依賴：G2, like_terms, S01 葉節點依據：like_terms + mko_polynomial + numeric_evaluation 合併 x² 項：x²−x²=(1−1)x²=0。所以 r=3，係數向量 [3]。r 是非零常數多項式（a_0=3≠0），係數非零的最大指數是 0，deg r=0。這是 MKO para0 的例子。 S08 · implies操作前 5x-5x 操作後 (5-5)x=0,\quad z=0\ \text{(zero polynomial)},\quad z\neq r 條件：無 規則：poly_eq_coeff · 依賴：G2, like_terms, S01, S07 葉節點依據：poly_eq_coeff + like_terms + numeric_evaluation 5x−5x=(5−5)x=0·x，所以 z 的所有係數都是 0，z 是零多項式，依本條目它的次數未定義。z 與 r 不同：兩者的常數項分別為 0 與 3，0≠3，依係數相等的定義 z≠r。零多項式與非零常數多項式不可混淆。 S09 · equivalent操作前 p+q=[2,0,3]+[-1,1] 操作後 [2+(-1),\,0+1,\,3+0]=[1,1,3],\quad p+q=3x^2+x+1 條件：無 規則：mko_poly_ops · 依賴：S04, S06, mko_poly_ops 葉節點依據：mko_poly_ops + poly_eq_coeff + numeric_evaluation 加法逐次相加係數；q 在 x² 的係數是 0（超出 [−1,1] 的範圍）。所以 p+q 的係數為 2+(−1)=1、0+1=1、3+0=3，即 3x²+x+1，次數 2。 S10 · equivalent操作前 p\cdot q,\quad a=[2,0,3],\ b=[-1,1] 操作後 c=[-2,2,-3,3],\quad pq=3x^3-3x^2+2x-2 條件：無 規則：mko_poly_ops · 依賴：S04, S06, mko_poly_ops 葉節點依據：mko_poly_ops + finite_sum_rules + poly_eq_coeff 乘積的係數是有限卷積 c_k=Σ_{i+j=k} a_i b_j，其中超出向量的 a_i、b_j 都是 0。子步 S10.1 算 c_0、c_1，S10.2 算 c_2、c_3 並說明 k≥4 時 c_k=0。 S11 · implies操作前 pq=3x^3-3x^2+2x-2 操作後 \deg(pq)=3=\deg p+\deg q 條件：c_3=3\neq 0 規則：mko_polynomial · 依賴：S10, S10.2, S01 葉節點依據：mko_polynomial + numeric_evaluation c_3=3≠0 且 k≥4 時 c_k=0，所以 deg(pq)=3。在本例中它等於 deg p+deg q=2+1；首項係數 3 正是 p 與 q 首項係數的乘積 3·1。一般的次數乘法公式不在本稿證明。 S12 · implies操作前 p(2),\ q(2),\ (pq)(2) 操作後 p(2)=14,\ q(2)=1,\ (pq)(2)=24-12+4-2=14=p(2)\,q(2) 條件：無 規則：eval_hom · 依賴：S04, S06, S10, eval_hom 葉節點依據：eval_hom + numeric_evaluation 代入 x=2：p(2)=3·4+2=14，q(2)=2−1=1，(pq)(2)=3·8−3·4+2·2−2=14。依 eval_hom 應有 (pq)(2)=p(2)q(2)=14，結果一致。這只是對 S10 的一個一致性檢查；乘積本身由係數卷積確定，一個點的吻合不能證明係數正確。 S13 · implies操作前 p(1)=5=t(1) 操作後 p\neq t\quad([2,0,3]\neq[0,5]) 條件：無 規則：poly_eq_coeff · 依賴：S04, G2, poly_eq_coeff, mko_poly_ops 葉節點依據：poly_eq_coeff + numeric_evaluation p(1)=3+2=5，t(1)=5·1=5，在 x=1 的值相同。但 p 的常數項是 2，t 的常數項是 0，2≠0，依係數相等的定義 p≠t；在 x=0 也可看出 p(0)=2≠0=t(0)。MKO 指出單個代入值相等不建立多項式恆等式。 S14 · implies操作前 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 條件：無 規則：and_intro_elim · 依賴：S05, S06, S07, S08, S09, S11, S13 葉節點依據：and_intro_elim 彙整：p=3x²+2 次數 2，q=x−1 次數 1，r=3 次數 0，z 是零多項式（次數未定義）且 z≠r，p+q=3x²+x+1 次數 2，pq=3x³−3x²+2x−2 次數 3，p≠t 雖然 p(1)=t(1)。每個結論都由係數資料得出。 ## 局部子步與引理 S10.1 · equivalent操作前 c_0,\ c_1 操作後 c_0=a_0b_0=-2,\quad c_1=a_0b_1+a_1b_0=2+0=2 條件：無 規則：finite_sum_rules · 依賴：S10, finite_sum_rules 葉節點依據：finite_sum_rules + numeric_evaluation k=0 時只有 (i,j)=(0,0)：c_0=2·(−1)=−2。k=1 時有 (0,1) 與 (1,0)：c_1=2·1+0·(−1)=2。 S10.2 · equivalent操作前 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) 條件：無 規則：finite_sum_rules · 依賴：S10, finite_sum_rules 葉節點依據：finite_sum_rules + mul_zero + numeric_evaluation k=2：(0,2)、(1,1)、(2,0) 給出 2·0+0·1+3·(−1)=−3。k=3：(0,3)、(1,2)、(2,1)、(3,0) 中只有 a_2b_1=3·1=3 非零（b_2=b_3=0、a_3=0）。k≥4 時 i+j=k 必有 i≥3 或 j≥2，對應的 a_i 或 b_j 為 0，所以 c_k=0。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-polynomial-01.json)