# 有理係數多項式因式分解：以係數比對驗證提公因子、二項式乘積與平方差 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-factorization/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-factorization-01 · production-20261019-adopted-96 ## 目標與範圍 在 ℚ[x] 中：(一) 把 p(x)=3x²+3x−18 分解為 3(x+3)(x−2)；(二) 把 q(x)=2x²−50 分解為 2(x−5)(x+5)；每個分解都以展開並比對每個係數驗證。(三) 證明 x²+25≠(x−5)(x+5)，且 x²+25 不能寫成兩個一次因式的乘積。(四) 說明 x³ 與 x 在 x=−1,0,1 取值相同卻不是同一個多項式。 在 MKO 的範圍內：一個形式變數 x、有理係數、有限係數資料。示範提公因子、二項式乘積與平方差，並以係數比對作為恆等式的判準。不提供一般多項式的完整分解演算法（MKO 明示），a、b 的選取只是嘗試，由隨後的展開驗證。x²−2 在 ℚ 與 ℝ 中可分解性的差別只作說明，不在本稿證明；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - distributive - add_comm - mul_comm - zero_product - square_nonneg - numeric_evaluation - G1 — 固定形式變數 x，係數屬於 ℚ，以有限係數資料表示；因子與乘積都去掉尾端零（MKO 假設 a1、a2）。 - G2 — p(x)=3x²+3x−18，q(x)=2x²−50，s(x)=x²+25；比較用的單項式 x³ 與 x。 - \mathbb{Q}[x] — 有理係數的一元多項式全體 - p=f\cdot g — 因式分解候選：一個多項式恆等式 - a,\ b,\ d — 二項式乘積與平方差中的有理常數 - p(c) — 在 x=c 求值 ## 規則與來源 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。 - square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。 - mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_factorization · cited — 在 Q[x] 中，p 的因式分解候選 p=f·g 是多項式恆等式：展開並合併同次項後每個係數都相同。本條目示範二項式乘積、提公因子與平方差，不宣稱提供全部多項式的完整分解演算法。 · mko-factorization - 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∈ℚ（或 c∈ℝ），求值 f↦f(c) 滿足 (f+g)(c)=f(c)+g(c) 與 (fg)(c)=f(c)g(c)；相等的多項式在每個 c 的值相同。 - L_binom · lemma — 對 a,b∈ℚ，ℚ[x] 中 (x+a)(x+b)=x²+(a+b)x+ab。 - L_diffsq · lemma — 對 d∈ℚ，ℚ[x] 中 (x−d)(x+d)=x²−d²。 - L_no_linear_factor · lemma — 不存在有理數 u、v、w、t（u≠0、w≠0）使 x²+25=(ux+v)(wx+t)；即 x²+25 在 ℚ[x] 中不是兩個一次因式的乘積。 ## 逐步主鏈 S01 · definition操作前 p=f\cdot g\ \text{(proposed)} 操作後 p=f\cdot g\iff\text{every coefficient of }p\text{ equals that of the expanded }f\cdot g 條件：無 規則：mko_factorization · 依賴：G1 葉節點依據：mko_factorization + poly_eq_coeff 依 MKO，因式分解候選是一個多項式恆等式：把右邊展開、合併同次項後，每個次方的係數都必須與左邊相同（poly_eq_coeff）。所以驗證一個分解就是做係數比對，而不是代入幾個數值。 S02 · equivalent操作前 (x+a)(x+b) 操作後 x^2+(a+b)x+ab 條件：a,b\in\mathbb{Q} 規則：L_binom · 依賴：S01 葉節點依據：distributive + mul_comm + like_terms 依引理 L_binom，兩個首一一次式的乘積的一次項係數是 a+b、常數項是 ab。這是 MKO 的二項式乘積公式；證明在 S02.1、S02.2。 S03 · equivalent操作前 3x^2+3x-18 操作後 3(x^2+x-6) 條件：無 規則：distributive · 依賴：G2, distributive 葉節點依據：distributive + poly_eq_coeff + numeric_evaluation 三個係數 3、3、−18 都是 3 的倍數，依分配律提出公因子 3：3(x²+x−6)=3x²+3x−18。核對係數：3·1=3、3·1=3、3·(−6)=−18。 S04 · implies操作前 a=3,\ b=-2 操作後 a+b=3+(-2)=1,\ ab=3\cdot(-2)=-6 條件：無 規則：numeric_evaluation · 依賴：S02, S03 葉節點依據：numeric_evaluation 要讓 x²+x−6 符合 S02 的形式，需要 a+b=1 且 ab=−6。嘗試 a=3、b=−2：3+(−2)=1、3·(−2)=−6，兩個條件都成立。怎麼找到這組數不重要，重要的是它通過 S05 的展開驗證。 S05 · equivalent操作前 (x+3)(x-2) 操作後 x^2+(3+(-2))x+3\cdot(-2)=x^2+x-6 條件：無 規則：L_binom · 依賴：S02, S04 葉節點依據：L_binom + forall_elim + numeric_evaluation 代入引理 L_binom（a=3、b=−2）：(x+3)(x−2)=x²+(3+(−2))x+3·(−2)=x²+x−6。係數 [−6,1,1] 與 x²+x−6 逐一相同。 S06 · equivalent操作前 3x^2+3x-18 操作後 3(x+3)(x-2) 條件：無 規則：eq_replace · 依賴：S03, S05 葉節點依據：eq_replace + poly_eq_coeff + distributive 在 S03 的 3(x²+x−6) 中，把 x²+x−6 換成 S05 的 (x+3)(x−2)，得 p=3(x+3)(x−2)。整體核對：展開 3(x+3)(x−2)=3(x²+x−6)=3x²+3x−18，係數 [−18,3,3] 與 p 相同（N6）。 S07 · equivalent操作前 (x-d)(x+d) 操作後 x^2-d^2 條件：d\in\mathbb{Q} 規則：L_diffsq · 依賴：S02 葉節點依據：L_binom + numeric_evaluation 依引理 L_diffsq，平方差 x²−d² 可分解為 (x−d)(x+d)。證明在 S07.1，是 L_binom 的特例。 S08 · equivalent操作前 2x^2-50 操作後 2(x^2-25) 條件：無 規則：distributive · 依賴：G2, distributive 葉節點依據：distributive + numeric_evaluation 係數 2 與 −50 都是 2 的倍數，提出公因子 2：2(x²−25)=2x²−50。 S09 · equivalent操作前 x^2-25 操作後 (x-5)(x+5) 條件：25=5^2 規則：L_diffsq · 依賴：S07 葉節點依據：L_diffsq + forall_elim + numeric_evaluation 25=5²，所以 x²−25 是平方差，依 L_diffsq（d=5）得 (x−5)(x+5)。 S10 · equivalent操作前 2x^2-50 操作後 2(x-5)(x+5) 條件：無 規則：eq_replace · 依賴：S08, S09 葉節點依據：eq_replace + poly_eq_coeff + distributive 把 S08 中的 x²−25 換成 (x−5)(x+5)，得 q=2(x−5)(x+5)。整體核對：展開得 2(x²−25)=2x²−50，係數 [−50,0,2] 與 q 相同（N9）；一次項係數 0 也必須相符。 S11 · implies操作前 x^2+25\ \text{vs.}\ (x-5)(x+5) 操作後 (x-5)(x+5)=x^2-25\neq x^2+25 條件：無 規則：poly_eq_coeff · 依賴：G2, S09, poly_eq_coeff 葉節點依據：poly_eq_coeff + numeric_evaluation 由 S09，(x−5)(x+5)=x²−25，常數項是 −25；s=x²+25 的常數項是 25。25≠−25，所以兩者不是同一個多項式。把平方和套用平方差公式是錯的。 S12 · implies操作前 x^2+25=(ux+v)(wx+t),\ u\neq0,\ w\neq0 操作後 \text{impossible in}\ \mathbb{Q}[x] 條件：u\neq 0; w\neq 0 規則：L_no_linear_factor · 依賴：G2, eval_hom, square_nonneg 葉節點依據：L_no_linear_factor + contradiction 依引理 L_no_linear_factor，x²+25 在 ℚ[x] 中不能寫成兩個一次因式的乘積，不只是 (x−5)(x+5) 不行。證明在 S12.1 至 S12.3：若有一次因式，就有有理根，但 c²+25 永遠是正數。 S13 · implies操作前 x^3\ \text{and}\ x\ \text{at}\ x=-1,0,1 操作後 \text{equal values, but}\ x^3\neq x\ \text{in}\ \mathbb{Q}[x] 條件：無 規則：poly_eq_coeff · 依賴：G2, poly_eq_coeff, eval_hom 葉節點依據：poly_eq_coeff + numeric_evaluation (−1)³=−1、0³=0、1³=1，所以 x³ 與 x 在這三點取值相同；事實上 x³−x=(x−1)x(x+1) 恰在這三點為零。但 x³ 的 x³ 係數是 1，x 的是 0，所以兩者不是同一個多項式；x=2 時 8≠2。兩者次數至多 3，要用代入值判定恆等至少需要 4 個相異點；三個點的吻合不足以建立恆等式。 S14 · implies操作前 p,\ q,\ s,\ x^3\ \text{vs}\ x 操作後 p=3(x+3)(x-2),\ q=2(x-5)(x+5),\ s\neq(x-5)(x+5),\ s\ \text{has no degree-one factor},\ x^3\neq x 條件：無 規則：and_intro_elim · 依賴：S06, S10, S11, S12, S13 葉節點依據：and_intro_elim 彙整：p=3(x+3)(x−2) 與 q=2(x−5)(x+5) 都通過逐係數比對；x²+25 不等於 (x−5)(x+5)，也沒有兩個一次因式的分解；x³ 與 x 在三點吻合仍是不同的多項式。 ## 局部子步與引理 S02.1 · equivalent操作前 (x+a)(x+b) 操作後 x\cdot x+x\cdot b+a\cdot x+a\cdot b 條件：無 規則：distributive · 依賴：distributive 葉節點依據：distributive 先把 (x+a) 分配到 (x+b)：(x+a)(x+b)=x(x+b)+a(x+b)，再各自分配，得四項 x·x、x·b、a·x、a·b。 S02.2 · equivalent操作前 x\cdot x+x\cdot b+a\cdot x+a\cdot b 操作後 x^2+(a+b)x+ab 條件：無 規則：like_terms · 依賴：S02.1, like_terms, mul_comm 葉節點依據：like_terms + mul_comm + add_comm x·x=x²；依乘法交換律 x·b=bx，與 ax 是同次項，合併為 (a+b)x；常數項是 ab。S02.1 與 S02.2 合起來證得引理 L_binom。 S07.1 · equivalent操作前 (x+(-d))(x+d) 操作後 x^2+(-d+d)x+(-d)d=x^2-d^2 條件：無 規則：L_binom · 依賴：S02 葉節點依據：L_binom + add_inverse + neg_mul 在 L_binom 中取 a=−d、b=d：一次項係數 −d+d=0，常數項 (−d)·d=−d²，所以 (x−d)(x+d)=x²−d²。這證得引理 L_diffsq。 S12.1 · implies操作前 x^2+25=(ux+v)(wx+t),\ u\neq 0 操作後 c=-\tfrac{v}{u}\in\mathbb{Q},\quad c^2+25=(uc+v)(wc+t)=0\cdot(wc+t)=0 條件：u\neq 0 規則：eval_hom · 依賴：eval_hom, mul_inverse_nonzero 葉節點依據：eval_hom + mul_inverse_nonzero + mul_zero 假設存在這樣的分解。因 u≠0，c=−v/u 是有理數，且 uc+v=−v+v=0。相等的多項式在 c 的值相同，求值又保持乘法（eval_hom），所以 c²+25=(uc+v)(wc+t)=0·(wc+t)=0。 S12.2 · implies操作前 c\in\mathbb{Q}\subseteq\mathbb{R} 操作後 c^2+25\geq 25>0 條件：無 規則：square_nonneg · 依賴：S12.1, square_nonneg, order_basics 葉節點依據：square_nonneg + order_basics c 是實數，依 square_nonneg，c²≥0；兩邊加 25 得 c²+25≥25>0，所以 c²+25≠0。 S12.3 · implies操作前 c^2+25=0\ \land\ c^2+25>0 操作後 \neg\exists\,u,v,w,t:\ x^2+25=(ux+v)(wx+t) 條件：無 規則：contradiction · 依賴：S12.1, S12.2 葉節點依據：contradiction + quantifier_negation S12.1 推出 c²+25=0，S12.2 推出 c²+25>0，矛盾。所以假設的分解不存在。S12.1 至 S12.3 合起來證得引理 L_no_linear_factor。同一論證把 c 換成實數也成立，所以 x²+25 連在 ℝ[x] 中也沒有一次因式；可分解性一般依賴係數域，例如 x²−2（見錯誤控制）。 ## 逐步反向審查 - S14 · sufficient_goal_reduction · S06, S10, S11, S12, S13, and_intro_elim — 目標 G：四項結論。足夠條件 H：S06、S10、S11、S12、S13 各自的結論；H⇒G 只是合取。H 由係數計算與反證正向證成，沒有把 G 當作前提。 - S13 · premise_audit · poly_eq_coeff, eval_hom, numeric_evaluation — 不等由係數證明，不靠代入；N13 只是三點的有限核對，N14 顯示第四點不同。「次數至多 d 的多項式在 d+1 個點相同即恆等」這個事實本稿沒有證明，只用來說明為何三點不夠。 - S12.3 · premise_audit · S12.1, S12.2, contradiction — 矛盾來自同一個 c 的兩個結論；反證假設在此釋放。 - S12.2 · premise_audit · square_nonneg, order_basics — 對每個實數 c 都成立，不是有限點核對；最小值 25 在 c=0 取得（N12）。 - S12.1 · premise_audit · eval_hom, mul_inverse_nonzero, mul_zero — 需要 u≠0 才能取 c=−v/u；這是在反證假設的作用域內推論。 - S12 · premise_audit · L_no_linear_factor, eval_hom, square_nonneg — 結論只針對兩個一次因式；把 x²+25 寫成 1·(x²+25) 這類含常數因子的寫法不算新的分解（MKO 假設 a2）。 - S11 · premise_audit · S09, poly_eq_coeff, numeric_evaluation — 一個係數不同就足以推出不等（N10、N11）；但這只否定這一個候選，是否有其他分解另見 S12。 - S10 · inverse_equivalence · eq_replace, poly_eq_coeff — 等值代換，雙向成立；三個係數全部比對。 - S09 · inverse_equivalence · L_diffsq, numeric_evaluation — 需要把常數寫成有理數的平方（N8）；恆等式雙向成立。 - S08 · inverse_equivalence · distributive, numeric_evaluation — 展開回到原式：2·1=2、2·(−25)=−50。 - S07.1 · inverse_equivalence · L_binom, add_inverse, neg_mul — 代入恆等式並化簡，每步都是等值代換。 - S07 · inverse_equivalence · L_diffsq — 恆等式雙向成立（N7）。注意它只適用於「差」：x²+d² 不在此列。 - S06 · inverse_equivalence · eq_replace, poly_eq_coeff — 等值代換雙向成立；公因子 3 必須保留，否則首項係數會變成 1。 - S05 · inverse_equivalence · L_binom, poly_eq_coeff — 引理是恆等式，代入特定 a、b 後仍雙向成立。 - S04 · premise_audit · S02, numeric_evaluation — 只核對這組候選（N4、N5）；不宣稱這是唯一或由某演算法求得。 - S03 · inverse_equivalence · distributive, poly_eq_coeff, numeric_evaluation — 展開 3(x²+x−6) 回到原式，三個係數逐一相同（N2、N3），雙向成立。 - S02.2 · inverse_equivalence · like_terms, mul_comm, add_comm — 合併同次項與把係數拆開互為反向，都是恆等式。 - S02.1 · inverse_equivalence · distributive — 分配律是恆等式，反向就是提出公因式。 - S02 · inverse_equivalence · L_binom — 兩邊是同一個多項式，可雙向代換；引理對所有有理 a、b 成立（N1 以次數界核對）。 - S01 · premise_audit · G1, mko_factorization, poly_eq_coeff — 此步只寫出判準；後面每個分解都依這個判準驗證。 ## 錯誤控制與反例 平方和不能套平方差MKO 指出的第一個誤解是把平方和套用平方差公式。(x−5)(x+5) 展開是 x²−25，不是 x²+25（S11）；而且 x²+25 根本沒有一次因式（S12），因為 c²+25 對每個實數 c 都是正數。 有限個點吻合不是恆等MKO 指出的第二個誤解是用有限數值吻合冒充沒有次數界證據的恆等式。x³ 與 x 在 −1、0、1 三點相同卻是不同多項式（S13）。本稿的每個分解都用逐係數比對驗證（S06、S10）；格點核對 N1、N6、N7、N9 依次數界設計，只作輔助。 係數域與公因子可分解性取決於係數域（MKO para2）：例如 x²−2 在 ℝ 中是 (x−√2)(x+√2)，在 ℚ 中則沒有一次因式（這依賴 √2 是無理數，本稿未證明）。另外，提出的公因子必須保留：3x²+3x−18 不等於 (x+3)(x−2)，因為後者首項係數是 1。因式分解也不是解方程，用零積性求根時還要指定數域。 - x²+25=(x−5)(x+5) → reject — 右邊展開為 x²−25，常數項 −25≠25。 - x³ 與 x 在 x=−1、0、1 取值相同，所以 x³=x 是多項式恆等式 → reject — x³ 的係數 1≠0；x=2 時 8≠2。 - 3x²+3x−18=(x+3)(x−2) → reject — (x+3)(x−2)=x²+x−6，首項係數 1≠3、常數項 −6≠−18；漏掉公因子 3。 - x²+x−6=(x−3)(x+2) → reject — (x−3)(x+2)=x²−x−6，一次項係數 −1≠1。 ## 結論與限制 在 ℚ[x] 中 3x²+3x−18=3(x+3)(x−2)，2x²−50=2(x−5)(x+5)，兩者都以展開後逐係數比對驗證。x²+25≠(x−5)(x+5)（常數項 25≠−25），而且 x²+25 不是兩個一次因式的乘積（否則 c²+25=0 有有理解）。x³ 與 x 在 −1、0、1 取值相同，但 x³≠x。 - 「x²−2 在 ℚ 中沒有一次因式」依賴 √2 的無理性，本稿只作說明，未證明。 - S04 的 a、b 是嘗試得到的候選；本稿不提供一般的因式分解演算法（MKO 明示不宣稱）。 - N13 只是三個點的有限核對，正是用來展示「有限吻合不足」；N1、N5 至 N10、N15 是依次數界設計的格點核對，作為係數比對的輔助。 ## 驗證及來源綁定 17 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 96eb7a6a6d15bd4bc31f1e82c3a0f24b1950d37ba0e48a4f3336de4395e33750 - original source SHA-256: 96eb7a6a6d15bd4bc31f1e82c3a0f24b1950d37ba0e48a4f3336de4395e33750 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-factorization-01.json)