# 全等：以 SSS 切片判定有明示對應的三角形全等 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-congruence/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-congruence-01 · production-20261019-adopted-96 ## 目標與範圍在同一個等單位正交平面中，A1=(0,0)、A2=(4,0)、A3=(0,3)，B1=(1,1)、B2=(1,5)、B3=(4,1)，對應明示為 Ai↔Bi。先以行列式驗證兩組點都是非退化三角形，再依 12、13、23 的順序精確比較平方邊長，判定 G(A,B)；說明 B 的方向與 A 相反卻仍全等；最後找出另一個對應 A1↔B1、A2↔B3、A3↔B2 的首個不等見證，並說明退化點組不合格。只在 MKO 的 SSS 切片內工作：同一等單位正交座標平面、整數座標、明示對應、以平方長度精確比較。不證明 SSS 判定本身，也不處理 SAS、ASA 等其他判定或無標籤的對應搜尋；鏡射映射只作交叉核對。不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - eq_congruence - distributive - zero_product - order_basics - sqrt_def - numeric_evaluation - G1 — 模型：同一個等單位正交歐氏平面 ℝ²，點以整數座標給出。 - G2 — A1=(0,0)、A2=(4,0)、A3=(0,3)；B1=(1,1)、B2=(1,5)、B3=(4,1)；明示對應 A1↔B1、A2↔B2、A3↔B3。 - G3 — 比較用資料：另一個對應 A1↔B1、A2↔B3、A3↔B2；退化候選點組 D=((0,0),(1,1),(2,2)) 與 D'=((5,5),(6,6),(7,7))。 - A_i,\ B_i — 兩個三角形的頂點，i=1,2,3 - A_i\leftrightarrow B_i — 明示的頂點對應 - |PQ| — P、Q 間的歐氏距離 - \det(u,v) — 以 u=(a,b)、v=(c,d) 為兩行（row）的二階行列式 ad−bc - G(A,B) — 在對應 Ai↔Bi 下 A 與 B 全等 ## 規則與來源 - eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。 - distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。 - zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。 - order_basics · prerequisite — 實數的序：任兩數恰有 uv 之一；u0 推出 uwvw。 - sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。 - 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。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - contrapositive · prerequisite — 逆否命題：P⇒Q 與 ¬Q⇒¬P 等價。逆命題 Q⇒P 一般不與 P⇒Q 等價。 - mko_sss_slice · cited — 在同一等單位正交歐氏平面，A、B 都為非退化三角形且對應明示為 Ai↔Bi 時，本輪以三組對應邊長全部相等的 SSS 切片判全等；可用平方長度精確比較，鏡射改變方向但不破壞全等。 · mko-congruence - 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），寫成 det((a,b),(c,d))。 · mko-determinant - det_collinear · prerequisite — 平面上三點 P、Q、R 共線（有一條直線含三者）當且僅當 det(Q−P, R−P)=0。有重點的三點必共線，所以 det≠0 推出三點相異且不共線。 - L_sq_eq · lemma — 對實數 u≥0、v≥0：u=v ⇔ u²=v²。 - L_T_iso · lemma — 映射 T(x,y)=(y+1, x+1)（關於 y=x 鏡射後平移 (1,1)）保持平方距離：對所有點 P、Q，|T(P)T(Q)|²=|PQ|²。 ## 逐步主鏈 S01 · definition操作前 G(A,B)\ \text{for labeled triangles} 操作後 G(A,B)\iff A,B\ \text{nondegenerate}\ \land\ |A_iA_j|=|B_iB_j|\ (ij=12,13,23) 條件：A_i\leftrightarrow B_i\ \text{explicit} 規則：mko_sss_slice · 依賴：G1, G2 葉節點依據：mko_sss_slice 依 MKO 的 SSS 切片固定判準：在明示對應 Ai↔Bi 下，A 與 B 全等，當且僅當兩者都是非退化三角形，且 12、13、23 三組對應邊長都相等。判準有兩道關卡：先驗非退化，再比邊長；比較的是指定的對應邊，不是任意重新配對。 S02 · equivalent操作前 \det(A_2-A_1,\,A_3-A_1) 操作後 \det((4,0),(0,3))=4\cdot 3-0\cdot 0=12 條件：無規則：det2_def · 依賴：G2, det2_def 葉節點依據：det2_def + numeric_evaluation 逐坐標相減：A2−A1=(4−0, 0−0)=(4,0)，A3−A1=(0−0, 3−0)=(0,3)。依行列式公式 ad−bc：4·3−0·0=12。兩邊是同一個數，這是等值代換。 S03 · implies操作前 \det(A_2-A_1,\,A_3-A_1)=12\neq 0 操作後 A_1,A_2,A_3\ \text{distinct, noncollinear: }A\ \text{nondegenerate} 條件：12\neq 0 規則：det_collinear · 依賴：S02, det_collinear 葉節點依據：det_collinear + numeric_evaluation 依 det_collinear，三點共線當且僅當行列式為 0；這裡行列式為 12≠0，所以 A1、A2、A3 不共線，也就兩兩相異（有重點的三點必共線）。依 MKO 假設 a1，這是把 A 當作三角形使用之前必須先驗的條件。 S04 · implies操作前 \det(B_2-B_1,\,B_3-B_1) 操作後 \det((0,4),(3,0))=0\cdot 0-4\cdot 3=-12\neq 0:\ B\ \text{nondegenerate} 條件：-12\neq 0 規則：det_collinear · 依賴：G2, det2_def, det_collinear 葉節點依據：det2_def + det_collinear + numeric_evaluation B2−B1=(1−1, 5−1)=(0,4)，B3−B1=(4−1, 1−1)=(3,0)，行列式 0·0−4·3=−12。它不是 0，所以 B1、B2、B3 相異且不共線，B 也是非退化三角形。行列式為負這件事留到 S11 解讀為方向；非退化只看它是否為 0。 S05 · equivalent操作前 |A_iA_j|=|B_iB_j| 操作後 |A_iA_j|^2=|B_iB_j|^2 條件：|A_iA_j|\ge 0; |B_iB_j|\ge 0 規則：L_sq_eq · 依賴：dist_formula 葉節點依據：eq_congruence + distributive + zero_product + order_basics 距離都是非負實數（dist_formula），所以依引理 L_sq_eq（u=|AiAj|、v=|BiBj|），比較邊長等價於比較平方邊長。平方邊長是整數座標差的平方和，可精確計算，不需開根號或取近似值。引理在 S05.1 至 S05.3 證明。 S06 · equivalent操作前 |A_1A_2|^2,\ |A_1A_3|^2,\ |A_2A_3|^2 操作後 16,\ 9,\ 25 條件：無規則：dist_formula · 依賴：G2, dist_formula 葉節點依據：dist_formula + numeric_evaluation 依距離平方公式，按 12、13、23 順序：|A1A2|²=(4−0)²+(0−0)²=16；|A1A3|²=(0−0)²+(3−0)²=9；|A2A3|²=(0−4)²+(3−0)²=16+9=25。每一項都是精確整數。 S07 · equivalent操作前 |B_1B_2|^2,\ |B_1B_3|^2,\ |B_2B_3|^2 操作後 16,\ 9,\ 25 條件：無規則：dist_formula · 依賴：G2, dist_formula 葉節點依據：dist_formula + numeric_evaluation 同一公式、同一順序：|B1B2|²=(1−1)²+(5−1)²=16；|B1B3|²=(4−1)²+(1−1)²=9；|B2B3|²=(4−1)²+(1−5)²=9+16=25。B 的邊指向不同方向（B1B2 鉛直，A1A2 水平），但平方長度只看座標差的平方和。 S08 · implies操作前 (16,9,25)\ \text{vs}\ (16,9,25) 操作後 |A_iA_j|^2=|B_iB_j|^2\ (ij=12,13,23) 條件：無規則：eq_refl_symm_trans · 依賴：S06, S07 葉節點依據：eq_refl_symm_trans + numeric_evaluation 依 12、13、23 的順序逐一比較：16=16、9=9、25=25。三組都相等，所以沒有首個不等見證，答案是「無不等邊」。比較的是指定對應下的邊：A1A2 只和 B1B2 比，不和 B 的其他邊比。 S09 · implies操作前 |A_iA_j|^2=|B_iB_j|^2\ (ij=12,13,23) 操作後 |A_1A_2|=|B_1B_2|=4,\ |A_1A_3|=|B_1B_3|=3,\ |A_2A_3|=|B_2B_3|=5 條件：\text{lengths}\ge 0 規則：L_sq_eq · 依賴：S05, S08 葉節點依據：L_sq_eq + sqrt_def 由 S05（引理 L_sq_eq 的 ⇐ 方向），平方相等的非負長度本身相等。具體數值：16、9、25 的非負平方根是 4、3、5（sqrt_def），所以三組對應邊長分別是 4、3、5。 S10 · theorem_application操作前 A,B\ \text{nondegenerate},\ |A_iA_j|=|B_iB_j|\ (ij=12,13,23) 操作後 G(A,B)\ \text{under}\ A_i\leftrightarrow B_i 條件：A,B\ \text{nondegenerate}; A_i\leftrightarrow B_i\ \text{explicit} 規則：mko_sss_slice · 依賴：S01, S03, S04, S09 葉節點依據：mko_sss_slice + and_intro_elim S01 判準的兩道關卡都已通過：非退化（S03、S04）與三組對應邊相等（S09）。所以在明示對應 Ai↔Bi 下 A 與 B 全等。判定沒有用到圖形外觀，也沒有猜測其他標籤排列。 S11 · implies操作前 \det(A_2-A_1,A_3-A_1)=12>0,\ \det(B_2-B_1,B_3-B_1)=-12<0 操作後 \text{opposite orientations; }G(A,B)\ \text{still holds} 條件：無規則：mko_sss_slice · 依賴：S02, S04, S10 葉節點依據：mko_sss_slice + order_basics 兩個行列式異號：A1→A2→A3 是逆時針，B1→B2→B3 是順時針，B 的方向與 A 相反。MKO 指出鏡射改變方向但不破壞全等；S10 的判定只用到非退化與邊長，兩者都與方向無關，所以 G(A,B) 不受影響。 S12 · implies操作前 T(x,y)=(y+1,\,x+1) 操作後 T(A_1)=B_1,\ T(A_2)=B_2,\ T(A_3)=B_3 條件：無規則：L_T_iso · 依賴：G2, S10 葉節點依據：L_T_iso + eq_replace + numeric_evaluation 交叉核對：T 是先關於直線 y=x 鏡射、再平移 (1,1)。T(A1)=(0+1, 0+1)=(1,1)=B1；T(A2)=(0+1, 4+1)=(1,5)=B2；T(A3)=(3+1, 0+1)=(4,1)=B3。依引理 L_T_iso（S12.1），T 保持所有平方距離，所以 B 是 A 的鏡像搬移，與 S10、S11 一致。本步不是 S10 的前提。 S13 · implies操作前 A_1\leftrightarrow B_1,\ A_2\leftrightarrow B_3,\ A_3\leftrightarrow B_2 操作後 |A_1A_2|^2=16\neq 9=|B_1B_3|^2:\ \text{first unequal witness}\ 12 條件：無規則：L_sq_eq · 依賴：G3, S05, S06, S07 葉節點依據：L_sq_eq + contrapositive + numeric_evaluation 在另一個對應下，第 12 組對應邊是 A1A2 與 B1B3。由 S06、S07，平方長度是 16 與 9，不等；依 S05（長度相等必平方相等）的逆否，長度也不等。依 12、13、23 順序，首個不等見證是 12，不必再看 13、23。這只否定這個對應；在 Ai↔Bi 下的全等（S10）仍然成立。 S14 · implies操作前 D=((0,0),(1,1),(2,2)) 操作後 \det((1,1),(2,2))=1\cdot 2-1\cdot 2=0:\ D\ \text{collinear, not eligible} 條件：無規則：det_collinear · 依賴：G3, det2_def, det_collinear 葉節點依據：det2_def + det_collinear + numeric_evaluation D 的兩個差向量是 (1,1) 與 (2,2)，行列式 0，所以 D 三點共線，不是非退化三角形；D' 是 D 平移 (5,5)，差向量相同，也共線。D 與 D' 的對應平方邊長都是 2、8、2（N13），三組都相等，但 SSS 切片的第一道關卡（非退化）不通過，所以不能說它們是全等三角形。這說明 S03、S04 必須在比較邊長之前完成。 ## 局部子步與引理 S05.1 · implies操作前 u=v 操作後 u^2=v^2 條件：無規則：eq_congruence · 依賴：eq_congruence 葉節點依據：eq_congruence 對相等的兩數作同一個運算（平方），結果相等。這是引理的「⇒」方向，對任何實數都成立。 S05.2 · equivalent操作前 u^2=v^2 操作後 (u-v)(u+v)=0 條件：無規則：distributive · 依賴：distributive 葉節點依據：distributive + mul_comm + add_inverse + eq_congruence 兩邊同減 v² 得 u²−v²=0；再以分配律展開 (u−v)(u+v)=u²+uv−vu−v²=u²−v²（乘法交換使 uv−vu=0）。N9 以多項式恆等式核對這個展開。 S05.3 · case_split操作前 (u-v)(u+v)=0,\ u\ge 0,\ v\ge 0 操作後 u=v 條件：u\ge 0; v\ge 0 規則：zero_product · 依賴：S05.2, zero_product, order_basics 葉節點依據：zero_product + case_analysis + order_basics 依零積性質，u−v=0 或 u+v=0。情況一：u−v=0，即 u=v。情況二：u+v=0，則 u=−v≤0，又 u≥0，所以 u=0，進而 v=0，仍得 u=v。兩種情況涵蓋全部可能，所以 u²=v² 推出 u=v。S05.1 至 S05.3 合起來證得引理 L_sq_eq。 S12.1 · equivalent操作前 |T(P)T(Q)|^2,\ P=(x_1,y_1),\ Q=(x_2,y_2) 操作後 ((y_2+1)-(y_1+1))^2+((x_2+1)-(x_1+1))^2=(x_2-x_1)^2+(y_2-y_1)^2=|PQ|^2 條件：無規則：dist_formula · 依賴：dist_formula, add_comm 葉節點依據：dist_formula + add_comm + add_inverse + forall_intro T(P)=(y1+1, x1+1)、T(Q)=(y2+1, x2+1)。依距離平方公式，|T(P)T(Q)|²=((y2+1)−(y1+1))²+((x2+1)−(x1+1))²=(y2−y1)²+(x2−x1)²；依加法交換，這等於 (x2−x1)²+(y2−y1)²=|PQ|²。P、Q 是任意點，所以證得引理 L_T_iso（N10 以多項式恆等式核對）。 ## 逐步反向審查 - S14 · premise_audit · G3, det2_def, det_collinear — 用的是「det=0 ⇒ 共線」；邊長相等的事實在這裡不足以補救資格。 - S13 · premise_audit · S05, S06, S07, contrapositive — 用的是「長度相等 ⇒ 平方相等」的逆否；本步不宣稱 A、B 在任何對應下都不全等。 - S12.1 · inverse_equivalence · dist_formula, add_comm — 每個等號都是對所有實數成立的恆等式，所以整條鏈雙向成立；沒有對 P、Q 加任何額外條件。 - S12 · premise_audit · G2, L_T_iso — 三個像點可逐坐標重算；引理在 S12.1 證明。本步只作一致性核對，不宣稱 SSS 判定需要找到這樣的映射。 - S11 · premise_audit · S02, S04, S10, mko_sss_slice — 方向只由行列式的正負讀出；本步不宣稱「方向相同」是全等的必要條件，反而說明它不是。 - S10 · sufficient_goal_reduction · S01, S03, S04, S09, mko_sss_slice — 目標 G：G(A,B)。足夠條件 H：兩者非退化且三組對應邊等長；H⇒G 由 SSS 切片。H 由 S03、S04、S09 從 G2 正向證成，沒有把 G 當作前提。 - S09 · premise_audit · S05, S08, sqrt_def — 需要長度非負，這由距離公式保證；具體長度值只是說明，判定本身只用平方相等。 - S08 · premise_audit · S06, S07, eq_refl_symm_trans — 只需 S06 與 S07 的六個值。若有不等，依 12、13、23 的既定順序遇到的第一組不等才是首個見證；其後也不等的組不會因此成為首組。S13 的另一個對應正是這種情形。 - S07 · inverse_equivalence · dist_formula, numeric_evaluation — 重算見 N6、N7、N8；兩邊是同一個數。 - S06 · inverse_equivalence · dist_formula, numeric_evaluation — 每個值都可由公式重算（N3、N4、N5），左右兩邊是同一個數。 - S05.3 · premise_audit · S05.2, zero_product, order_basics — 情況二用到 u、v≥0；沒有這個條件，u=2、v=−2 會使 u²=v² 而 u≠v。 - S05.2 · inverse_equivalence · distributive, eq_congruence, add_inverse — 減 v² 與加 v² 互為反運算，展開是恆等式，所以雙向成立。 - S05.1 · premise_audit · eq_congruence — 此子步只宣稱 ⇒；反向需要非負條件，在 S05.3 處理。 - S05 · inverse_equivalence · L_sq_eq, dist_formula — 引理兩個方向都在子步證明，前提 u、v≥0 由距離非負提供；若允許負數，平方相等不能推回原數相等（例如 2 與 −2）。 - S04 · premise_audit · G2, det2_def, det_collinear — 重算見 N2；判定只用 det≠0 ⇒ 不共線，負號不影響資格。 - S03 · premise_audit · S02, det_collinear — 只用到「det≠0 ⇒ 不共線」這一方向；本步不宣稱其他三角形性質。 - S02 · inverse_equivalence · det2_def, numeric_evaluation — 反向重算（N1）：12=4·3−0·0 正是兩行（row）(4,0)、(0,3) 的行列式；兩式表示同一個數。 - S01 · premise_audit · G1, G2, mko_sss_slice — 此步只寫出本稿使用的判準，不推出新事實；判準只在 MKO 的切片（同一正交平面、明示對應）內使用。 ## 錯誤控制與反例方向相反不是不全等MKO 列出的誤解之一是把鏡射造成的方向反轉當成不全等。本例 det 為 12 與 −12，方向相反，但 SSS 切片只看非退化與三組對應邊長，與方向無關（S11）；S12 更找到把 A 送到 B 的鏡射加平移。方向只說明是否需要鏡射，不決定全等與否。先驗資格與對應，再比邊MKO 也警告忽略非退化與標記對應、或猜圖形全等。D、D' 的對應邊相等，但它們共線，不是三角形（S14）；所以非退化必須先驗。另一方面，對應是給定的，不能自行重排：在 A1↔B1、A2↔B3、A3↔B2 下第 12 組就不等（S13），而這只否定那個對應，不否定 Ai↔Bi 下的全等。比較平方需要非負以平方長度代替長度的依據是引理 L_sq_eq，它要求兩數都非負。距離非負，所以可用；但同樣的推理不能用在可正可負的量上（2 與 −2 平方相等）。平方比較也避免了 √25 之類的近似誤差：所有比較都是整數相等。 - det(A) 與 det(B) 異號，所以 A 與 B 不全等 → reject — 異號只表示方向相反；SSS 切片的三組對應邊的平方長度 16、9、25 全部相等，A、B 全等（S10、S11）。 - 對應 A1↔B1、A2↔B3、A3↔B2 在第 12 組不等，所以 A 與 B 不全等 → reject — 這只否定該對應；在明示對應 Ai↔Bi 下 A、B 全等。 - D 與 D' 的對應平方邊長都是 2、8、2，所以它們是全等三角形 → reject — det((1,1),(2,2))=0，兩者共線，不是非退化三角形，不在本條目的適用範圍。 - 兩組對應邊相等就足以判定全等 → reject — P=((0,0),(5,0),(3,4)) 與 Q=((0,0),(5,0),(4,3)) 都非退化，第 12、13 組平方邊長都是 25、25，但第 23 組是 20 與 10。 ## 結論與限制兩組點都是非退化三角形（行列式 12 與 −12）。在明示對應 Ai↔Bi 下，三組對應平方邊長依 12、13、23 順序都是 16、9、25，所以 A 與 B 全等，邊長為 4、3、5。B 的方向與 A 相反（B 是 A 關於 y=x 鏡射再平移 (1,1) 的像），但這不破壞全等。另一個對應 A1↔B1、A2↔B3、A3↔B2 的首個不等見證是第 12 組（16≠9），只否定該對應；共線點組 D、D' 雖然對應邊相等，但不合格。 - SSS 切片取自 MKO，本稿不從「全等即存在等距映射」的定義去證明它；S12 的映射只是與結論一致的交叉核對。 - det_collinear（三點共線 ⇔ 差向量行列式為 0）是本稿的前提，未在本稿中證明。 - 本稿只檢查題目給定的兩個對應，不搜尋其餘四個頂點排列。 ## 驗證及來源綁定 16 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 83caa0f7f586d45c5a409ca376921926f4b747c37d11d7d8431e892c2d0e380c - original source SHA-256: 727649daf1fc5c011c5f0341aae0d1188360a7ed505f2b639965409a85d8281c - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-congruence-01.json)