全等：以 SSS 切片判定有明示對應的三角形全等

目標與範圍

在同一個等單位正交平面中，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 — 實數的序：任兩數恰有 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。
• 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|²。

逐步主鏈

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)

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

\det((4,0),(0,3))=4\cdot 3-0\cdot 0=12

\det(A_2-A_1,\,A_3-A_1)=12\neq 0

A_1,A_2,A_3\ \text{distinct, noncollinear: }A\ \text{nondegenerate}

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

|A_iA_j|=|B_iB_j|

|A_iA_j|^2=|B_iB_j|^2

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

16,\ 9,\ 25

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

16,\ 9,\ 25

(16,9,25)\ \text{vs}\ (16,9,25)

|A_iA_j|^2=|B_iB_j|^2\ (ij=12,13,23)

|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

A,B\ \text{nondegenerate},\ |A_iA_j|=|B_iB_j|\ (ij=12,13,23)

G(A,B)\ \text{under}\ A_i\leftrightarrow B_i

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

T(x,y)=(y+1,\,x+1)

T(A_1)=B_1,\ T(A_2)=B_2,\ T(A_3)=B_3

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

D=((0,0),(1,1),(2,2))

\det((1,1),(2,2))=1\cdot 2-1\cdot 2=0:\ D\ \text{collinear, not eligible}

局部子步與引理

u=v

u^2=v^2

u^2=v^2

(u-v)(u+v)=0

(u-v)(u+v)=0,\ u\ge 0,\ v\ge 0

u=v

|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

逐步反向審查

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