Geometric transformations: proving the basic isometries and classifying uniform scaling

Goal and scope

On the equal-unit orthonormal real plane, prove that translations, the counterclockwise quarter-turn R90(x,y)=(−y,x) about the origin, and the other rotations and axis reflections listed in the MKO are isometries; that the half-turn (−x,−y) is not a reflection in any of the listed axes; and that uniform scaling Hc(x,y)=(cx,cy) multiplies every distance by |c|. Use this to classify c=0, c=−1, c=−2 and c=2, with a numerical check on P=(3,1), Q=(−1,4).

Treats only the maps listed in the MKO: translations, counterclockwise rotations about the origin by 0°, 90°, 180°, 270°, reflections in the four specified lines, and uniform scaling, with Euclidean distance in an equal-unit orthonormal frame. It does not treat general rotation angles, reflections in general lines, or the full classification of isometries. It does not change the canonical MKO or its English edition.

Givens and symbols

• neg_mul
• distributive
• power_laws
• abs_rules
• sqrt_def
• order_basics
• numeric_evaluation

• G1 — Model: the equal-unit orthonormal real plane ℝ², with domain and codomain the whole plane; distance d(P,Q)=√((x2−x1)²+(y2−y1)²).
• G2 — Maps: translation T(x,y)=(x+tx, y+ty); R90(x,y)=(−y,x); R180(x,y)=(−x,−y); R270(x,y)=(y,−x); reflections in the x-axis (x,−y), the y-axis (−x,y), y=x as (y,x), and y=−x as M(x,y)=(−y,−x); uniform scaling Hc(x,y)=(cx,cy).
• G3 — For numerical checks: P=(3,1), Q=(−1,4); coefficients c=0, −1, 2, −2.

• d(P,Q) — the Euclidean distance between P and Q
• \Delta x,\ \Delta y — the coordinate differences x2−x1 and y2−y1 of Q and P
• R_{90} — counterclockwise quarter-turn about the origin, (x,y)↦(−y,x)
• M — reflection in y=−x, (x,y)↦(−y,−x)
• H_c — uniform scaling (x,y)↦(cx,cy)

Rules and sources

• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• sqrt_def · prerequisite — Principal square root: for a≥0, √a is the unique real b with b≥0 and b²=a. Negative numbers have no real square root.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_transformations · cited — On the equal-unit orthonormal real plane, translations, counterclockwise rotations about the origin by 0°, 90°, 180°, 270°, and reflections across the x-axis, y-axis, y=x and y=−x are isometries. For Hc(x,y)=(cx,cy), c=0 gives a degenerate constant map; |c|=1 gives a whole-plane isometry; any other nonzero c gives a non-isometric similarity with positive length scale |c|. · mko-geometric-transformations
• dist_formula · cited — In one equal-unit orthonormal frame, P=(x1,y1) and Q=(x2,y2) have distance d(P,Q)=√((x2−x1)²+(y2−y1)²)≥0. · mko-distance-formula
• isometry_def · prerequisite — A map H:ℝ²→ℝ² is an isometry when d(H(P),H(Q))=d(P,Q) for all points P and Q. It is a whole-plane property: it must hold for every pair of points.
• L_signed_perm · lemma — If the two coordinates of H(Q)−H(P) are ±Δx and ±Δy (any signs, in either order), then d(H(P),H(Q))=d(P,Q).
• L_sqrt_scale · lemma — For a real c and S≥0: √(c²S)=|c|√S.

Main derivation

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}

Substeps and lemmas

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

Reverse audits

• S15 · sufficient_goal_reduction · S10, S11, S14, case_analysis — Goal G: the MKO's three-way classification. Sufficient condition H: the general equality of S10 plus the analysis of three cases; the cases c=0, |c|=1 and other nonzero c are exclusive and cover all reals. H is proved forwards from S10, without assuming G.
• S14 · premise_audit · S10, G3, quantifier_negation — One pair of distinct points refutes isometry; degeneracy comes from the factor 0 not being positive.
• S13 · premise_audit · S12, S01, quantifier_negation — One counterexample suffices to refute a universal statement; conversely, one fixed point does not suffice to establish it.
• S12 · premise_audit · S10, G3, numeric_evaluation — It can be recomputed (N5, N6, N7); one example cannot replace the general proof in S10.
• S11 · premise_audit · S10, abs_rules, forall_intro — Substitute c=−1 into the general equality of S10; P and Q are arbitrary, so the conclusion is for the whole plane.
• S10.3 · premise_audit · S10.1, S10.2, sqrt_def — Uniqueness is the key: b²=c²S alone is not enough, b≥0 is also needed; when c<0 and S>0, c√S has the right square but is negative and is not the principal root. When S=0, both expressions are 0.
• S10.2 · inverse_equivalence · power_laws, abs_rules, neg_mul, sqrt_def — Each step replaces equals by equals and holds both ways; the two cases for |c|²=c² cover every real c (N10 is only a finite spot check).
• S10.1 · premise_audit · abs_rules, sqrt_def, order_basics — Only nonnegativity is claimed, not positivity (it is 0 when c=0 or S=0).
• S10 · inverse_equivalence · L_sqrt_scale, square_nonneg — The lemma gives an equality, valid both ways; its hypothesis S≥0 follows from squares being nonnegative.
• S09 · inverse_equivalence · distributive, power_laws — Identities, valid both ways; no condition on c.
• S08 · premise_audit · G2, function_def — Two functions differ as soon as their values differ at one point; the step does not claim they differ at every other point.
• S07 · premise_audit · S02, G2, L_signed_perm, forall_intro — Each difference vector can be recomputed coordinatewise from the formulas in G2; the lemma's hypothesis (a signed permutation) is checked case by case.
• S06 · sufficient_goal_reduction · S01, S02, S03, S05, forall_intro — Goal G: T and R90 are isometries. Sufficient condition H: distance is unchanged for an arbitrary pair; H⇒G by the definition. H is proved forwards in S03 and S05, without assuming G; no finite set of pairs replaces the arbitrary pair.
• S05.1 · inverse_equivalence · neg_mul, add_comm, eq_congruence — All identities, valid both ways; all four sign choices and both orders are covered.
• S05 · inverse_equivalence · L_signed_perm — The lemma gives an equality of two expressions, valid both ways; it is proved in S05.1 without circularity.
• S04 · inverse_equivalence · distributive, neg_mul — Coordinatewise identities, valid both ways.
• S03 · inverse_equivalence · dist_formula, add_inverse — Each equality is an identity, so the chain holds both ways; no condition is placed on tx or ty.
• S02 · premise_audit · G1, dist_formula, def_intro — It only names and states the formula; the arbitrariness of P and Q is what S06 needs for generalization.
• S01 · premise_audit · G1, isometry_def — This step only states the definition and derives no new fact.

Error controls and negative controls

A negative coefficient is not a negative length scale

One misconception the MKO lists is reading a negative coefficient as a negative length scale. S10 proves that distances are multiplied by |c|: c=−2 has scale 2 (distance 5 becomes 10, S12), and c=−1 is even an isometry (S11). At fixed |c|, the negative sign adds a half-turn without changing the length factor relative to +|c|. The complete coefficient c=−2 still doubles lengths; its sign never makes a distance negative.

One fixed point does not give global isometry

H2 fixes the origin, yet d(H2(P),H2(Q))=10≠5. Isometry is a universal whole-plane property (S01): establishing it needs an argument for an arbitrary pair (as in S06), and refuting it needs one counterexample (S13). Inferring isometry from one coincident or fixed point is exactly what MKO assumption a3 forbids.

State the rotation direction, centre and mirror axis

The counterclockwise quarter-turn is (x,y)↦(−y,x), sending (1,0) to (0,1); the clockwise one is (y,−x), which is R270 here and sends (1,0) to (0,−1). The half-turn (−x,−y) is not the x-axis reflection: that reflection fixes (1,0) while the half-turn sends it to (−1,0) (S08). Mixing up directions or axes gives wrong image points even though the map is still an isometry.

• H(−2) has length scale −2 → reject — Distances are multiplied by |−2|=2; the distance of P and Q goes from 5 to 10 (S10, S12).
• H2 fixes the origin, so H2 is an isometry → reject — d(H2(P),H2(Q))=10≠5=d(P,Q).
• The half-turn (x,y)↦(−x,−y) is the reflection in the x-axis → reject — The x-axis reflection sends (1,0) to (1,0); the half-turn sends it to (−1,0).
• No uniform scaling with a negative coefficient is an isometry → reject — For c=−1, |c|=1 and H(−1) is the half-turn, an isometry (S11).
• The counterclockwise quarter-turn about the origin sends (1,0) to (0,−1) → reject — R90(1,0)=(−0,1)=(0,1); (0,−1) is the clockwise image (R270).

Result and limitations

Translations, R0, R90, R180, R270 and the reflections in the x-axis, the y-axis, y=x and y=−x preserve the distance of any two points, so they are isometries; the half-turn (−x,−y) fixes only the origin and is not a reflection in any of these axes. Uniform scaling satisfies d(Hc(P),Hc(Q))=|c|d(P,Q): c=0 is a degenerate constant map; c=±1 are isometries (c=−1 is the half-turn); every other nonzero c, for example c=2 or c=−2, is a non-isometric similarity of scale |c|, turning the distance 5 of P=(3,1), Q=(−1,4) into 10. That H2 fixes the origin does not change this.

• This guide proves isometry only for the finitely many formula types or map families listed in the MKO (translation parameters still range over arbitrary reals); it does not treat rotations by general angles, reflections in general lines, or the complete classification of plane isometries.
• N10 is a finite spot check of |c|²=c² at the integers from −5 to 5; the general proof is the two-case argument of S10.2.

Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.

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

Same-source full JSON (formulas, ASTs, controls and revision log)