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

目標與範圍

在等單位正交實平面中證明：平移、原點逆時針 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。

逐步主鏈

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)

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}

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)

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

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

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

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

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}

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}

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

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

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)

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)

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

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

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

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

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}

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}

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}

局部子步與引理

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

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

|c|\sqrt S\ge 0

(|c|\sqrt S)^2

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

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

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

逐步反向審查

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