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

目標與範圍

(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)。

逐步主鏈

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

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

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

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

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

-72=-72

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

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

\frac{-6}{-8}

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

\frac{6}{8}

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

\frac{9}{12}

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

\frac{3}{4}

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

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

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

\frac{38}{24}

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

\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}

\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}

\frac{3}{0}

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

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}

局部子步與引理

q\neq 0,\ s\neq 0

qs\neq 0

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

ps=rq

ps=rq

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

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

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

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

\frac{ps+rq}{qs}

逐步反向審查

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