有理係數多項式因式分解：以係數比對驗證提公因子、二項式乘積與平方差

目標與範圍

在 ℚ[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 — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• 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] 中不是兩個一次因式的乘積。

逐步主鏈

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

(x+a)(x+b)

x^2+(a+b)x+ab

3x^2+3x-18

3(x^2+x-6)

a=3,\ b=-2

a+b=3+(-2)=1,\ ab=3\cdot(-2)=-6

(x+3)(x-2)

x^2+(3+(-2))x+3\cdot(-2)=x^2+x-6

3x^2+3x-18

3(x+3)(x-2)

(x-d)(x+d)

x^2-d^2

2x^2-50

2(x^2-25)

x^2-25

(x-5)(x+5)

2x^2-50

2(x-5)(x+5)

x^2+25\ \text{vs.}\ (x-5)(x+5)

(x-5)(x+5)=x^2-25\neq x^2+25

x^2+25=(ux+v)(wx+t),\ u\neq0,\ w\neq0

\text{impossible in}\ \mathbb{Q}[x]

x^3\ \text{and}\ x\ \text{at}\ x=-1,0,1

\text{equal values, but}\ x^3\neq x\ \text{in}\ \mathbb{Q}[x]

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

局部子步與引理

(x+a)(x+b)

x\cdot x+x\cdot b+a\cdot x+a\cdot b

x\cdot x+x\cdot b+a\cdot x+a\cdot b

x^2+(a+b)x+ab

(x+(-d))(x+d)

x^2+(-d+d)x+(-d)d=x^2-d^2

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

c\in\mathbb{Q}\subseteq\mathbb{R}

c^2+25\geq 25>0

c^2+25=0\ \land\ c^2+25>0

\neg\exists\,u,v,w,t:\ x^2+25=(ux+v)(wx+t)

逐步反向審查

• 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、反控制與修訂記錄）