Coordinate Proof

Prove geometric statements by placing figures in a coordinate system and using algebraic computations.

The Key Insight

Geometric relationships become algebraic equations. Distance, angle, and position relationships can all be verified through computation.

Step 1: Choose a Coordinate System

• • Place the origin strategically (often at a vertex or center)
• • Align axes with sides or symmetry lines
• • Use general coordinates (a, b) not specific numbers for generality

Strategic Placement Guidelines

Example for triangle ABC:

A = (0, 0)
B = (c, 0)      -- on x-axis, distance c from origin
C = (a, b)      -- general point

Step 2: Assign Coordinates

• • Label all vertices with coordinates
• • Use symmetry to simplify when possible
• • Keep coordinates general (parameters) for general proofs
• • For special triangles (isoceles, right), use appropriate constraints

Common Setups

Isoceles triangle (symmetric about y-axis):

A = (-a, 0), B = (a, 0), C = (0, h)

Right triangle (right angle at origin):

A = (0, 0), B = (a, 0), C = (0, b)

Parallelogram:

A = (0, 0), B = (a, 0), C = (a+b, c), D = (b, c)

Step 3: Compute Algebraically

Use these fundamental formulas:

Distance Formula

d(P₁, P₂) = √[(x₂-x₁)² + (y₂-y₁)²]

Midpoint Formula

M = ((x₁+x₂)/2, (y₁+y₂)/2)

Slope Formula

m = (y₂-y₁)/(x₂-x₁)

Key Relationships

Step 4: Derive the Result

• • Substitute coordinates into formulas
• • Simplify algebraic expressions
• • Verify the required relationship holds
• • Use symbolic_compute for complex calculations

Tools to use:

• •symbolic_compute: Simplify algebraic expressions
• •lean_prover: Verify formal proof in Lean

Step 5: Lean Formalization

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

-- Distance in ℝ²
def dist2 (p q : ℝ × ℝ) : ℝ :=
  Real.sqrt ((q.1 - p.1)^2 + (q.2 - p.2)^2)

-- Midpoint
def midpoint2 (p q : ℝ × ℝ) : ℝ × ℝ :=
  ((p.1 + q.1)/2, (p.2 + q.2)/2)

-- Slope (when x₁ ≠ x₂)
def slope (p q : ℝ × ℝ) : ℝ :=
  (q.2 - p.2) / (q.1 - p.1)

-- Example: Midpoint of hypotenuse equidistant from all vertices
theorem midpoint_equidistant (a b : ℝ) (ha : a > 0) (hb : b > 0) :
    let A : ℝ × ℝ := (0, 0)
    let B : ℝ × ℝ := (a, 0)
    let C : ℝ × ℝ := (0, b)
    let M := midpoint2 B C
    dist2 M A = dist2 M B ∧ dist2 M B = dist2 M C := by
  sorry -- Proof by computation

Example: Prove Diagonals of Rectangle Bisect Each Other

Problem: Show that the diagonals of a rectangle bisect each other.

Setup:

A = (0, 0)
B = (a, 0)
C = (a, b)
D = (0, b)

Proof: Diagonal AC: from (0,0) to (a,b) Midpoint of AC = ((0+a)/2, (0+b)/2) = (a/2, b/2)

Diagonal BD: from (a,0) to (0,b) Midpoint of BD = ((a+0)/2, (0+b)/2) = (a/2, b/2)

Both diagonals have the same midpoint (a/2, b/2), so they bisect each other.

Output Format

**Theorem:** [Geometric statement]

**Coordinate Setup:**
[Coordinate assignments with justification]

**Computation:**
[Step-by-step algebraic work]

**Conclusion:**
[How computation proves the theorem]

**Lean Proof:**
[Formal verification]

Common Pitfalls

1. •Overly specific coordinates: Using (3, 4) instead of (a, b) proves only one case
2. •Loss of generality: Placing a general triangle with one vertex at (0, 0) is fine; forcing two vertices on axes over-constrains
3. •Division by zero: Check for vertical lines (undefined slope) separately
4. •Forgetting constraints: If proving for rectangles, coordinates must satisfy perpendicularity

Advanced Techniques

Vector Form

For some proofs, vectors are cleaner:

• •Position vector: r = (x, y)
• •Displacement: AB = B - A
• •Dot product: u · v = 0 ⟺ perpendicular

Parametric Lines

Line through P in direction d:

(x, y) = P + t·d = (p₁ + t·d₁, p₂ + t·d₂)