# 相似：以指定正倍率判定標記三角形相似並求面積

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

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

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



## 目標與範圍

在同一等單位正交平面中，A1=(0,0)、A2=(4,0)、A3=(0,2)，B1=(1,1)、B2=(1,7)、B3=(4,1)，對應 Ai↔Bi，倍率方向為 |BiBj|=k|AiAj|，指定 k=3/2。判定兩者在 k=3/2 下相似，並由已知面積 Area(A)=4 求 Area(B)；再說明 k=2 只被否定為見證、k=−3/2 不合資格，以及方向相反不改變正倍率。

只在 MKO 的 SSS 相似切片內工作：明示對應、明示倍率方向、k=p/q 且 q>0、整數座標、以交叉相乘精確比較。面積只用 MKO 給出的「面積為 k² 倍」條款，從已給的正面積計算；不發展一般面積理論，不搜尋其他對應。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- eq_congruence
- power_laws
- frac_rules
- zero_product
- order_basics
- numeric_evaluation


- G1 — 模型：同一等單位正交歐氏平面 ℝ²，整數座標。
- G2 — A1=(0,0)、A2=(4,0)、A3=(0,2)；B1=(1,1)、B2=(1,7)、B3=(4,1)；對應 Ai↔Bi；倍率方向 |BiBj|=k|AiAj|。
- G3 — 指定倍率 k=3/2（p=3、q=2）；已知 Area(A)=4；比較用候選倍率 k=2 與 k=−3/2。


- k=\tfrac{p}{q} — 指定的長度倍率，q>0
- |A_iA_j| — A 的第 ij 組邊長
- S_k(A,B) — 在對應 Ai↔Bi 下以倍率 k 相似
- \mathrm{Area}(A) — A 的已知正面積
- \det(u,v) — 以 u、v 為兩行（row）的二階行列式





## 規則與來源


- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- 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_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。
- mko_sim_slice · cited — 對明示 Ai↔Bi 的兩個非退化歐氏平面三角形，正倍率 k 的 SSS 相似切片要求每組對應邊長 BiBj=k·AiAj；等價地三組平方長度都乘 k²；若給定 A 的正面積值，B 的面積為 k² 倍；鏡射不改變正長度倍率。 · mko-similarity
- dist_formula · cited — 在同一等單位正交座標系，P=(x1,y1)、Q=(x2,y2) 的距離為 d(P,Q)=√((x2−x1)²+(y2−y1)²)≥0；距離平方是兩個座標差平方之和。 · mko-distance-formula
- det2_def · cited — 實二階方陣 M=[[a,b],[c,d]] 的行列式為 det(M)=ad−bc；本稿把向量 (a,b)、(c,d) 作為兩行（row）。 · mko-determinant
- det_collinear · prerequisite — 平面上三點 P、Q、R 共線當且僅當 det(Q−P, R−P)=0；所以 det≠0 推出三點相異且不共線。
- L_scale_sq · lemma — 對實數 k>0、u≥0、v≥0：v=ku ⇔ v²=k²u²。





## 逐步主鏈

S01 · definition操作前

S(A,B)\ \text{at a specified scale}\ k

操作後

S_k(A,B)\iff k>0\ \land\ A,B\ \text{nondegenerate}\ \land\ |B_iB_j|=k|A_iA_j|\ (ij=12,13,23)

條件：A_i\leftrightarrow B_i\ \text{explicit}; \text{scale direction explicit}

規則：mko_sim_slice · 依賴：G1, G2

葉節點依據：mko_sim_slice

依 MKO 固定判準：在明示對應與倍率方向下，A、B 以倍率 k 相似，當且僅當 k 為正、兩者非退化，且三組對應邊都滿足 |BiBj|=k|AiAj|。方向很重要：這裡是 B 的邊等於 k 乘 A 的邊，不是反過來（反過來的倍率是 1/k）。



S02 · implies操作前

k=\tfrac{p}{q}=\tfrac{3}{2}

操作後

p=3>0,\ q=2>0\ \Rightarrow\ k>0

條件：q>0

規則：order_basics · 依賴：G3, order_basics

葉節點依據：order_basics + mul_inverse_nonzero

MKO 假設 a2：k=p/q 且 q>0，倍率合格當且僅當 p>0。這裡 p=3>0、q=2>0。由 2>0 得 1/2>0（因 2·(1/2)=1>0，若 1/2≤0 則乘以正數 2 得 1≤0，矛盾），再以正數 3 乘之得 3/2>0。所以 k=3/2 是合格的正倍率。



S03 · implies操作前

\det(A_2-A_1,\,A_3-A_1)

操作後

\det((4,0),(0,2))=4\cdot 2-0\cdot 0=8\neq 0:\ A\ \text{nondegenerate}

條件：8\neq 0

規則：det_collinear · 依賴：G2, det2_def, det_collinear

葉節點依據：det2_def + det_collinear + numeric_evaluation

A2−A1=(4,0)、A3−A1=(0,2)，行列式 4·2−0·0=8≠0，所以 A1、A2、A3 相異且不共線，A 是非退化三角形（MKO 假設 a1）。



S04 · implies操作前

\det(B_2-B_1,\,B_3-B_1)

操作後

\det((0,6),(3,0))=0\cdot 0-6\cdot 3=-18\neq 0:\ B\ \text{nondegenerate}

條件：-18\neq 0

規則：det_collinear · 依賴：G2, det2_def, det_collinear

葉節點依據：det2_def + det_collinear + numeric_evaluation

B2−B1=(0,6)、B3−B1=(3,0)，行列式 0·0−6·3=−18≠0，所以 B 也是非退化三角形。負號在 S12 解讀為方向。



S05 · equivalent操作前

|B_iB_j|=k|A_iA_j|

操作後

|B_iB_j|^2=k^2|A_iA_j|^2

條件：k>0; |A_iA_j|\ge 0; |B_iB_j|\ge 0

規則：L_scale_sq · 依賴：S02, dist_formula

葉節點依據：eq_congruence + power_laws + zero_product + order_basics

依引理 L_scale_sq（u=|AiAj|、v=|BiBj|），在 k>0 且長度非負時，長度關係與平方長度關係等價。這正是 MKO 所說「長度乘 k 等價於平方長度乘 k²」；引理在 S05.1 至 S05.3 證明。



S06 · equivalent操作前

|B_iB_j|^2=\left(\tfrac{p}{q}\right)^2|A_iA_j|^2

操作後

|B_iB_j|^2\,q^2=|A_iA_j|^2\,p^2

條件：q\neq 0

規則：frac_rules · 依賴：S05, frac_rules

葉節點依據：frac_rules + power_laws + mul_inverse_nonzero + eq_congruence

(p/q)²=p²/q²，兩邊同乘 q²（q≠0，所以 q²≠0）得整數交叉乘積式。這是 MKO 所說的精確檢查 B²q²=A²p²：只用整數乘法，不用小數。



S07 · equivalent操作前

|A_1A_2|^2,\ |A_1A_3|^2,\ |A_2A_3|^2

操作後

16,\ 4,\ 20

條件：無

規則：dist_formula · 依賴：G2, dist_formula

葉節點依據：dist_formula + numeric_evaluation

按 12、13、23 順序：(4−0)²+(0−0)²=16；(0−0)²+(2−0)²=4；(0−4)²+(2−0)²=16+4=20。



S08 · equivalent操作前

|B_1B_2|^2,\ |B_1B_3|^2,\ |B_2B_3|^2

操作後

36,\ 9,\ 45

條件：無

規則：dist_formula · 依賴：G2, dist_formula

葉節點依據：dist_formula + numeric_evaluation

同一順序：(1−1)²+(7−1)²=36；(4−1)²+(1−1)²=9；(4−1)²+(1−7)²=9+36=45。



S09 · implies操作前

|B_1B_2|^2q^2\ \text{vs}\ |A_1A_2|^2p^2

操作後

36\cdot 2^2=144=16\cdot 3^2

條件：無

規則：numeric_evaluation · 依賴：S06, S07, S08, G3

葉節點依據：numeric_evaluation + eq_refl_symm_trans

第 12 組：左邊 36·4=144，右邊 16·9=144，相等，所以由 S06 得 |B1B2|²=(3/2)²|A1A2|²。



S10 · implies操作前

\text{pairs }13,\ 23

操作後

9\cdot 2^2=36=4\cdot 3^2,\quad 45\cdot 2^2=180=20\cdot 3^2

條件：無

規則：numeric_evaluation · 依賴：S06, S07, S08, G3

葉節點依據：numeric_evaluation + eq_refl_symm_trans

第 13 組：9·4=36=4·9；第 23 組：45·4=180=20·9。三組都通過交叉乘積檢查，沒有首個不等見證。



S11 · implies操作前

|B_iB_j|^2=\tfrac{9}{4}|A_iA_j|^2\ (ij=12,13,23)

操作後

S_{3/2}(A,B):\ 6=\tfrac32\cdot 4,\ 3=\tfrac32\cdot 2,\ 3\sqrt5=\tfrac32\cdot 2\sqrt5

條件：k=\tfrac32>0; A,B\ \text{nondegenerate}

規則：mko_sim_slice · 依賴：S01, S02, S03, S04, S05, S09, S10

葉節點依據：mko_sim_slice + L_scale_sq + and_intro_elim

由 S09、S10 與 S06，三組平方長度都乘 9/4；由 S05（引理 ⇐ 方向，k=3/2>0），三組長度都乘 3/2：6=(3/2)·4、3=(3/2)·2、√45=3√5=(3/2)·√20=(3/2)·2√5。加上 S02 至 S04 的資格，S01 的判準全部成立，所以 A、B 在 k=3/2 下相似。



S12 · implies操作前

\det_A=8>0,\ \det_B=-18<0

操作後

\text{opposite orientations; scale still}\ k=\tfrac32>0

條件：無

規則：mko_sim_slice · 依賴：S03, S04, S11

葉節點依據：mko_sim_slice + order_basics + numeric_evaluation

兩個行列式異號，B 的方向與 A 相反：B 可由 A 先關於 y=x 鏡射、再均勻放大 3/2、再平移 (1,1) 得到，即 Bi=(1+(3/2)y, 1+(3/2)x)，其中 Ai=(x,y)（N18、N19 核對 B2、B3）。MKO 指出鏡射不改變正長度倍率；倍率是長度之比，長度非負，所以倍率仍是 3/2，不是 −3/2。



S13 · theorem_application操作前

S_{3/2}(A,B),\ \mathrm{Area}(A)=4

操作後

\mathrm{Area}(B)=\left(\tfrac32\right)^2\cdot 4=9

條件：S_{3/2}(A,B); \mathrm{Area}(A)=4>0

規則：mko_sim_slice · 依賴：S11, G3

葉節點依據：mko_sim_slice + power_laws + numeric_evaluation

依 MKO 的面積條款：已確立以正倍率 k 相似，且給定 A 的正面積，則 B 的面積是 k² 倍。k²=9/4，所以 Area(B)=(9/4)·4=9。不是 k·4=6：面積是二維量，乘的是 k²。



S14 · implies操作前

k=2=\tfrac{2}{1}

操作後

36\cdot 1^2=36\neq 64=16\cdot 2^2:\ k=2\ \text{rejected as a witness}

條件：無

規則：numeric_evaluation · 依賴：S06, S07, S08

葉節點依據：numeric_evaluation + contrapositive

以 p=2、q=1 做第 12 組交叉乘積：36·1=36，16·4=64，不等，所以第 12 組就是首個不等見證，k=2 不是相似倍率見證。MKO 假設 a3：這只否定 k=2 這個見證，不代表 A、B 不相似（S11 已證 k=3/2 可行）。事實上在此對應下倍率被第 12 組決定：若 |B1B2|=k'|A1A2|，則 6=4k'，k'=3/2。



S15 · implies操作前

k=-\tfrac32=\tfrac{-3}{2}

操作後

p=-3\le 0:\ k\ \text{ineligible}

條件：無

規則：mko_sim_slice · 依賴：G3, S01, S05

葉節點依據：mko_sim_slice + order_basics + numeric_evaluation

MKO 假設 a2：資格題允許 p≤0，並答否。這裡 p=−3≤0，所以 k=−3/2 不合格。注意 (−3/2)²=9/4，平方交叉乘積會全部通過，所以符號必須另外檢查；直接看長度也一樣：|B1B2|=6，而 (−3/2)·4=−6，長度不可能是負數。







## 局部子步與引理

S05.1 · implies操作前

k>0,\ u\ge 0

操作後

ku\ge 0

條件：k>0

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics + mul_zero + case_analysis

若 u=0，ku=0≥0；若 u>0，兩邊乘正數 k 保持不等號：ku>k·0=0。所以 ku≥0。



S05.2 · implies操作前

v=ku

操作後

v^2=(ku)^2=k^2u^2

條件：無

規則：eq_congruence · 依賴：eq_congruence, power_laws

葉節點依據：eq_congruence + power_laws

兩邊平方（同一運算作用於相等的數），再用 (ab)²=a²b²。這是引理的 ⇒ 方向。



S05.3 · case_split操作前

v^2=k^2u^2,\ v\ge 0,\ ku\ge 0

操作後

v=ku

條件：v\ge 0; ku\ge 0

規則：zero_product · 依賴：S05.1, zero_product, distributive

葉節點依據：zero_product + distributive + case_analysis + order_basics

v²−(ku)²=(v−ku)(v+ku)=0（N17 核對此恆等式），依零積性質 v−ku=0 或 v+ku=0。前者即 v=ku。後者時 v=−ku≤0（因 S05.1 的 ku≥0），又 v≥0，故 v=0，進而 ku=0，仍得 v=ku。S05.1 至 S05.3 合起來證得引理 L_scale_sq。







## 逐步反向審查


- S15 · premise_audit · G3, S01, S05, mko_sim_slice — S05 的 ⇐ 方向需要 k>0，所以平方檢查不能代替符號檢查；本步不宣稱負倍率的任何幾何意義。
- S14 · premise_audit · S06, S07, S08, numeric_evaluation — 用到 S06 的等價（不等的平方式推出不等的長度關係）；不宣稱任何其他對應下的結論。
- S13 · premise_audit · S11, G3, mko_sim_slice — 需要 S11 的相似結論與已給的正面積；本步不從座標推導面積理論。
- S12 · premise_audit · S03, S04, S11, mko_sim_slice — 方向只由行列式正負讀出，相似判定（S11）沒有用到方向；映射公式只是交叉核對。
- S11 · sufficient_goal_reduction · S01, S02, S03, S04, S05, S09, S10 — 目標 G：S_{3/2}(A,B)。足夠條件 H：k>0、兩者非退化、三組邊長都乘 k；H⇒G 由判準 S01。H 由 S02 至 S10 正向證成，沒有把 G 當作前提。
- S10 · premise_audit · S06, S07, S08, numeric_evaluation — 精確整數相等（N10、N11）。
- S09 · premise_audit · S06, S07, S08, numeric_evaluation — 精確整數相等（N9）；只處理第 12 組。
- S08 · inverse_equivalence · dist_formula, numeric_evaluation — 重算見 N6、N7、N8。
- S07 · inverse_equivalence · dist_formula, numeric_evaluation — 重算見 N3、N4、N5；兩邊是同一個數。
- S06 · inverse_equivalence · frac_rules, mul_inverse_nonzero — 反向是兩邊同除以 q²，需要 q≠0，由 MKO 的 q>0 保證。
- S05.3 · premise_audit · S05.1, zero_product, order_basics — 第二情況使用 ku≥0，本稿由 k>0、u≥0 得到它。若 k=−3/2 且 u>0，ku<0，這條推理不能直接使用；若 u=0 則 ku=0。具體非退化三角形的邊長為正，仍依 S02 排除負倍率。
- S05.2 · premise_audit · eq_congruence, power_laws — 只宣稱 ⇒；反向在 S05.3 使用非負條件處理。
- S05.1 · premise_audit · order_basics, mul_zero — 本稿採 k>0 作充分前提，且它是相似倍率的資格條件。單就 ku≥0 而言，u≥0 時 k=0 也可用；若 k<0 且 u>0 則 ku<0。這不把零倍率納入本稿的相似資格。
- S05 · inverse_equivalence · L_scale_sq, S02 — 兩個方向都在子步證明。本稿以 k>0 與非負長度保證 ku≥0，讓平方關係推回長度關係；這是所採用的充分前提。k=0 的算術邊界也可成立，但不符合 S02 的倍率資格；負 k 配正長度時則有符號問題。
- S04 · premise_audit · G2, det2_def, det_collinear — 重算見 N2；負號不影響非退化。
- S03 · premise_audit · G2, det2_def, det_collinear — 重算見 N1；只用 det≠0 ⇒ 不共線。
- S02 · premise_audit · G3, order_basics — 只用正數乘正數仍為正；本步不宣稱 3/2 是唯一可能的倍率（見 S14）。
- S01 · premise_audit · G1, G2, mko_sim_slice — 此步只寫出判準，不推出新事實；k 是被檢查的見證，不是由圖形猜出。





## 錯誤控制與反例

長度乘 k，面積乘 k²MKO 的誤解之一是長度和面積都只乘 k，或把平方倍率當長度倍率。本例長度乘 3/2（6=(3/2)·4），平方長度乘 9/4（36=(9/4)·16），面積乘 9/4（4 變成 9）。若面積只乘 k 會得到 6；若把平方長度乘 k 會得到 24 而不是 36。

錯誤的 k 只否定該見證k=2 在第 12 組失敗（36≠64），但這只說明 k=2 不是見證；以 k=3/2 檢查則三組都通過。MKO 假設 a3 明言：指定倍率不符合只否定那個倍率見證，不代表不存在其他相似倍率。

負座標係數與負長度倍率不同方向相反（行列式異號）或座標乘負數，都不會讓長度倍率變負。MKO 指出對座標做係數 −2 的均勻縮放，長度倍率是正的 2。本例的 B 含鏡射，但倍率仍是 3/2；k=−3/2 因 p≤0 不合格，雖然它的平方與 3/2 的平方相同。


- Area(B)=k·Area(A)=(3/2)·4=6 → reject — 面積乘 k²：(9/4)·4=9。
- 平方長度也只乘 k，所以 |B1B2|²=(3/2)·16=24 → reject — |B1B2|²=36=(9/4)·16；平方長度乘 k²。
- k=2 在第 12 組失敗，所以 A 與 B 不相似 → reject — 只否定 k=2 這個見證；k=3/2 三組都通過（S11）。
- k=−3/2 的平方交叉乘積全部通過，所以 −3/2 也是合格倍率 → reject — p=−3≤0 不合格；平方檢查無法分辨 k 與 −k，而 (−3/2)·4=−6 不可能等於長度 6。





## 結論與限制

A、B 都非退化（行列式 8 與 −18）。在對應 Ai↔Bi 下三組平方邊長 16、4、20 與 36、9、45 都滿足 B²·2²=A²·3²，所以 A、B 以 k=3/2 相似，平方長度乘 9/4；由 Area(A)=4 得 Area(B)=9。B 的方向與 A 相反，但倍率仍是正的 3/2。k=2 在第 12 組失敗，只否定該見證；k=−3/2 因 p≤0 不合格。


- 面積結論只用 MKO 的 k² 面積條款，從已給的 Area(A)=4 計算。N20 以 |det|/2 做獨立數值交叉核對（18/2=9），該面積公式未在本稿證明，論證不依賴它。
- det_collinear 是本稿的前提，未在本稿中證明；本稿只檢查題目給定的對應。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: a3e5da3d8b98c14fda10b000ea7223cdb705cfc1824ae646dd1becfcce543568
- original source SHA-256: 58669e6075a82ec69759d174d0aa3477b52d7ff3ba2964ddac1c24f126d02aed
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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