# 分數：判定等值、化為最簡正分母形式與分數加法

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-fraction/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-fraction-01 · production-20261019-adopted-96



## 目標與範圍

(1) 判定 (−6)/(−8) 與 9/12 是否表示同一個有理數；(2) 把 (−6)/(−8) 化成最簡、正分母的表示，並說明數值不變；(3) 計算 3/4+5/6，並說明「分子加分子、分母加分母」得到的 8/10 不是和；(4) 說明 3/0 不是合法的分數表示。

在 MKO 的範圍內：分子分母為整數、分母非零（假設 a1），p/q 的數值是有理數 p·(1/q)。本稿由有理數的運算證明等值判準 ps=rq 與加法公式；不證明「每個有理數恰有一個最簡正分母表示」的一般唯一性（見開放項目）；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- mul_inverse_nonzero
- zero_product
- frac_rules
- mul_assoc
- mul_comm
- numeric_evaluation


- G1 — p、q、r、s 是整數，所有作為分母的數都非零（MKO 假設 a1）；q≠0 時 p/q 表示有理數 p·(1/q)。
- G2 — 要處理的表示：(−6)/(−8)、9/12、3/4、5/6、6/8，以及寫法 3/0。


- \frac{p}{q} — 分數表示，數值為 p·(1/q)
- ps=rq — 交叉乘積等式
- \gcd(m,n) — m、n 的最大公因數
- \mathbb{Q} — 有理數





## 規則與來源


- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- 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）。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- de_morgan_logic · prerequisite — 邏輯的德摩根律：¬(P∧Q) ⇔ ¬P∨¬Q；¬(P∨Q) ⇔ ¬P∧¬Q。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- modus_ponens · prerequisite — 肯定前件：由 P 與 P⇒Q 得 Q。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- 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_fraction_def · cited — 對整數 p、q 且 q≠0，p/q 表示有理數。兩個合法表示 p/q 與 r/s 等值，當且僅當 ps=rq；約分與正分母正規化改變表示而不改變數值。 · mko-fraction
- gcd_def · prerequisite — 對不全為 0 的整數 m、n，gcd(m,n) 是同時整除 m 與 n 的最大正整數；q>0 且 gcd(p,q)=1 時，稱 p/q 為最簡正分母形式。
- L_cross · lemma — 對整數 p、q、r、s，q≠0、s≠0：p/q=r/s ⇔ ps=rq。
- L_add · lemma — 對整數 p、q、r、s，q≠0、s≠0：p/q+r/s=(ps+rq)/(qs)。





## 逐步主鏈

S01 · definition操作前

\frac{-6}{-8},\ \frac{9}{12}

操作後

\text{valid representations, since}\ -8\neq 0,\ 12\neq 0

條件：-8\neq 0; 12\neq 0

規則：mko_fraction_def · 依賴：G1, G2, mko_fraction_def

葉節點依據：mko_fraction_def + numeric_evaluation

依 MKO，整數 p 與非零整數 q 寫成的 p/q 才是合法表示。兩個分母 −8 與 12 都不是 0，所以兩者都表示有理數。分子或分母是負數並不影響合法性。



S02 · equivalent操作前

\frac{-6}{-8}=\frac{9}{12}

操作後

(-6)\cdot 12=9\cdot(-8)

條件：-8\neq 0; 12\neq 0

規則：L_cross · 依賴：S01, L_cross

葉節點依據：L_cross

依引理 L_cross（p=−6、q=−8、r=9、s=12），兩個表示等值當且僅當交叉乘積相等。引理需要 q≠0 與 s≠0，S01 已確認。



S03 · equivalent操作前

(-6)\cdot 12=9\cdot(-8)

操作後

-72=-72

條件：無

規則：numeric_evaluation · 依賴：S02

葉節點依據：numeric_evaluation

精確計算兩個交叉乘積：(−6)·12=−72，9·(−8)=−72。兩邊相等，所以交叉乘積等式為真。



S04 · implies操作前

(-6)\cdot 12=9\cdot(-8)\ \text{true}

操作後

\frac{-6}{-8}=\frac{9}{12}

條件：無

規則：modus_ponens · 依賴：S02, S03

葉節點依據：modus_ponens + iff_intro

S02 的等價加上 S03 的「交叉乘積相等」，得 (−6)/(−8)=9/12：兩個分母不同、符號也不同的表示，表示同一個有理數。



S05 · equivalent操作前

\frac{-6}{-8}

操作後

\frac{(-6)(-1)}{(-8)(-1)}=\frac{6}{8}

條件：k=-1\neq 0

規則：frac_rules · 依賴：S01, frac_rules

葉節點依據：frac_rules + numeric_evaluation

正分母正規化：依 frac_rules（a/b=(ak)/(bk)，k≠0），分子分母同乘 k=−1，得 6/8，分母變成正數。核對：(−6)·8=−48=6·(−8)，依 L_cross 數值相同。



S06 · equivalent操作前

\frac{6}{8}

操作後

\frac{3\cdot 2}{4\cdot 2}=\frac{3}{4}

條件：k=2\neq 0

規則：frac_rules · 依賴：S05, gcd_def, frac_rules

葉節點依據：frac_rules + gcd_def + numeric_evaluation

約分：6 的正因數是 1、2、3、6，8 的正因數是 1、2、4、8，共同的最大者是 2，所以 gcd(6,8)=2。6=3·2、8=4·2，依 frac_rules（k=2≠0）得 6/8=3/4。



S07 · equivalent操作前

\frac{9}{12}

操作後

\frac{3\cdot 3}{4\cdot 3}=\frac{3}{4}

條件：k=3\neq 0

規則：frac_rules · 依賴：S04, gcd_def, frac_rules

葉節點依據：frac_rules + gcd_def + numeric_evaluation

gcd(9,12)=3（9 的正因數 1、3、9；12 的正因數 1、2、3、4、6、12），9=3·3、12=4·3，所以 9/12=3/4。兩個原表示都化到同一個 3/4，與 S04 一致。



S08 · implies操作前

\frac{3}{4}

操作後

4>0,\ \gcd(3,4)=1:\ \text{lowest terms, positive denominator}

條件：無

規則：gcd_def · 依賴：S06, S07, gcd_def

葉節點依據：gcd_def + divides_def + numeric_evaluation

3 的正因數是 1 與 3，而 3 不整除 4，所以 gcd(3,4)=1；分母 4>0。因此 3/4 是最簡正分母形式。(−6)/(−8)、6/8、9/12、3/4 是同一個數值的四種表示：MKO 所說的約分與正規化只改變表示，不改變數值。



S09 · equivalent操作前

\frac{3}{4}+\frac{5}{6}

操作後

\frac{3\cdot 6+5\cdot 4}{4\cdot 6}=\frac{38}{24}

條件：4\neq 0; 6\neq 0

規則：L_add · 依賴：L_add

葉節點依據：L_add + numeric_evaluation

依引理 L_add（p=3、q=4、r=5、s=6）：分子 3·6+5·4=18+20=38，分母 4·6=24。



S10 · equivalent操作前

\frac{38}{24}

操作後

\frac{19\cdot 2}{12\cdot 2}=\frac{19}{12}

條件：k=2\neq 0

規則：frac_rules · 依賴：S09, gcd_def, frac_rules

葉節點依據：frac_rules + gcd_def + numeric_evaluation

gcd(38,24)=2：38=2·19，19 是質數且不整除 24，所以共同正因數只有 1 與 2。38=19·2、24=12·2，約分得 19/12；gcd(19,12)=1，分母 12>0，這是最簡正分母形式。所以 3/4+5/6=19/12。



S11 · implies操作前

\frac{3+5}{4+6}=\frac{8}{10}\ \text{vs}\ \frac{19}{12}

操作後

8\cdot 12=96\neq 190=19\cdot 10,\ \text{so}\ \frac{8}{10}\neq\frac{19}{12}

條件：10\neq 0; 12\neq 0

規則：L_cross · 依賴：S10, L_cross

葉節點依據：L_cross + contrapositive + numeric_evaluation

「分子加分子、分母加分母」得 8/10。依 L_cross，8/10=19/12 當且僅當 8·12=19·10；但 96≠190，所以 8/10≠19/12。這個文字操作不是分數加法（MKO 第三段）。



S12 · implies操作前

\frac{6}{8}\ (=\tfrac{3}{4})\ \text{and}\ \frac{5}{6}

操作後

\frac{6+5}{8+6}=\frac{11}{14}\neq\frac{8}{10},\quad \frac{6\cdot 6+5\cdot 8}{8\cdot 6}=\frac{76}{48}=\frac{19}{12}

條件：8\neq 0; 6\neq 0; 14\neq 0; 48\neq 0

規則：L_cross · 依賴：S05, S06, L_cross, L_add

葉節點依據：L_cross + L_add + numeric_evaluation

把 3/4 換成等值的 6/8 再做文字操作，得 11/14；而 11·10=110≠112=8·14，所以 11/14≠8/10。同一對數值給出兩個不同結果，說明文字操作根本不是數的運算，只依賴寫法。真正的加法 L_add 給 76/48，且 76·12=912=19·48，仍等於 19/12：結果只依賴數值。



S13 · implies操作前

\frac{3}{0}

操作後

\text{not a valid representation: } 0\ \text{has no inverse}

條件：無

規則：mul_inverse_nonzero · 依賴：G1, mul_inverse_nonzero, mko_fraction_def

葉節點依據：mul_inverse_nonzero + mul_zero + mko_fraction_def

3/0 應表示 3·(1/0)，但 0 沒有倒數（對任何 t，0·t=0≠1），所以 3/0 不表示任何有理數，也不是「零」。MKO 只對 q≠0 定義 p/q。L_cross 也只對非零分母成立：若硬套到 3/0 與 6/0，交叉乘積 3·0=0=6·0 相等，卻沒有任何數值可比。



S14 · implies操作前

S04,\ S08,\ S10,\ S11,\ S13

操作後

\frac{-6}{-8}=\frac{9}{12}=\frac{3}{4},\ \ \frac{3}{4}+\frac{5}{6}=\frac{19}{12}\neq\frac{8}{10},\ \ \frac{3}{0}\ \text{invalid}

條件：無

規則：and_intro_elim · 依賴：S04, S08, S10, S11, S13

葉節點依據：and_intro_elim

四個目標分別由 S04（等值）、S05 到 S08（正規化，數值不變）、S09 到 S11（加法與錯誤的文字操作）與 S13（零分母）完成。







## 局部子步與引理

S02.1 · implies操作前

q\neq 0,\ s\neq 0

操作後

qs\neq 0

條件：無

規則：zero_product · 依賴：zero_product

葉節點依據：zero_product + de_morgan_logic

依零乘積性質，qs=0 ⇔ q=0 或 s=0。兩者都不成立，所以 qs≠0，因此 1/(qs) 存在。



S02.2 · implies操作前

\frac{p}{q}=\frac{r}{s}

操作後

ps=rq

條件：q\neq 0; s\neq 0

規則：eq_congruence · 依賴：G1, eq_congruence, mul_inverse_nonzero

葉節點依據：eq_congruence + mul_inverse_nonzero + mul_assoc + mul_comm + mul_one

兩邊同乘 qs：左邊 p·(1/q)·q·s=p·1·s=ps，右邊 r·(1/s)·q·s=r·q·(s·(1/s))=rq（結合律、交換律、q·(1/q)=1、s·(1/s)=1）。所以 ps=rq。



S02.3 · implies操作前

ps=rq

操作後

\frac{p}{q}=\frac{r}{s}

條件：qs\neq 0

規則：eq_congruence · 依賴：S02.1, eq_congruence, frac_rules

葉節點依據：eq_congruence + frac_rules + mul_comm

依 S02.1，qs≠0，兩邊同乘 1/(qs)：左邊 (ps)/(qs)=p/q（frac_rules，消去非零的 s），右邊 (rq)/(qs)=(rq)/(sq)=r/s（交換律後消去非零的 q）。所以 p/q=r/s。S02.1 到 S02.3 合起來證得引理 L_cross。



S09.1 · equivalent操作前

\frac{p}{q}+\frac{r}{s}

操作後

\frac{ps}{qs}+\frac{rq}{qs}

條件：q\neq 0; s\neq 0

規則：frac_rules · 依賴：frac_rules, mul_comm

葉節點依據：frac_rules + mul_comm

依 frac_rules 的擴分（k≠0）：p/q=(ps)/(qs)（k=s≠0），r/s=(rq)/(sq)=(rq)/(qs)（k=q≠0，再用交換律 sq=qs）。兩個分數現在有相同的分母 qs。



S09.2 · equivalent操作前

\frac{ps}{qs}+\frac{rq}{qs}

操作後

\frac{ps+rq}{qs}

條件：qs\neq 0

規則：frac_rules · 依賴：S09.1, S02.1, frac_rules

葉節點依據：frac_rules + distributive

同分母相加：a/c+b/c=(a+b)/c，其中 c=qs≠0（S02.1）。S09.1 與 S09.2 合起來證得引理 L_add。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S04, S08, S10, S11, S13, and_intro_elim — 目標 G：(1) 到 (4)。足夠條件 H：S04、S08、S10、S11、S13 各自成立；H⇒G 由合取引入。H 由引理與精確計算正向證成，沒有把 G 當作前提。
- S13 · premise_audit · mul_inverse_nonzero, mko_fraction_def — 結論只說 3/0 不是合法表示；不宣稱交叉乘積可用來替它賦值。
- S12 · premise_audit · L_cross, L_add, S06 — 所有比較都經 L_cross，且所用分母 8、6、10、14、48、12 都非零。
- S11 · premise_audit · L_cross, S10, numeric_evaluation — 用的是 L_cross 的逆否：交叉乘積不等推出數值不等；兩個分母 10、12 都非零。
- S10 · inverse_equivalence · frac_rules, gcd_def — 約分改變表示不改變數值；N11 到 N13 重算。
- S09.2 · inverse_equivalence · frac_rules, S02.1 — 這是對所有非零 c 成立的恆等式，雙向成立。
- S09.1 · inverse_equivalence · frac_rules, mul_comm — 擴分與約分互為反運算，需要 s≠0 與 q≠0。
- S09 · inverse_equivalence · L_add — 引理是兩個數相等的恆等式，兩邊表示同一個有理數，雙向成立；引理在 S09.1、S09.2 證明。
- S08 · premise_audit · gcd_def, S06, S07 — 此步只宣稱 3/4 滿足最簡正分母的條件；不宣稱一般有理數的最簡表示唯一（那需要另外的定理）。
- S07 · inverse_equivalence · frac_rules, gcd_def — 反向是同乘 3；k=3≠0。
- S06 · inverse_equivalence · frac_rules, gcd_def — 反向是分子分母同乘 2；兩向都只用 k=2≠0。
- S05 · inverse_equivalence · frac_rules, L_cross — 反向再乘一次 −1 即回到原表示；需要 k≠0。
- S04 · premise_audit · S02, S03, modus_ponens — 結論來自交叉乘積，不是看分母是否相同。
- S03 · inverse_equivalence · numeric_evaluation — 精確求值不改變等式的真假（N1、N2）。
- S02.3 · premise_audit · S02.1, frac_rules, eq_congruence — 乘以 1/(qs) 需要 qs≠0；若容許零分母，ps=rq 不能推回任何數值關係（見錯誤控制二）。
- S02.2 · premise_audit · eq_congruence, mul_inverse_nonzero, mul_assoc, mul_comm — 化簡需要 1/q、1/s 存在，即 q≠0、s≠0。這是 ⇒ 方向；⇐ 方向在 S02.3。
- S02.1 · premise_audit · zero_product — 需要兩個分母各自非零；只要一個是 0，qs 就是 0。
- S02 · inverse_equivalence · L_cross, S01 — 引理兩個方向都在 S02.2、S02.3 證明。
- S01 · premise_audit · G1, mko_fraction_def — 此步只核對合法性條件（分母非零），不推出數值關係。





## 錯誤控制與反例

分母不同不代表數值不同MKO 指出分數的字面表示不唯一。(−6)/(−8)、6/8、9/12、3/4 的分母各不相同，數值卻相同。判定兩個表示是否等值，要比較交叉乘積 ps 與 rq（L_cross），而不是比較分子或分母。

零分母不表示零MKO 指出零分母不表示零。0/5 是零（分子為零、分母非零），但 3/0 根本不是表示，因為 0 沒有倒數。交叉乘積判準只在分母非零時成立：若對 3/0 與 6/0 硬套，3·0=6·0 會「證明」兩者相等，這是無意義的。

分子加分子、分母加分母不是分數加法3/4 與 5/6 用文字操作得 8/10，但真正的和是 19/12，且 8·12=96≠190=19·10。更糟的是，把 3/4 寫成 6/8 再操作得 11/14≠8/10：結果依賴寫法，所以它不是數的運算。正確公式是 p/q+r/s=(ps+rq)/(qs)（L_add）。


- 9/12 與 (−6)/(−8) 的分母不同，所以數值不同 → reject — (−6)·12=−72=9·(−8)，依 L_cross 兩者相等。
- 3/0=0 → reject — 0 沒有倒數，3/0 不是合法表示；零值的表示是像 0/5 這樣分子為零、分母非零的分數。
- 3/4+5/6=(3+5)/(4+6)=4/5 → reject — 和是 19/12；4·12=48≠95=19·5。
- 因為 3·0=6·0，所以 3/0=6/0 → reject — L_cross 需要分母非零；3/0、6/0 不表示任何數。





## 結論與限制

(−6)/(−8)=9/12，因為 (−6)·12=−72=9·(−8)；它的最簡正分母形式是 3/4，約分與正規化只改變表示。3/4+5/6=(18+20)/24=38/24=19/12，而「分子分母分別相加」的 8/10 不等於 19/12，且結果隨寫法改變。3/0 不是合法表示，零分母不表示零。


- 本稿只驗證 3/4 與 19/12 是最簡正分母形式，沒有證明一般的唯一性（每個有理數恰有一個最簡正分母表示）；那需要歐幾里得引理或貝祖等式，留給後續。
- N17 是 p、q、k 的多項式恆等式核對，說明擴分保持交叉乘積相等；它補充 S05、S06，論證不依賴它。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
- original source SHA-256: 6d3a1d5f7536f8c32b52e78378a872546ab4eeaf24030466909289ff9ffaa771
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-fraction-01.json)