# 比與比例：解 3:4=x:10、代回核對與檢查正比例資料

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

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

derivation-mko-ratio-proportion-01 · production-20261019-adopted-96



## 目標與範圍

在有理數中：(1) 證明對 b≠0、d≠0，比例 a:b=x:d 恰有一個有理解 x=ad/b；(2) 用它解 3:4=x:10 並代回核對；(3) 說明 4:3=x:10 的解不同，比的順序有意義；(4) 判定資料 (2,5)、(4,10)、(6,15)、(8,21) 是否符合同一個正比例 y=kx。

在 MKO 的範圍內：有理數的數值比，後項 b、d 非零（假設 a1）。資料是不帶單位的純數；若描述量，須先指定單位與可比較性（假設 a2）。本稿不由數值比例推出幾何相似或因果關係；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


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


- G1 — a、b、c、d、x 是有理數，且 b≠0、d≠0（MKO 假設 a1）。
- G2 — 數值比 a:b 的值是 a/b；比例 a:b=c:d 表示 a/b=c/d。
- G3 — 資料表 (xᵢ,yᵢ)：(2,5)、(4,10)、(6,15)、(8,21)。「資料符合正比例 y=kx」的意思是：存在同一個有理數 k，使每一筆都有 yᵢ=k·xᵢ。


- a:b — 數值比，值為 a/b（b≠0）
- a:b=c:d — 比例，意即 a/b=c/d
- x — 比例中的未知項
- k — 正比例 y=kx 的比例常數
- (x_i,y_i) — 第 i 筆資料





## 規則與來源


- 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）。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- iff_intro · prerequisite — 雙條件：P⇒Q 與 Q⇒P 都成立時，P⇔Q 成立；反之亦然。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- 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_ratio_def · cited — 對有理數 a、b、c、d 且 b≠0、d≠0，數值比 a:b 的值為 a/b；比例 a:b=c:d 表示 a/b=c/d，等價於 ad=bc。 · mko-ratio-proportion
- L_cross · lemma — 對有理數 a、b、c、d，b≠0、d≠0：a/b=c/d ⇔ ad=bc。
- L_solve · lemma — 對有理數 u 與 b≠0：bx=u ⇔ x=u/b。





## 逐步主鏈

S01 · definition操作前

a:b=x:d

操作後

\frac{a}{b}=\frac{x}{d}\quad (b\neq 0,\ d\neq 0)

條件：b\neq 0; d\neq 0

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

葉節點依據：mko_ratio_def + def_unfold

依 MKO，比 a:b 的值是 a/b，所以比例 a:b=x:d 就是有理數等式 a/b=x/d。兩個後項 b、d 必須非零，兩個商才有定義。



S02 · equivalent操作前

\frac{a}{b}=\frac{x}{d}

操作後

ad=bx

條件：b\neq 0; d\neq 0

規則：L_cross · 依賴：S01, L_cross

葉節點依據：L_cross

依引理 L_cross（c=x），比例等價於交叉乘積相等 ad=bx。這是 MKO 中「等價於 ad=bc」的內容，引理在 S02.1、S02.2 證明。



S03 · equivalent操作前

ad=bx

操作後

x=\frac{ad}{b}

條件：b\neq 0

規則：L_solve · 依賴：S02, L_solve

葉節點依據：L_solve + eq_refl_symm_trans

依等號對稱，ad=bx 即 bx=ad。依引理 L_solve（u=ad），因 b≠0，bx=ad ⇔ x=ad/b。



S04 · implies操作前

a:b=x:d

操作後

\{x\in\mathbb{Q}\mid a:b=x:d\}=\left\{\frac{ad}{b}\right\}

條件：b\neq 0; d\neq 0

規則：logic_chain · 依賴：S01, S02, S03

葉節點依據：logic_chain + set_extensionality + iff_intro

S01 到 S03 是一串等價：a:b=x:d ⇔ x=ad/b。所以解集恰為 {ad/b}。存在：ad/b 是有理數（有理數對乘法封閉，且 b≠0 時可除）。唯一：任何解都等於 ad/b。這就是 MKO 第三段所說的唯一有理解。



S05 · implies操作前

3:4=x:10

操作後

x=\frac{3\cdot 10}{4}=\frac{30}{4}=\frac{15}{2}

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

規則：forall_elim · 依賴：S04

葉節點依據：forall_elim + frac_rules + numeric_evaluation

代入 a=3、b=4、d=10；條件 4≠0、10≠0 成立。依 S04，唯一解是 x=3·10/4=30/4；約去公因數 2 得 15/2。



S06 · implies操作前

x=\frac{15}{2}

操作後

\frac{15/2}{10}=\frac{15}{20}=\frac{3}{4},\quad 3\cdot 10=30=4\cdot\frac{15}{2}

條件：無

規則：L_cross · 依賴：S05, L_cross

葉節點依據：L_cross + frac_rules + numeric_evaluation

代回核對：(15/2)/10=15/20=3/4，與 3:4 的值相同；交叉乘積 3·10=30、4·(15/2)=30 也相等。代回只確認 15/2 是解；「只有這個解」來自 S04 的等價鏈。



S07 · implies操作前

4:3=x:10

操作後

x=\frac{40}{3}\neq\frac{15}{2}

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

規則：L_cross · 依賴：S04, S05, L_cross

葉節點依據：L_cross + contrapositive + numeric_evaluation

把比的前後項對調：4:3 的後項是 3≠0，所以它是合法的比，依 S04 解得 x=4·10/3=40/3。40/3 與 15/2 的交叉乘積 40·2=80、3·15=45 不相等，所以兩個解不同。又 4/3 與 3/4 的交叉乘積 4·4=16≠9=3·3，所以 4:3≠3:4。比的順序是資料的一部分。



S08 · equivalent操作前

y_i=k\,x_i\quad (x_i\neq 0)

操作後

k=\frac{y_i}{x_i}

條件：x_i\neq 0

規則：L_solve · 依賴：G3, L_solve

葉節點依據：L_solve + mul_comm

四筆資料的 xᵢ 是 2、4、6、8，都非零。依 L_solve（b=xᵢ、u=yᵢ），yᵢ=k·xᵢ ⇔ k=yᵢ/xᵢ。所以資料符合正比例，當且僅當四個比值 yᵢ/xᵢ 是同一個數。



S09 · implies操作前

\frac{5}{2},\ \frac{10}{4},\ \frac{15}{6}

操作後

\frac{5}{2}=\frac{10}{4}=\frac{15}{6}

條件：無

規則：L_cross · 依賴：S08, L_cross

葉節點依據：L_cross + numeric_evaluation

前三筆的比值：10/4 與 5/2 的交叉乘積 10·2=20=4·5；15/6 與 5/2 的交叉乘積 15·2=30=6·5。依 L_cross，三個比值都等於 5/2，所以 k=5/2 適合前三筆。



S10 · implies操作前

\frac{21}{8}\ \text{vs}\ \frac{5}{2}

操作後

21\cdot 2=42\neq 40=8\cdot 5,\ \text{so no single}\ k

條件：無

規則：contradiction · 依賴：S08, S09, L_cross

葉節點依據：contradiction + L_cross + eq_refl_symm_trans + numeric_evaluation

第四筆的比值 21/8 與 5/2 的交叉乘積 42≠40，所以 21/8≠5/2。若有同一個 k 適合全部四筆，依 S08，k=5/2（第一筆）且 k=21/8（第四筆），推出 5/2=21/8，矛盾。所以整張表不符合任何正比例 y=kx，雖然前三筆符合。



S11 · implies操作前

0:0=x:5

操作後

\text{not a proportion, although}\ 0\cdot 5=0\cdot x\ \text{for every}\ x

條件：無

規則：mko_ratio_def · 依賴：S01, mko_ratio_def

葉節點依據：mko_ratio_def + mul_inverse_nonzero + mul_zero

非實例：0:0 的後項是 0，依 MKO 它不是數值比，0/0 沒有定義，所以 0:0=x:5 不是比例。若硬算交叉乘積，0·5=0·x 對每個 x 都成立，似乎「每個 x 都是解」；這只說明 L_cross 的前提 b≠0 不能省略，交叉乘積相等不能讓零後項變得合法。



S12 · implies操作前

S04,\ S05,\ S07,\ S10

操作後

x=\frac{ad}{b}\ \text{unique};\ 3:4=x:10\Leftrightarrow x=\frac{15}{2};\ 4:3=x:10\Leftrightarrow x=\frac{40}{3};\ \text{table not proportional}

條件：無

規則：and_intro_elim · 依賴：S04, S05, S07, S10

葉節點依據：and_intro_elim

四個目標分別由 S04（唯一解公式）、S05 與 S06（3:4=x:10 的解與核對）、S07（順序）與 S10（資料判定）完成。







## 局部子步與引理

S02.1 · implies操作前

\frac{a}{b}=\frac{c}{d}

操作後

ad=bc

條件：b\neq 0; d\neq 0

規則：eq_congruence · 依賴：eq_congruence, mul_inverse_nonzero

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

兩邊同乘 bd：左邊 a·(1/b)·b·d=a·1·d=ad，右邊 c·(1/d)·b·d=b·c·(d·(1/d))=bc（結合律、交換律、b·(1/b)=1、d·(1/d)=1）。



S02.2 · implies操作前

ad=bc

操作後

\frac{a}{b}=\frac{c}{d}

條件：bd\neq 0

規則：eq_congruence · 依賴：zero_product, eq_congruence, frac_rules

葉節點依據：eq_congruence + zero_product + frac_rules

因 b≠0、d≠0，依零乘積性質 bd≠0。兩邊同乘 1/(bd)：左邊 (ad)/(bd)=a/b（消去非零的 d），右邊 (bc)/(bd)=c/d（消去非零的 b）。S02.1 與 S02.2 合起來證得引理 L_cross。



S03.1 · equivalent操作前

bx=u

操作後

x=\frac{u}{b}

條件：b\neq 0

規則：mul_inverse_nonzero · 依賴：mul_inverse_nonzero, eq_congruence

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

⇒：兩邊同乘 1/b，(1/b)(bx)=((1/b)b)x=1·x=x，右邊 u·(1/b)=u/b。⇐：兩邊同乘 b，b·(u/b)=u·((1/b)b)=u。b=0 時 1/b 不存在，兩個方向都不能做。此子步證得引理 L_solve。







## 逐步反向審查


- S12 · sufficient_goal_reduction · S04, S05, S07, S10, and_intro_elim — 目標 G：(1) 到 (4)。足夠條件 H：S04、S05、S07、S10 各自成立；H⇒G 由合取引入。H 由定義、引理與精確計算正向證成，沒有把 G 當作前提。
- S11 · premise_audit · mko_ratio_def, mul_inverse_nonzero — 結論只是「這不是比例」；不對 x 宣稱任何解集。
- S10 · premise_audit · S08, S09, contradiction, L_cross — 矛盾來自「同一個 k」必須逐點成立；也可直接看 (5/2)·8=20≠21（N10）。
- S09 · premise_audit · S08, L_cross, numeric_evaluation — 逐點比較同一個 k；這只涉及前三筆，不推論表外或第四筆。
- S08 · inverse_equivalence · L_solve, G3 — 每一筆都是等價變形；需要 xᵢ≠0。
- S07 · premise_audit · S04, L_cross, contrapositive — 反向比 b:a 需要原前項 a≠0；這裡 a=3≠0。不等的結論用 L_cross 的逆否：交叉乘積不等推出值不等。
- S06 · premise_audit · S05, L_cross, numeric_evaluation — 這是獨立的數值核對（N2、N3），不取代 S04 的唯一性論證。
- S05 · premise_audit · S04, forall_elim, frac_rules — 套用 S04 前先確認兩個後項非零；30/4=15/2 是約分（N1）。
- S04 · premise_audit · S02, S03, logic_chain, set_extensionality — 因為每一步都是等價，所以同時得到存在與唯一；若其中有單向步驟，就只能得到其中一半。
- S03.1 · inverse_equivalence · mul_inverse_nonzero, eq_congruence, mul_assoc — 乘 1/b 與乘 b 互為反運算，前提 b≠0。
- S03 · inverse_equivalence · L_solve, eq_refl_symm_trans — 引理兩向都在 S03.1 證明；需要 b≠0。
- S02.2 · premise_audit · zero_product, frac_rules, eq_congruence — 這是 ⇐ 方向，需要 bd≠0；若容許 b=0 或 d=0，ad=bc 推不回任何比例（見錯誤控制一）。
- S02.1 · premise_audit · eq_congruence, mul_inverse_nonzero, mul_assoc, mul_comm — 化簡需要 1/b、1/d 存在。這是 ⇒ 方向。
- S02 · inverse_equivalence · L_cross — 引理兩個方向都有證明，且都需要 b≠0、d≠0。
- S01 · premise_audit · G1, G2, mko_ratio_def — 此步只展開定義；條件 b≠0、d≠0 之後每一步都要用到。





## 錯誤控制與反例

交叉乘積不能讓零後項合法MKO 提醒：交叉乘積相等不能讓零分母的表示變得合法。0:0=x:5 的「交叉乘積」0·5=0·x 對每個 x 都成立，3:0=6:0 的 3·0=0·6 也成立，但 0:0、3:0、6:0 都不是比。L_cross 的兩個方向（S02.1、S02.2）都用到 b≠0、d≠0；先確認後項非零，再比較交叉乘積。

相同比例不自動建立幾何相似MKO 指出相同比例也不自動建立幾何相似。例如邊長 1、2、夾角 60° 的平行四邊形，與邊長 2、4 的長方形，對應邊成比例（1:2=2:4），但一個有 60° 角、一個全是 90° 角，兩者不相似。數值比例只是關於數的陳述；相似或因果需要另外的條件與證明（假設 a2）。

順序有意義，有限資料要逐點檢查3:4 與 4:3 不同（交叉乘積 9≠16），把比例寫反會得到 40/3 而不是 15/2；反向比還需要原前項非零。判定正比例時，要對每一筆資料檢查同一個 k：前三筆都給 k=5/2，但第四筆 (8,21) 不符合，所以不能從一點或幾點推論全部輸入（MKO 第三段）。


- 因為 0·5=0·x，所以 0:0=x:5 對每個 x 成立 → reject — 0:0 的後項為 0，不是比；L_cross 需要後項非零。
- 3:4=4:3 → reject — 交叉乘積 3·3=9≠16=4·4。
- 前三筆資料都滿足 y=(5/2)x，所以整張表是正比例 → reject — 第四筆 (5/2)·8=20≠21。
- 邊長 1、2 的 60° 平行四邊形與 2×4 長方形對應邊成比例，所以兩者相似 → reject — 角不相等（60° 與 90°）；數值比例不推出幾何相似。





## 結論與限制

對 b≠0、d≠0，a:b=x:d 恰有一解 x=ad/b。3:4=x:10 的解是 15/2（代回 3·10=30=4·15/2）；4:3=x:10 的解是 40/3，比的順序有意義。資料前三筆符合 y=(5/2)x，但第四筆 21/8≠5/2，所以整張表不是正比例。0:0 不是比，交叉乘積不能讓它合法。


- 錯誤控制二的平行四邊形例子用到「相似圖形的對應角相等」這一幾何事實，本稿未證明它，只用來說明數值比例不足以推出相似。





## 驗證及來源綁定

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


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

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