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

目標與範圍

在有理數中：(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。

逐步主鏈

a:b=x:d

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

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

ad=bx

ad=bx

x=\frac{ad}{b}

a:b=x:d

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

3:4=x:10

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

x=\frac{15}{2}

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

4:3=x:10

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

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

k=\frac{y_i}{x_i}

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

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

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

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

0:0=x:5

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

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}

局部子步與引理

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

ad=bc

ad=bc

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

bx=u

x=\frac{u}{b}

逐步反向審查

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