Rational Points

This file defines rational points in the plane and basic geometric operations on them.

@[reducible, inline]

abbrev RationalPoint : Type

A point in the plane with rational coordinates

Equations

• RationalPoint = (Fin 2 → ℚ)

def RationalPoint.distSq (p q : RationalPoint) : ℚ

Squared distance between two points (avoids square roots)

Equations

• p.distSq q = (p 0 - q 0) * (p 0 - q 0) + (p 1 - q 1) * (p 1 - q 1)

def RationalPoint.crossProduct (u v : RationalPoint) : ℚ

Cross product of two 2D vectors (returns scalar)

Equations

• u.crossProduct v = u 0 * v 1 - u 1 * v 0

def RationalPoint.dotProduct (u v : RationalPoint) : ℚ

Dot product of two 2D vectors

Equations

• u.dotProduct v = u 0 * v 0 + u 1 * v 1

def RationalPoint.lengthSq (v : RationalPoint) : ℚ

Euclidean length squared of a vector

Equations

• v.lengthSq = v 0 * v 0 + v 1 * v 1

theorem RationalPoint.lengthSq_nonneg (v : RationalPoint) : 0 ≤ v.lengthSq

def RationalPoint.isStrictlyLeftOf (p p1 p2 : RationalPoint) : Bool

Check if a point is strictly to the left of the directed line from p1 to p2. Uses the cross product: positive means left, negative means right, zero means collinear.

Equations

• p.isStrictlyLeftOf p1 p2 = decide ((p2 - p1).crossProduct (p - p1) > 0)

def RationalPoint.ccw (p1 p2 p3 : RationalPoint) : Bool

Check if three points are in counterclockwise order

Equations

• p1.ccw p2 p3 = p3.isStrictlyLeftOf p1 p2

def RationalPoint.rotate90Counterclockwise (p : RationalPoint) : RationalPoint

Rotate a rational point by 90° counterclockwise about the origin.

Equations

• p.rotate90Counterclockwise = ![-p 1, p 0]

theorem RationalPoint.lengthSq_rotate90Counterclockwise (v : RationalPoint) : v.rotate90Counterclockwise.lengthSq = v.lengthSq

theorem RationalPoint.lengthSq_pos_of_ne (v : RationalPoint) (hv : v ≠ 0) : 0 < v.lengthSq