Transformation Proof

Prove geometric statements by applying transformations and analyzing what properties are preserved.

The Key Insight

Transformations map figures to congruent or similar figures while preserving key properties. If we can transform one configuration into another, they share all preserved properties.

Step 1: Identify the Transformation

Isometries (Preserve Distance)

Similarities (Preserve Shape)

What Each Preserves

Step 2: Set Up the Transformation

• • Identify what to transform (which figure or points)
• • Choose transformation parameters (center, angle, axis, vector)
• • Determine where key points map

Notation

• •T_v: Translation by vector v
• •R_O,θ: Rotation by angle θ about point O
• •S_ℓ: Reflection across line ℓ
• •D_O,k: Dilation with center O and ratio k

Key Relationships

Rotation: If R_O,θ(A) = A', then:

• •OA = OA' (radii)
• •∠AOA' = θ

Reflection: If S_ℓ(A) = A', then:

• •ℓ is perpendicular bisector of AA'
• •If A is on ℓ, then A' = A

Dilation: If D_O,k(A) = A', then:

• •O, A, A' are collinear
• •OA'/OA = k

Step 3: Apply and Analyze

• • Apply transformation to relevant points/figures
• • Identify what maps to what
• • Use preservation properties to draw conclusions

Common Proof Strategies

Show congruence: Find an isometry mapping one figure to another.

Show similarity: Find a similarity transformation connecting figures.

Use symmetry: If figure has symmetry, use the symmetry transformation.

Composition: Combine transformations (e.g., two reflections = rotation).

Step 4: Lean Formalization

import Mathlib.Geometry.Euclidean.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2

-- Rotation in ℝ²
def rotate2 (θ : ℝ) (p : ℝ × ℝ) : ℝ × ℝ :=
  (p.1 * Real.cos θ - p.2 * Real.sin θ,
   p.1 * Real.sin θ + p.2 * Real.cos θ)

-- Reflection across x-axis
def reflectX (p : ℝ × ℝ) : ℝ × ℝ := (p.1, -p.2)

-- Rotation preserves distance from origin
theorem rotate_preserves_norm (θ : ℝ) (p : ℝ × ℝ) :
    (rotate2 θ p).1^2 + (rotate2 θ p).2^2 = p.1^2 + p.2^2 := by
  simp [rotate2]
  ring_nf
  rw [Real.cos_sq_add_sin_sq]
  ring

-- Two reflections = rotation
theorem two_reflections_rotation (p : ℝ × ℝ) :
    reflectX (reflectX p) = p := by
  simp [reflectX]

Example: Prove Angle Sum using Rotation

Problem: Prove that the angles of a triangle sum to 180°.

Proof using transformations:

Consider triangle ABC. We perform rotations:

1. •Rotate 180° about the midpoint M_AB of side AB
2. •Rotate 180° about the midpoint M_BC of side BC

After both rotations, vertex A maps to a point A'', and:

• •The angles at A, B, C together form a straight line at the image
• •Therefore ∠A + ∠B + ∠C = 180°

Example: Prove Regular Hexagon Property using Rotation

Problem: In regular hexagon ABCDEF, prove AC = 2·AB.

Proof:

The regular hexagon has 6-fold rotational symmetry about its center O.

By rotational symmetry (R_O,60°):

• •All sides are equal: AB = BC = CD = DE = EF = FA
• •O is equidistant from all vertices

Connect O to all vertices, creating 6 equilateral triangles. Each central angle is 360°/6 = 60°. Since OA = OB = AB (equilateral), triangle OAB is equilateral.

Now for diagonal AC:

• •Triangle OAC contains angle ∠AOC = 120° (two 60° central angles)
• •OA = OC (radii)
• •By the Law of Cosines or noting this creates two equilateral triangles: AC = AB√3...

Actually, using the 30-60-90 triangle formed: AC = 2 · AB · cos(30°) = AB√3.

Output Format

**Theorem:** [Statement]

**Transformation Approach:**
[Identify which transformation to use and why]

**Setup:**
- Transform: [Description with parameters]
- Maps: [A → A', B → B', ...]

**Analysis:**
[Use preserved properties to derive conclusion]

**Conclusion:**
[Final statement]

**Lean Proof:**
[Formal verification]

Common Pitfalls

1. •Wrong center/axis: The transformation parameters must be chosen so points map correctly
2. •Orientation issues: Reflections reverse orientation; compositions of two reflections preserve it
3. •Not checking well-defined: Ensure the transformation is properly defined (e.g., rotation angle, dilation center not on the figure when k ≠ 1)
4. •Forgetting fixed points: The fixed points of a transformation often play a key role

Advanced Techniques

Composition Rules

Symmetry Arguments

If a figure is invariant under transformation T, then:

• •Any property preserved by T holds for corresponding parts
• •Fixed points of T lie on symmetry elements

Finding the Transformation

Given two congruent figures:

• •Same orientation → rotation or translation
• •Opposite orientation → reflection or glide reflection
• •Find corresponding points to determine parameters