方程式：在定義域內解 x²/(x−1)=1/(x−1)

目標與範圍

在允許範圍 ℝ 中，求方程 x²/(x−1)=1/(x−1) 的解集；並說明為什麼兩邊乘以 x−1 後得到的方程 x²=1 有兩個解，而原方程只有一個。

依 MKO 的定義：解集由使兩側都有定義且相等的允許 x 組成。只處理一個含分式的實數方程，示範定義域、乘以非零式的等價變形、零乘積、排除候選值與代回核對。不處理一般有理方程的理論或複數解；不改動 canonical MKO 或英文 edition。

已知條件與符號

• mul_inverse_nonzero
• eq_congruence
• distributive
• zero_product
• set_builder
• numeric_evaluation

• G1 — 允許範圍與運算：變數 x 取值於 ℝ；使用實數的加、減、乘、除，v/u 只在 u≠0 時有定義（mul_inverse_nonzero）。
• G2 — 方程：L(x)=R(x)，其中 L(x)=x²/(x−1)，R(x)=1/(x−1)。
• G3 — 解集的定義（MKO）：𝒮={x∈ℝ ∣ L(x) 與 R(x) 都有定義且 L(x)=R(x)}。

• L(x)=\frac{x^2}{x-1} — 左側表達式
• R(x)=\frac{1}{x-1} — 右側表達式
• D — 兩側都有定義的 x 所成的集合
• \mathcal{S} — 原方程的解集
• u\neq 0 — 非零條件；除以 u 或使用 1/u 都需要它

規則與來源

• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_equation · cited — 給定兩個具有共同語境的表達式 L(x)、R(x)，方程式 L(x)=R(x) 的解集由所有使兩側皆有定義且值相等的允許 x 組成。 · mko-equation
• L_zero_diff · lemma — 對實數 u、c：u−c=0 ⇔ u=c。
• L_den · lemma — 對實數 a、b 與 u≠0：a/u=b/u ⇔ a=b。

逐步主鏈

L(x)=R(x)\ \text{over}\ \mathbb{R}

\mathcal{S}=\{x\in\mathbb{R}\mid L(x),R(x)\ \text{defined}\ \land\ L(x)=R(x)\}

L(x)\ \text{and}\ R(x)\ \text{defined}

x-1\neq 0

x-1\neq 0

x\neq 1;\quad D=\{x\in\mathbb{R}\mid x\neq 1\}

\frac{x^2}{x-1}=\frac{1}{x-1},\ x\in D

x^2=1,\ x\in D

x^2=1

x^2-1=0

x^2-1=0

(x-1)(x+1)=0

(x-1)(x+1)=0

x-1=0\ \lor\ x+1=0

x-1=0\ \lor\ x+1=0

x=1\ \lor\ x=-1

x\in D:\ L(x)=R(x)

\mathcal{S}=\{x\in\mathbb{R}\mid x\in D\ \land\ (x=1\lor x=-1)\}

x=1

1\notin D,\ \text{so}\ 1\notin\mathcal{S}

x=-1

-1\in D,\ \text{so}\ -1\in\mathcal{S}

x\in\mathcal{S}\iff x\in D\land(x=1\lor x=-1)

\mathcal{S}=\{-1\}

x=-1\ \text{in}\ L,\ R

L(-1)=\frac{1}{-2}=-\tfrac{1}{2}=R(-1)

\{x\in\mathbb{R}\mid x^2=1\}

\{-1,1\}\supsetneq\mathcal{S}=\{-1\}

\mathcal{S}=\{-1\},\ \{x\mid x^2=1\}=\{-1,1\}

\text{answer: }\mathcal{S}=\{-1\};\ 1\ \text{excluded since}\ 1\notin D

局部子步與引理

u-c=0

(u-c)+c=0+c

(u-c)+c=0+c

u=c

\frac{a}{u}=\frac{b}{u}

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

\frac{a}{u}\cdot u=\frac{b}{u}\cdot u

a=b

逐步反向審查

• S15 · sufficient_goal_reduction · S12, S13, S14, and_intro_elim — 目標 G：求 𝒮 並說明 x²=1 多出的解。足夠條件 H：S12（𝒮={−1}）與 S14（多出的解來自 x−1=0）；H⇒G 直接成立。H 由 G1 到 G3 正向證成，沒有把 G 當作前提；S13 是獨立核對。
• S14 · premise_audit · S05, S08, S12, set_extensionality — 兩集合只差 1，而 1∉D；這解釋了差異，但不宣稱乘以任何式子都只會多出乘數的零點以外沒有別的影響。
• S13 · premise_audit · S12, G2, numeric_evaluation — 這是對 x=−1 的獨立核對；它確認 −1 是解，但不能單獨證明沒有其他解，那由 S04 到 S12 的等價鏈負責。
• S12 · premise_audit · S10, S11, set_extensionality, case_analysis — 需要兩個包含：𝒮⊆{−1} 用 S10 排除 x=1，{−1}⊆𝒮 用 S11。
• S11 · premise_audit · S03, S09, set_builder — 兩個合取項都檢查了：x∈D 與 x=1∨x=−1。
• S10 · premise_audit · S03, S09, set_builder — 只需 1 不滿足合取項 x∈D；不必（也無法）計算兩側的值。
• S09 · inverse_equivalence · logic_chain, S04, S08 — 每一環都是雙向的，而且 S04 只在 x∈D 中使用；所以串起來的等價也只在 D 中成立，並把 x∈D 保留在集合條件裡。
• S08 · inverse_equivalence · L_zero_diff, numeric_evaluation — 代回：1−1=0、(−1)+1=0；兩支都是雙向等價。
• S07 · inverse_equivalence · zero_product — 向前需要 ℝ 沒有零因子；向後用 u·0=0。兩個方向都包含在 zero_product 中。
• S06 · inverse_equivalence · distributive, eq_replace — 這是對所有實數成立的恆等式（N4 是獨立的多項式核對），等值代換雙向成立。
• S05 · inverse_equivalence · L_zero_diff — 引理兩向都已證；這一步對每個實數成立，不依賴 x∈D。
• S04.2 · inverse_equivalence · mul_assoc, mul_comm, mul_inverse_nonzero, mul_one — 等值代換雙向成立；(1/u)u=1 需要 u≠0。
• S04.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, mul_assoc — 向後乘以 1/u 需要 u≠0。若 u=0，a/u 與 b/u 原本就未定義，不能先乘 0 再把它們算成 0。另對已定義的實數式，乘以 0 雖會把兩邊變成 0，卻會失去原式資訊；這是另一個警告，不是本步在 u=0 的求值。
• S04 · inverse_equivalence · L_den, S03 — 反向是兩邊同乘 1/(x−1)，需要 x−1≠0；在 D 之外（x=1）反向不能做，所以這裡一直帶著「x∈D」。
• S03.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — 只把式子換成相等的式子，等式真假不變，雙向成立。
• S03.1 · inverse_equivalence · eq_congruence, add_inverse — 加 c 與加 −c 互為反運算，對任何實數都可做，沒有附加條件。
• S03 · inverse_equivalence · L_zero_diff — 等價的兩邊同取否定仍是等價；引理的兩個方向都在子步證明。
• S02 · inverse_equivalence · mul_inverse_nonzero — 若 x−1≠0，1/(x−1) 存在，兩側都有定義；若 x−1=0，兩側都含除以 0，都沒有定義。兩個方向都有理由。
• S01 · premise_audit · G1, G2, G3, mko_equation — 此步只寫出解集的定義，不推出新事實。

錯誤控制與反例

乘以可能為零的式子

MKO 列出的誤解包括「乘零後仍宣稱解集不變」與「除以可能為零的式子」。兩邊乘以 x−1 只在 x−1≠0 時是等價變形（S04）；在 x=1 處乘數為 0，變形不可逆，x²=1 因而多出解 1（S14）。正確做法是先寫出定義域 D={x ∣ x≠1}，並在整條等價鏈中保留 x∈D。

求得候選值後要代回原式

MKO 提醒求得候選值後要代回原式檢查。候選值 1 代入原式時兩側都是除以 0，沒有定義，所以不是解（S10）；候選值 −1 代入後兩側都是 −1/2（S13）。只把候選值代入 x²=1 檢查會錯把 1 當成解，因為 x²=1 已經不是原方程。

約分也不能丟掉定義域

類似的方程 (x²−1)/(x−1)=2，若先約分寫成 x+1=2，會得 x=1；但 x=1 時左側除以 0，沒有定義。約分 (x²−1)/(x−1)=x+1 只在 x≠1 時成立，所以這個方程的解集是空集。只化簡一側時，必須連同它成立的條件一起帶著。

• 原方程的解集是 {−1,1} → reject — x=1 時 1−1=0，兩側都沒有定義，1∉𝒮（S10）。
• x=1 是解，因為 1²=1 → reject — 那是在檢查 x²=1，不是原方程；原方程在 x=1 兩側都沒有定義。
• 兩邊同乘一個式子永遠不改變解集 → reject — x=2 兩邊乘 0 得 0=0，解集從 {2} 變成 ℝ；本題乘以 x−1 也多出解 1（S14）。
• x²/(x−1) 本身就是一個方程 → reject — 它沒有等號，只是一個表達式（方程的一側）；沒有另一側就沒有解集。

結論與限制

在 ℝ 中，x²/(x−1)=1/(x−1) 的解集是 {−1}。兩側只在 x≠1 時有定義；在這個範圍內方程等價於 x²=1，即 x=1 或 x=−1，而 x=1 不在定義域內。兩邊乘以 x−1 後的方程 x²=1 有解 {−1,1}，多出的 1 正是乘數 x−1 為零之處。

• 本稿只處理一個具體方程；一般有理方程（多個分母、高次分子）需要同樣的定義域追蹤，但不在此證明。
• 零乘積性質與分式規則以規則表中的前提使用，不在此由域公理推出。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 70e4d5766cd19e87cc7a8b9f5a847402b534f1a14a56165b9364b027e1664496
• original source SHA-256: 105cc4d24c32a42632c2fa35bdefc5573f9ebff81adc1112f41ccac5a8a97832
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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