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

目標與範圍

在同一等單位正交平面中，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²。

逐步主鏈

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)

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

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

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

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

|B_iB_j|=k|A_iA_j|

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

|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

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

16,\ 4,\ 20

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

36,\ 9,\ 45

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

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

\text{pairs }13,\ 23

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

|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

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

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

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

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

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

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

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

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

局部子步與引理

k>0,\ u\ge 0

ku\ge 0

v=ku

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

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

v=ku

逐步反向審查

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