# 幾何變換：證明基本等距並分類均勻縮放

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

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

derivation-mko-geometric-transformations-01 · production-20261019-adopted-96



## 目標與範圍

在等單位正交實平面中證明：平移、原點逆時針 90° 旋轉 R90(x,y)=(−y,x) 以及 MKO 列出的其他旋轉與軸鏡射都是等距映射；半轉 (−x,−y) 不是所列四條軸中任何一條的鏡射；均勻縮放 Hc(x,y)=(cx,cy) 使每個距離乘 |c|。據此分類 c=0、c=−1、c=−2、c=2，並以 P=(3,1)、Q=(−1,4) 做數值核對。

只處理 MKO 列出的映射：平移、繞原點逆時針 0°、90°、180°、270° 旋轉、四條指定軸的鏡射、均勻縮放；距離用等單位正交座標的歐氏距離。不處理一般旋轉角、一般直線鏡射或等距映射的完整分類。不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- neg_mul
- distributive
- power_laws
- abs_rules
- sqrt_def
- order_basics
- numeric_evaluation


- G1 — 模型：等單位正交實平面 ℝ²，定義域與陪域都是整個平面；距離為 d(P,Q)=√((x2−x1)²+(y2−y1)²)。
- G2 — 映射：平移 T(x,y)=(x+tx, y+ty)；R90(x,y)=(−y,x)；R180(x,y)=(−x,−y)；R270(x,y)=(y,−x)；鏡射 x 軸 (x,−y)、y 軸 (−x,y)、y=x 為 (y,x)、y=−x 為 M(x,y)=(−y,−x)；均勻縮放 Hc(x,y)=(cx,cy)。
- G3 — 數值核對用：P=(3,1)、Q=(−1,4)；係數 c=0、−1、2、−2。


- d(P,Q) — P、Q 的歐氏距離
- \Delta x,\ \Delta y — Q 與 P 的座標差 x2−x1、y2−y1
- R_{90} — 繞原點逆時針 90° 旋轉 (x,y)↦(−y,x)
- M — 關於 y=−x 的鏡射 (x,y)↦(−y,−x)
- H_c — 均勻縮放 (x,y)↦(cx,cy)





## 規則與來源


- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
- 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 — 明確整數或有理數算式的精確求值；可以獨立重算。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- add_zero · prerequisite — 加法單位元：u+0=u。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
- two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
- zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- mko_transformations · cited — 在等單位正交實平面，平移、原點逆時針 0／90／180／270 度旋轉及關於 x 軸、y 軸、y=x、y=−x 的鏡射均為等距映射。均勻縮放 Hc(x,y)=(cx,cy)：c=0 是退化常值映射，|c|=1 是全平面等距，其他非零 c 是正倍率 |c| 的非等距相似映射。 · mko-geometric-transformations
- dist_formula · cited — 在同一等單位正交座標系，P=(x1,y1)、Q=(x2,y2) 的距離為 d(P,Q)=√((x2−x1)²+(y2−y1)²)≥0。 · mko-distance-formula
- isometry_def · prerequisite — 映射 H:ℝ²→ℝ² 是等距映射，指對所有點 P、Q 都有 d(H(P),H(Q))=d(P,Q)。這是全平面性質：要對每一對點成立。
- L_signed_perm · lemma — 若 H(Q)−H(P) 的兩個坐標是 ±Δx 與 ±Δy（任意正負號，順序可對調），則 d(H(P),H(Q))=d(P,Q)。
- L_sqrt_scale · lemma — 對實數 c 與 S≥0：√(c²S)=|c|√S。





## 逐步主鏈

S01 · definition操作前

H:\mathbb{R}^2\to\mathbb{R}^2

操作後

H\ \text{isometry}\iff\forall P,Q\in\mathbb{R}^2:\ d(H(P),H(Q))=d(P,Q)

條件：無

規則：isometry_def · 依賴：G1, isometry_def

葉節點依據：isometry_def + def_unfold

固定要證明的性質：等距是對「所有」點對成立的全平面性質。要證明某映射是等距，必須對任意一對點證明；要否定，只需一對點的反例。距離採 G1 的歐氏距離。



S02 · definition操作前

P=(x_1,y_1),\ Q=(x_2,y_2)\ \text{arbitrary}

操作後

\Delta x=x_2-x_1,\ \Delta y=y_2-y_1,\ d(P,Q)=\sqrt{\Delta x^2+\Delta y^2}

條件：無

規則：dist_formula · 依賴：G1, dist_formula

葉節點依據：def_intro + dist_formula

取任意兩點 P、Q，不對它們加任何條件，並為座標差取名 Δx、Δy。依距離公式 d(P,Q)=√(Δx²+Δy²)。之後各映射的論證都對這一對任意點進行，最後才能用全稱推廣。



S03 · equivalent操作前

d(T(P),T(Q))

操作後

\sqrt{((x_2+t_x)-(x_1+t_x))^2+((y_2+t_y)-(y_1+t_y))^2}=\sqrt{\Delta x^2+\Delta y^2}=d(P,Q)

條件：無

規則：dist_formula · 依賴：S02, G2

葉節點依據：dist_formula + add_assoc + add_comm + add_inverse + add_zero

平移：T(Q)−T(P) 的坐標是 (x2+tx)−(x1+tx)=Δx 與 (y2+ty)−(y1+ty)=Δy（加法結合、交換與反元素消去 tx、ty；N1 核對）。根號內完全相同，所以 d(T(P),T(Q))=d(P,Q)。



S04 · equivalent操作前

R_{90}(Q)-R_{90}(P)

操作後

(-y_2-(-y_1),\ x_2-x_1)=(-\Delta y,\ \Delta x)

條件：無

規則：distributive · 依賴：S02, G2

葉節點依據：distributive + neg_mul + eq_replace

R90(P)=(−y1, x1)、R90(Q)=(−y2, x2)。第一坐標 −y2−(−y1)=−(y2−y1)=−Δy（負號分配，N2 核對），第二坐標 x2−x1=Δx。旋轉方向是逆時針：(1,0) 送到 (0,1)。



S05 · equivalent操作前

d(R_{90}(P),R_{90}(Q))

操作後

\sqrt{(-\Delta y)^2+\Delta x^2}=\sqrt{\Delta x^2+\Delta y^2}=d(P,Q)

條件：無

規則：L_signed_perm · 依賴：S04

葉節點依據：neg_mul + add_comm + eq_congruence

R90(Q)−R90(P)=(−Δy, Δx) 的兩個坐標正是帶正負號、順序對調的 Δy 與 Δx，所以依引理 L_signed_perm，d(R90(P),R90(Q))=d(P,Q)。引理在 S05.1 證明。



S06 · implies操作前

d(T(P),T(Q))=d(P,Q),\ d(R_{90}(P),R_{90}(Q))=d(P,Q)\ \text{for arbitrary}\ P,Q

操作後

T\ \text{and}\ R_{90}\ \text{are isometries}

條件：無

規則：forall_intro · 依賴：S02, S03, S05, S01

葉節點依據：forall_intro + isometry_def

S03、S05 的等式是對 S02 中任意的 P、Q 證明的，沒有對它們加條件；依全稱推廣，對所有點對成立。依 S01 的定義，平移 T 與 R90 都是等距映射。



S07 · implies操作前

R_{180},\ R_{270},\ \text{reflections in }x\text{-axis},\ y\text{-axis},\ y=x,\ y=-x

操作後

(-\Delta x,-\Delta y),\ (\Delta y,-\Delta x),\ (\Delta x,-\Delta y),\ (-\Delta x,\Delta y),\ (\Delta y,\Delta x),\ (-\Delta y,-\Delta x):\ \text{all isometries}

條件：無

規則：L_signed_perm · 依賴：S02, G2, S05, S01

葉節點依據：L_signed_perm + forall_intro + distributive + neg_mul

逐一寫出 H(Q)−H(P)：R180 為 (−Δx,−Δy)；R270(x,y)=(y,−x) 為 (Δy,−Δx)；x 軸鏡射為 (Δx,−Δy)；y 軸鏡射為 (−Δx,Δy)；y=x 鏡射為 (Δy,Δx)；y=−x 鏡射 M 為 (−Δy,−Δx)。每一個都是帶正負號的 Δx、Δy（可能對調），所以依引理 L_signed_perm 與全稱推廣（同 S06），六個映射都是等距；R0 是恆等映射，顯然等距。



S08 · implies操作前

R_{180}(x,y)=(-x,-y)

操作後

R_{180}\ \text{differs from each of the four axis reflections}

條件：無

規則：function_def · 依賴：G2, function_def

葉節點依據：function_def + numeric_evaluation + two_nonzero + zero_product

鏡射固定其軸上每一點：x 軸鏡射固定 (1,0)，y 軸鏡射固定 (0,1)，y=x 鏡射固定 (1,1)，y=−x 鏡射 M 固定 (1,−1)（M(1,−1)=(1,−1)）。半轉 (−x,−y)=(x,y) 當且僅當 2x=0 且 2y=0，即只固定原點；所以 R180 把這四點分別送到 (−1,0)、(0,−1)、(−1,−1)、(−1,1)，與四個鏡射在各自的點上取值不同。依函數相等的定義，R180 不是其中任何一個鏡射；它是中心反演，也就是半轉。



S09 · equivalent操作前

H_c(Q)-H_c(P)

操作後

(c\Delta x,\ c\Delta y),\quad (c\Delta x)^2+(c\Delta y)^2=c^2(\Delta x^2+\Delta y^2)

條件：無

規則：distributive · 依賴：S02, G2

葉節點依據：distributive + power_laws + mul_comm

Hc(Q)−Hc(P)=(cx2−cx1, cy2−cy1)=(cΔx, cΔy)（分配律）。平方和為 c²Δx²+c²Δy²=c²(Δx²+Δy²)（(ab)²=a²b² 與分配律；N4 核對）。



S10 · equivalent操作前

d(H_c(P),H_c(Q))=\sqrt{c^2(\Delta x^2+\Delta y^2)}

操作後

|c|\sqrt{\Delta x^2+\Delta y^2}=|c|\,d(P,Q)

條件：S=\Delta x^2+\Delta y^2\ge 0

規則：L_sqrt_scale · 依賴：S09, S02

葉節點依據：sqrt_def + abs_rules + power_laws + order_basics + square_nonneg

令 S=Δx²+Δy²≥0（平方和非負）。依引理 L_sqrt_scale，√(c²S)=|c|√S，所以 d(Hc(P),Hc(Q))=|c|d(P,Q)。重點是乘的是 |c|，不是 c：距離不會是負數。引理在 S10.1 至 S10.3 證明。



S11 · implies操作前

c=-1:\ d(H_{-1}(P),H_{-1}(Q))=|-1|\,d(P,Q)

操作後

H_{-1}=R_{180}\ \text{is an isometry}

條件：無

規則：forall_intro · 依賴：S10, G2

葉節點依據：abs_rules + forall_intro + numeric_evaluation

|−1|=1，所以對任意 P、Q 距離不變，H(−1) 是等距；而且 H(−1)(x,y)=(−x,−y) 正是半轉 R180，與 S07 一致。這說明負係數不一定破壞等距。



S12 · implies操作前

c=-2,\ P=(3,1),\ Q=(-1,4)

操作後

d(P,Q)=5,\ d(H_{-2}(P),H_{-2}(Q))=10=|-2|\cdot 5

條件：無

規則：numeric_evaluation · 依賴：S10, G3

葉節點依據：numeric_evaluation + dist_formula

數值核對：Q−P=(−4,3)，d(P,Q)=√(16+9)=5。H(−2)(P)=(−6,−2)、H(−2)(Q)=(2,−8)，差為 (8,−6)，距離 √(64+36)=10=2·5。倍率是 |−2|=2，與 S10 一致；不是 −2，也不是 −10。這只是一個例子，一般結論來自 S10。



S13 · implies操作前

c=2:\ H_2(0,0)=(0,0),\ d(H_2(P),H_2(Q))=10\neq 5=d(P,Q)

操作後

H_2\ \text{is not an isometry}

條件：無

規則：quantifier_negation · 依賴：S12, S01

葉節點依據：quantifier_negation + isometry_def + numeric_evaluation

|2|=|−2|，所以同一對 P、Q 在 H2 下距離也是 10≠5。等距要求對所有點對成立，否定它只需一個反例：¬∀ 等於 ∃¬。雖然 H2 固定原點（一個不變點），這不能證明全平面等距，MKO 假設 a3 正是這個警告。



S14 · implies操作前

c=0:\ H_0(x,y)=(0,0)

操作後

d(H_0(P),H_0(Q))=0\neq 5:\ \text{degenerate constant map, not an isometry}

條件：無

規則：quantifier_negation · 依賴：S10, G3, S12

葉節點依據：quantifier_negation + numeric_evaluation

c=0 時每一點都送到原點，是常值映射。對相異的 P、Q，d(P,Q)=5>0 但像的距離為 0。倍率 |0|=0 不是正數，所以它既不是等距，也不是 MKO 意義下的正倍率相似映射，而是退化映射。



S15 · case_split操作前

d(H_c(P),H_c(Q))=|c|\,d(P,Q)\ \forall P,Q

操作後

c=0:\ \text{degenerate};\ |c|=1:\ \text{isometry};\ \text{other }c\neq 0:\ \text{similarity of scale }|c|,\ \text{not an isometry}

條件：無

規則：case_analysis · 依賴：S10, S11, S13, S14, S06, S07

葉節點依據：case_analysis + abs_rules + quantifier_negation + forall_intro

分三種情況涵蓋所有實數 c。c=0：S14，退化常值映射。|c|=1（c=1 恆等、c=−1 半轉）：S10 給出距離不變，等距。其他非零 c：S10 給出每個距離乘正數 |c|，所以是倍率 |c| 的相似映射；又 |c|≠1，取 P=(0,0)、Q=(1,0)，d(P,Q)=1 而像的距離 |c|≠1，所以不是等距。這與 MKO 的分類一致。







## 局部子步與引理

S05.1 · equivalent操作前

(\sigma_1 a)^2+(\sigma_2 b)^2,\ \sigma_i\in\{1,-1\},\ \{a,b\}=\{\Delta x,\Delta y\}

操作後

a^2+b^2=\Delta x^2+\Delta y^2

條件：無

規則：neg_mul · 依賴：neg_mul, add_comm, eq_congruence

葉節點依據：neg_mul + add_comm + eq_congruence + case_analysis

σ=−1 時 (−a)²=(−a)(−a)=a²（負負得正），σ=1 時顯然；所以 (σ1a)²+(σ2b)²=a²+b²（N3 核對）。a、b 是 Δx、Δy 的某種順序，依加法交換 a²+b²=Δx²+Δy²。兩個根號內相等，依等式的合同性根號值相等，即 d(H(P),H(Q))=d(P,Q)。這證得引理 L_signed_perm。



S10.1 · implies操作前

|c|\ge 0,\ \sqrt S\ge 0

操作後

|c|\sqrt S\ge 0

條件：S\ge 0

規則：order_basics · 依賴：abs_rules, sqrt_def, order_basics

葉節點依據：abs_rules + sqrt_def + order_basics + mul_zero + case_analysis

|c|≥0（絕對值非負），√S≥0（主平方根非負）；兩個非負數之積非負（若其一為 0 積為 0，否則正乘正為正）。



S10.2 · equivalent操作前

(|c|\sqrt S)^2

操作後

|c|^2(\sqrt S)^2=c^2S

條件：S\ge 0

規則：power_laws · 依賴：abs_rules, neg_mul, sqrt_def, power_laws

葉節點依據：power_laws + abs_rules + neg_mul + sqrt_def + case_analysis

(ab)²=a²b² 給出 |c|²(√S)²。|c|²=c²：若 c≥0，|c|=c；若 c<0，|c|=−c，(−c)²=c²（負負得正）。(√S)²=S 由主平方根定義。所以 (|c|√S)²=c²S。



S10.3 · implies操作前

b=|c|\sqrt S\ge 0,\ b^2=c^2S

操作後

\sqrt{c^2S}=|c|\sqrt S

條件：c^2S\ge 0

規則：sqrt_def · 依賴：S10.1, S10.2, sqrt_def

葉節點依據：sqrt_def + abs_rules + power_laws + order_basics

c²S≥0，所以 √(c²S) 是唯一滿足 b≥0 且 b²=c²S 的實數 b。由 S10.1、S10.2，b=|c|√S 滿足這兩個條件，依唯一性 √(c²S)=|c|√S。S10.1 至 S10.3 合起來證得引理 L_sqrt_scale。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S10, S11, S14, case_analysis — 目標 G：MKO 的三分類。足夠條件 H：S10 的一般等式加上三個情況的分析；三個情況（c=0、|c|=1、其他非零 c）互斥且涵蓋全部實數。H 由 S10 正向證成，未把 G 當作前提。
- S14 · premise_audit · S10, G3, quantifier_negation — 一對相異點即足以否定等距；退化的判斷來自倍率 0 不是正數。
- S13 · premise_audit · S12, S01, quantifier_negation — 一個反例足以否定全稱命題；反過來，一個不變點不足以肯定它。
- S12 · premise_audit · S10, G3, numeric_evaluation — 可重算（N5、N6、N7）；一個例子不能取代 S10 的一般證明。
- S11 · premise_audit · S10, abs_rules, forall_intro — 用 S10 的一般等式代入 c=−1；P、Q 任意，所以是全平面結論。
- S10.3 · premise_audit · S10.1, S10.2, sqrt_def — 關鍵是唯一性：只驗 b²=c²S 不夠，還需 b≥0；c<0 且 S>0 時，c√S 雖平方正確卻為負，不是主平方根；S=0 時兩式都為0。
- S10.2 · inverse_equivalence · power_laws, abs_rules, neg_mul, sqrt_def — 每一步都是等式代換，雙向成立；|c|²=c² 的兩個情況涵蓋所有實數 c（N10 只是有限抽查）。
- S10.1 · premise_audit · abs_rules, sqrt_def, order_basics — 只宣稱非負，不宣稱為正（c=0 或 S=0 時為 0）。
- S10 · inverse_equivalence · L_sqrt_scale, square_nonneg — 引理給出兩式相等，雙向成立；前提 S≥0 由平方非負保證。
- S09 · inverse_equivalence · distributive, power_laws — 恆等變形，雙向成立；對 c 沒有條件。
- S08 · premise_audit · G2, function_def — 兩函數不等只需一點取值不同；本步不宣稱 R180 與鏡射在其他點都不同。
- S07 · premise_audit · S02, G2, L_signed_perm, forall_intro — 每個差向量都可由 G2 的公式逐坐標重算；引理的條件（帶號置換）逐一檢查成立。
- S06 · sufficient_goal_reduction · S01, S02, S03, S05, forall_intro — 目標 G：T、R90 是等距。足夠條件 H：對任意點對距離不變；H⇒G 由定義。H 由 S03、S05 正向證成，未把 G 當作前提；沒有用任何有限點對代替任意點對。
- S05.1 · inverse_equivalence · neg_mul, add_comm, eq_congruence — 全是恆等式，雙向成立；四種正負號與兩種順序都涵蓋。
- S05 · inverse_equivalence · L_signed_perm — 引理給出的是兩個式子的相等，雙向成立；引理在 S05.1 證明，沒有循環。
- S04 · inverse_equivalence · distributive, neg_mul — 逐坐標的恆等變形，雙向成立。
- S03 · inverse_equivalence · dist_formula, add_inverse — 每個等號都是恆等式，整條鏈雙向成立；沒有對 tx、ty 加條件。
- S02 · premise_audit · G1, dist_formula, def_intro — 只取名並寫出公式；P、Q 的任意性是 S06 使用全稱推廣的前提。
- S01 · premise_audit · G1, isometry_def — 此步只寫出定義，不推出新事實。





## 錯誤控制與反例

負係數不是負長度倍率MKO 的誤解之一是把負係數當負長度倍率。S10 證明距離乘的是 |c|：c=−2 的倍率是 2（距離 5 變 10，S12），c=−1 甚至是等距（S11）。在固定 |c| 下，係數的負號額外帶來半轉效果，不改變相對於 +|c| 的長度倍率；完整係數 c=−2 仍把長度放大 2 倍。距離不會因負號變成負數。

一個不變點不推出全域等距H2 固定原點，但 d(H2(P),H2(Q))=10≠5。等距是全平面的全稱性質（S01）：肯定它要對任意點對證明（S06 的作法），否定它只需一個反例（S13）。從一個重合點或不變點推論等距是 MKO 假設 a3 明言禁止的。

旋轉方向、中心與鏡射軸要明示逆時針 90° 是 (x,y)↦(−y,x)，把 (1,0) 送到 (0,1)；順時針 90° 則是 (y,−x)，即本稿的 R270，把 (1,0) 送到 (0,−1)。半轉 (−x,−y) 不是 x 軸鏡射：x 軸鏡射固定 (1,0)，半轉把它送到 (−1,0)（S08）。混用方向或軸會得到錯誤的像點，即使它仍是等距。


- H(−2) 的長度倍率是 −2 → reject — 距離乘 |−2|=2；P、Q 的距離由 5 變 10（S10、S12）。
- H2 固定原點，所以 H2 是等距映射 → reject — d(H2(P),H2(Q))=10≠5=d(P,Q)。
- 半轉 (x,y)↦(−x,−y) 就是關於 x 軸的鏡射 → reject — x 軸鏡射把 (1,0) 送到 (1,0)，半轉把它送到 (−1,0)。
- 係數為負的均勻縮放都不是等距 → reject — c=−1 時 |c|=1，H(−1) 是半轉，是等距（S11）。
- 繞原點逆時針 90° 把 (1,0) 送到 (0,−1) → reject — R90(1,0)=(−0,1)=(0,1)；(0,−1) 是順時針（R270）的像。





## 結論與限制

平移、R0、R90、R180、R270 與關於 x 軸、y 軸、y=x、y=−x 的鏡射，對任意兩點都保持距離，所以都是等距映射；半轉 (−x,−y) 只固定原點，不是所列四條軸中任何一條的鏡射。均勻縮放滿足 d(Hc(P),Hc(Q))=|c|d(P,Q)：c=0 是退化常值映射；c=±1 是等距（c=−1 即半轉）；其他非零 c（例如 c=2、c=−2）是倍率 |c| 的非等距相似映射，P=(3,1)、Q=(−1,4) 的距離 5 變成 10。H2 固定原點也不改變這個結論。


- 本稿只證明 MKO 列出的有限種公式或映射族（平移參數仍可為任意實數）是等距；不處理一般角度旋轉、一般直線鏡射或平面等距的完整分類。
- N10 是 |c|²=c² 在 −5 到 5 的整數上的有限抽查；一般證明在 S10.2 用兩個情況完成。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: b2381974fe84d166a9e1c4c15b5317ce2f5a357d19a292ebdd8111cd97ee96cf
- original source SHA-256: e7f90378f82483f1ef33bf0f1ac86bbee7369e81b121701b1725f67cb43d1d8d
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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