有理數：同一個有理數的不同分數表示、交叉相乘與約分

目標與範圍

依 MKO 的定義（存在整數 p、q，q≠0，使 x=p/q），證明 6/(−8)、−3/4、9/(−12) 表示同一個有理數，並把 6/(−8) 精確約成正規形式 −3/4；以交叉相乘證明 2/3≠3/5；說明「5/0」不表示任何數；說明有限小數 −1.25=−5/4 與整數 7=7/1 都是有理數；並在分母為正時用交叉相乘證明 −3/4<−2/3。

在 ℝ 中討論分數（p/q 定義為 p·(1/q)），只用域的運算與序。證明兩個引理：分母非零時以交叉相乘判定相等，分母為正時以交叉相乘判定大小。不證明正規形式（既約且分母為正）的唯一性，不處理與 Lean Rat.divInt 的對接；不改動 canonical MKO 或英文 edition。

已知條件與符號

• mul_inverse_nonzero
• frac_rules
• zero_product
• order_basics
• numeric_evaluation

• G1 — 在實數 ℝ 中討論，整數 ℤ⊆ℝ；對 q≠0，p/q 表示 p·(1/q)；0 沒有倒數。
• G2 — MKO 的定義：數 x 是有理數，若存在整數 p、q，q≠0，使 x=p/q（假設 a1、a2）。
• G3 — 正規顯示慣例（MKO 說明）：分子與分母互質（最大公因數為 1），且分母為正。
• G4 — 資料：6/(−8)、−3/4、9/(−12)、2/3、3/5、字串「5/0」、有限小數 −1.25、整數 7、−2/3。

• \mathbb{Q} — 有理數集合
• \frac{p}{q} — p·(1/q)，q≠0
• (p,q) — 表示有理數的一對整數
• \gcd(a,b) — 最大公因數
• k — 約分時分子分母同乘的非零數

規則與來源

• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。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）。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=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。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_rat_def · cited — 數 x 是有理數，若存在整數 p、q 且 q≠0，使 x=p/q。不同整數對可以表示同一個有理數。 · mko-rational-number
• canonical_def · prerequisite — 正規形式：p/q 中 gcd(|p|,q)=1 且 q>0。
• gcd_def · prerequisite — 整數 a、b 不全為 0 時，gcd(a,b) 是同時整除 a 與 b 的最大正整數。
• decimal_def · prerequisite — 有限小數：整數部分加上小數點後第 j 位數字乘以 10^{−j} 之和；例如 1.25=1+2/10+5/100。
• L_cross · lemma — 對實數 p、q、r、s，q≠0、s≠0：p/q=r/s ⇔ ps=rq。
• L_cross_order · lemma — 對實數 p、q、r、s，q>0、s>0：p/q<r/s ⇔ ps<rq。

逐步主鏈

x\in\mathbb{Q}

\exists p,q\in\mathbb{Z},\ q\neq 0:\ x=\frac{p}{q}

\frac{p}{q}=\frac{r}{s}\quad(q\neq0,\ s\neq0)

ps=rq

6\cdot 4=24=(-3)\cdot(-8)

\frac{6}{-8}=\frac{-3}{4}

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

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

\frac{6}{-8}

\frac{6\cdot(-\frac12)}{(-8)\cdot(-\frac12)}=\frac{-3}{4}

\frac{-3}{4}

\gcd(3,4)=1,\ 4>0:\ \text{canonical form}

2\cdot5=10\neq 9=3\cdot3

\frac{2}{3}\neq\frac{3}{5}

x\cdot 0=5\ \text{for some}\ x

0=5,\ \text{a contradiction}

-1.25

-\frac{125}{100}=-\frac{5}{4}\in\mathbb{Q}

n\in\mathbb{Z}

n=\frac{n}{1}\in\mathbb{Q}

(-3)\cdot3=-9<-8=(-2)\cdot4

\frac{-3}{4}<\frac{-2}{3}

\text{S04, S06 to S11}

\tfrac{6}{-8}=\tfrac{9}{-12}=\tfrac{-3}{4};\ \tfrac{2}{3}\neq\tfrac{3}{5};\ -1.25,\ 7\in\mathbb{Q};\ \tfrac{-3}{4}<\tfrac{-2}{3}

局部子步與引理

q\neq 0,\ s\neq 0

qs\neq 0,\ \frac{p}{q}\cdot qs=ps,\ \frac{r}{s}\cdot qs=rq

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

ps=rq

q>0,\ s>0,\ \frac{p}{q}<\frac{r}{s}

ps<rq

逐步反向審查

• S12 · sufficient_goal_reduction · S03, S04, S05, S06, S07, S08, S09, S10, S11 — 目標是 goal 所列各項。足夠條件 H：S03 到 S11 各自成立；H 推出目標只用合取。每一項都由定義、兩個引理與精確計算正向證成，沒有把目標當作前提。
• S11.1 · inverse_equivalence · order_basics, S02.1, mul_inverse_nonzero — 乘以正數 qs 與乘以正數 1/(qs) 都保持不等號方向，互為反運算。
• S11 · inverse_equivalence · L_cross_order, numeric_evaluation — 本稿在兩個分母都為正的前提下證明此雙條件；這是已證明的適用範圍，不表示其他符號情形一律不成立。
• S10 · premise_audit · exists_intro, mul_one, forall_intro — 反向（每個有理數都是整數）不成立，例如 −5/4 不是整數。
• S09 · premise_audit · decimal_def, exists_intro, L_cross, numeric_evaluation — 存在性只需一對 (p,q)；約分是另外的等式。
• S08 · premise_audit · mul_zero, contradiction, mul_inverse_nonzero — 矛盾來自 x·0=0 對所有 x 成立；這正是 0 沒有倒數的原因。
• S07 · inverse_equivalence · L_cross, numeric_evaluation — P⇔Q 與 ¬P⇔¬Q 等價（N10）。
• S06 · premise_audit · gcd_def, canonical_def, divides_def — 只檢查 −3/4 是正規形式；正規形式的唯一性不在本稿證明（開放項目）。
• S05 · inverse_equivalence · frac_rules, numeric_evaluation — 反向：分子分母同乘 −2 回到 6/(−8)；k≠0 是規則的條件。
• S04 · inverse_equivalence · L_cross, numeric_evaluation, eq_refl_symm_trans — 每個相等都由雙條件得到，並以等號傳遞連起來（N4 到 N6）。
• S03 · inverse_equivalence · L_cross, numeric_evaluation — L_cross 是雙條件；計算可重算（N1、N2、N3）。
• S02.2 · inverse_equivalence · eq_congruence, mul_inverse_nonzero, S02.1 — 乘 qs 與乘 1/(qs) 互為反運算，前提 qs≠0。
• S02.1 · premise_audit · zero_product, mul_inverse_nonzero, mul_assoc, mul_comm — 需要 q≠0 與 s≠0，才有 1/q 與 1/s。
• S02 · inverse_equivalence · L_cross — 引理是雙條件，兩個方向都在子步證明；分母非零不可省。
• S01 · premise_audit · mko_rat_def, G1 — q≠0 是定義的一部分（假設 a2），不能省略；q=0 時 p/q 沒有定義。

錯誤控制與反例

分母不可為零

MKO 指出的誤解之一是允許零分母。「5/0」看起來像分數，但若它是某個數 x，就要有 x·0=5，而 x·0 永遠是 0（S08）。所以 (5,0) 不表示任何有理數；相對地，0/5=0 是合法的有理數。

外觀不同的分數可以相等

MKO 的另一誤解是把不同分數外觀當成不同數值。6/(−8)、−3/4、9/(−12) 看起來不同，卻是同一個有理數（S03、S04）；判定要用交叉相乘 L_cross，而不是比較分子或分母。比較大小時還要先讓分母為正：1/(−2) 與 1/3 若直接交叉相乘，1·3=3>−2=1·(−2) 會誤判 1/(−2)>1/3，事實上 −1/2<1/3（N18、N19）。

約分是精確等式，不是近似

MKO 提醒不要把約分視為近似。6/(−8)=−3/4 由 a/b=(ak)/(bk)（k≠0）得到，是精確等式（S05）。真正改變數值的是四捨五入：把 −0.75 寫成 −0.8，而 −0.8≠−3/4（N21）。

• 5/0 是有理數，因為 5 與 0 都是整數 → reject — 定義要求 q≠0；而且沒有任何數 x 滿足 x·0=5（S08）。
• 6/(−8) 與 −3/4 外觀不同，所以是不同的有理數 → reject — 交叉乘積 6·4=24=(−3)·(−8)，依 L_cross 兩者相等（S03）。
• 把 6/(−8) 約成 −3/4 只是近似 → reject — a/b=(ak)/(bk)（k=−1/2≠0）是精確等式（S05）。
• 因為 1·3>1·(−2)，所以 1/(−2)>1/3 → reject — L_cross_order 需要分母為正；事實上 −1/2<1/3（N19）。

結論與限制

6/(−8)、−3/4、9/(−12) 是同一個有理數（交叉乘積 24=24、−72=−72），正規形式為 −3/4（gcd(3,4)=1，分母為正），約分是精確等式；2/3≠3/5（10≠9）；「5/0」不表示任何數；−1.25=−125/100=−5/4 與 7=7/1 都是有理數；分母為正時 −3/4<−2/3（−9<−8）。

• 本稿只檢查 −3/4 是正規形式，不證明每個有理數恰有一個正規形式（唯一性需要例如歐幾里得引理）。
• 與 Lean Rat.divInt、非零分母與正規化分子分母聲明的對接（MKO formal next）未在此處理。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 7082af66df1018fc25b71890f73e46bebc2e117da1918db747a20e274bd8bc19
• original source SHA-256: b6cd86f150bfd74850fefee9d1f793b0b5d8bf486f024406abf8d1a96e33ec1f
• Lean: NOT_RUN · independent AI: NOT_MEASURED

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