The coordinate plane · The Lumenary

Lens

MotivationH

Where exactly?

“The treasure is buried somewhere in the field” is not much help. “Walk 30 paces east from the old baobab tree, then 20 paces north” is. Two numbers, measured from an agreed starting point in two agreed directions, pin down a place exactly.

People use this idea everywhere. A chess move is written as a letter and a number, such as e4. A seat in a cinema has a row and a number. A ship's position is given by latitude and longitude: Quito lies almost exactly on the equator, at latitude $0^\circ$ . Many cities, from La Plata in Argentina to Chandigarh in India, are laid out in grids of streets, so a delivery rider thinks in “blocks east” and “blocks north”.

Mathematics takes this everyday idea and makes it precise. The result, the coordinate plane, lets us draw numbers and calculate with pictures. It is one of the most useful inventions in the whole of mathematics.

IntuitionH

Two number lines at right angles

Take a number line and lay it horizontally: this is the $x$ -axis. Take a second number line and stand it up vertically, crossing the first at $0$ : this is the $y$ -axis. The crossing point is the origin. Every point of the plane can now be reached from the origin by moving some distance left or right (along the $x$ -axis) and then some distance up or down (parallel to the $y$ -axis).

The coordinate plane. The axes divide it into four quadrants, numbered I to IV anticlockwise from the top right. Order matters: A = (3, 2) and B = (2, 3) are different points. Coordinates can be fractions or negative: D = (−2.5, −3).

To reach A, start at the origin, go 3 to the right, then 2 up. To reach B, go 2 to the right, then 3 up. Same two numbers, different order, different place.

DefinitionsH

Definitions

Definition— coordinate plane

The coordinate plane is formed by two perpendicular number lines, the $x$ -axis (horizontal) and the $y$ -axis (vertical), which meet at their zeros. The meeting point is the origin, $O = (0, 0)$ .

Definition— coordinates

The coordinates $(a, b)$ of a point $P$ are its signed horizontal and vertical positions relative to the origin: $a$ is the $x$ -coordinate (positive to the right, negative to the left) and $b$ is the $y$ -coordinate (positive up, negative down). An ordered pair is a pair of numbers in which the order matters: $(a, b) = (c, d)$ exactly when $a = c$ and $b = d$ .

Definition— quadrants

The axes split the rest of the plane into four quadrants: I where $x > 0$ and $y > 0$ ; II where $x \lt 0$ and $y > 0$ ; III where $x \lt 0$ and $y \lt 0$ ; IV where $x > 0$ and $y \lt 0$ . Points on an axis are in no quadrant.

Definition— absolute value

The absolute value $|a|$ is the distance of $a$ from $0$ on the number line: $|a| = a$ if $a \ge 0$ , and $|a| = -a$ if $a \lt 0$ . So $|5| = 5$ , $|-5| = 5$ and $|0| = 0$ .

Definition— reflection in an axis

The reflection of a point $P$ in a line $\ell$ is the point $P'$ on the other side of $\ell$ such that $\ell$ crosses the segment $PP'$ at right angles, exactly halfway. A point on $\ell$ is its own reflection.

Worked examplesH

Worked examples

Example— Plotting with negative numbers and fractions

To plot $D = (-2.5, -3)$ : from the origin go $2.5$ units left (the $x$ -coordinate is negative), then $3$ units down. $D$ is in quadrant III. The point $(\tfrac{3}{4}, -6)$ is in quadrant IV, and $(0, -2)$ lies on the $y$ -axis, in no quadrant.

Example— Reading a distance along a horizontal line

How far is $(-3, 2)$ from $(4, 2)$ ? Both points are 2 units up, so the segment joining them is horizontal. From $x = -3$ to $x = 0$ is 3 units; from $0$ to $4$ is 4 more. The distance is $7 = |-3 - 4| = |4 - (-3)|$ . It is not $4 - 3 = 1$ : the points are on opposite sides of the $y$ -axis.

Example— A vertical distance

From $(1, -4)$ to $(1, 3)$ the segment is vertical, and its length is $|-4 - 3| = 7$ .

Example— Distance along the grid

A delivery rider in a city of square blocks travels from $(-3, 2)$ to $(4, -1)$ along the streets. She must go $|-3 - 4| = 7$ blocks east and $|2 - (-1)| = 3$ blocks south: $10$ blocks, whichever route she picks (as long as she never doubles back). This grid distance $|a - c| + |b - d|$ is also called the taxicab distance.

Example— Reflections

Reflect $A = (3, 2)$ in the $x$ -axis: it lands at $(3, -2)$ , 2 units below the axis. Reflect it in the $y$ -axis: $(-3, 2)$ . Reflect it in both: $(-3, -2)$ , the same as turning $A$ half way round the origin.

Example— Plotting a relationship

A kettle's water starts at $20\,^\circ\mathrm{C}$ and warms by $15$ degrees each minute. Plotting (minutes, temperature) gives $(0, 20)$ , $(1, 35)$ , $(2, 50)$ , $(3, 65)$ , $(4, 80)$ : the points lie on a straight line. Turning a table into points in the plane makes patterns visible — the starting point for linear relationships.

ProofH

Why it all works

Theorem— Theorem 1 (one point, one ordered pair)

Every point of the plane has exactly one pair of coordinates, and every ordered pair of numbers $(a, b)$ is the address of exactly one point. Two points are the same exactly when their $x$ -coordinates are equal and their $y$ -coordinates are equal.

Proof

Given a point $P$ , draw the line through $P$ parallel to the $y$ -axis. It crosses the $x$ -axis at exactly one point, which is some number $a$ on that number line. Likewise the line through $P$ parallel to the $x$ -axis crosses the $y$ -axis at exactly one number $b$ . So $P$ has the coordinates $(a, b)$ , and no others.

Conversely, given $(a, b)$ , the vertical line through $a$ and the horizontal line through $b$ are perpendicular, so they cross at exactly one point. That point has coordinates $(a, b)$ .

So points and ordered pairs match up one-to-one, and two points are equal exactly when their pairs are equal, that is, when both coordinates agree.

∎

In particular $(3, 2) \neq (2, 3)$ : their $x$ -coordinates differ.

Theorem— Theorem 2 (distance along a line)

The distance between $(a, b)$ and $(c, b)$ is $|a - c|$ . The distance between $(a, b)$ and $(a, d)$ is $|b - d|$ . Also $|a - c| = |c - a|$ .

Proof

The points $(a, b)$ and $(c, b)$ lie on the horizontal line at height $b$ , which is a copy of the $x$ -axis number line. On a number line the distance between $a$ and $c$ is the larger minus the smaller. If $a \ge c$ that is $a - c$ , which equals $|a - c|$ because $a - c \ge 0$ . If $a \lt c$ it is $c - a = -(a - c)$ , which equals $|a - c|$ because $a - c \lt 0$ . Either way the distance is $|a - c|$ ; and because the distance does not depend on which point we call first, $|a - c| = |c - a|$ . The vertical case is the same, using the $y$ -coordinates.

∎

Theorem— Theorem 3 (reflections in the axes)

Reflecting $(a, b)$ in the $x$ -axis gives $(a, -b)$ ; reflecting it in the $y$ -axis gives $(-a, b)$ . Reflecting twice in the same axis brings every point back, and reflecting in both axes, in either order, gives $(-a, -b)$ .

Proof

Let $P = (a, b)$ . The line through $P$ perpendicular to the $x$ -axis is the vertical line at $a$ , so the reflection $P'$ also has $x$ -coordinate $a$ . The $x$ -axis must cross $PP'$ halfway, so $P'$ is as far below the axis as $P$ is above it (or vice versa): its $y$ -coordinate is $-b$ . (If $b = 0$ , then $P$ is on the axis and $P' = P = (a, -0)$ .) The $y$ -axis case is the same with the roles of the coordinates swapped.

Reflecting $(a, -b)$ in the $x$ -axis gives $(a, -(-b)) = (a, b)$ , the starting point. Reflecting in the $y$ -axis and then the $x$ -axis gives $(-a, b) \mapsto (-a, -b)$ ; the other order gives $(a, -b) \mapsto (-a, -b)$ . The same point.

∎

Theorem— Theorem 4 (reflections and quadrants)

Reflection in the $x$ -axis swaps quadrants I and IV, and II and III. Reflection in the $y$ -axis swaps I and II, and III and IV. The points that reflection in the $x$ -axis leaves where they are are exactly the points of the $x$ -axis.

Proof

Reflection in the $x$ -axis keeps the sign of the $x$ -coordinate and reverses the sign of the $y$ -coordinate. Quadrants I and IV are exactly the two quadrants with $x > 0$ , differing only in the sign of $y$ ; so are II and III with $x \lt 0$ . For the last claim: $(a, -b) = (a, b)$ exactly when $-b = b$ , that is $2b = 0$ , that is $b = 0$ . The $y$ -axis case is the same with the coordinates swapped.

∎

Theorem— Theorem 5 (reflections keep distances)

Reflecting two points in an axis does not change the horizontal distance, the vertical distance, or the grid distance between them.

Proof

Reflect $(a, b)$ and $(c, d)$ in the $x$ -axis. The horizontal distance is still $|a - c|$ . The vertical distance becomes $|(-b) - (-d)| = |d - b| = |b - d|$ by Theorem 2. So the grid distance $|a - c| + |b - d|$ is unchanged too. The $y$ -axis is similar.

∎

ExplanationH

Taxicab geometry: a different distance

In a city of square blocks, the grid distance $|a - c| + |b - d|$ is the distance that matters to a taxi driver: you cannot drive through buildings. It obeys the same basic rule as ordinary distance, the triangle inequality: going from $P$ to $R$ by way of a third point $Q$ is never shorter than going directly.

Theorem— Theorem 6 (triangle inequality for grid distance)

For any points $P$ , $Q$ , $R$ : $\;\text{grid}(P, R) \le \text{grid}(P, Q) + \text{grid}(Q, R)$ .

Proof

On a number line, $|u + v| \le |u| + |v|$ for all numbers $u$ and $v$ : if $u$ and $v$ have the same sign, both sides are equal; if they have opposite signs, they partly cancel on the left. Apply this with $u = a - e$ and $v = e - c$ for the $x$ -coordinates $a, e, c$ of $P, Q, R$ : $|a - c| \le |a - e| + |e - c|$ . Do the same for the $y$ -coordinates and add the two inequalities.

∎

Taxicab geometry has surprises. The set of points at grid distance $3$ from the origin — a taxicab “circle” — is not round at all: it is a square standing on one corner, with corners at $(3, 0)$ , $(0, 3)$ , $(-3, 0)$ and $(0, -3)$ . Ordinary straight-line distance, the kind a bird would fly, needs the Pythagorean theorem, which comes next.

Formal mathematicsF

The coordinate plane in Lean

In Lean a point is a structure holding two rational numbers. Lean then knows that a point is nothing more and nothing less than its two coordinates — and we prove it:

PointLean 4Formally verified

/-- A point of the coordinate plane: its `x`-coordinate (horizontal position) and its
`y`-coordinate (vertical position), measured from the origin `⟨0, 0⟩`. -/
structure Point where
  x : Rat
  y : Rat
deriving DecidableEq

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

point_eq_iffLean 4Proved here from basic factsFormally verified

/-- **One point, one ordered pair.** Two points are the same exactly when their
`x`-coordinates agree **and** their `y`-coordinates agree. -/
theorem point_eq_iff (P Q : Point) : P = Q ↔ P.x = Q.x ∧ P.y = Q.y := by
  constructor
  · intro h
    rw [h]
    exact ⟨rfl, rfl⟩
  · intro ⟨hx, hy⟩
    cases P
    cases Q
    simp only at hx hy
    rw [hx, hy]

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

order_mattersLean 4Proved here from basic factsFormally verified

/-- The order of the coordinates matters: `(3, 2)` and `(2, 3)` are different points. -/
theorem order_matters : (⟨3, 2⟩ : Point) ≠ ⟨2, 3⟩ := by decide +kernel

Axioms used: propext, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

Quadrants, with a point that has a fraction coordinate:

quadrantLean 4Formally verified

/-- The quadrant of a point: 1 (`x > 0, y > 0`), 2 (`x < 0, y > 0`), 3 (`x < 0, y < 0`),
4 (`x > 0, y < 0`), and `0` for points on an axis, which lie in no quadrant. -/
def quadrant (P : Point) : Nat :=
  if 0 < P.x ∧ 0 < P.y then 1
  else if P.x < 0 ∧ 0 < P.y then 2
  else if P.x < 0 ∧ P.y < 0 then 3
  else if 0 < P.x ∧ P.y < 0 then 4
  else 0

Axioms used: propext, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

example_quadrantLean 4Proved here from basic factsFormally verified

/-- The point `(-1/2, 3)` lies in the second quadrant, and `(0, -2)` on an axis. -/
theorem example_quadrant : quadrant ⟨-1/2, 3⟩ = 2 ∧ quadrant ⟨0, -2⟩ = 0 := by decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

Reflections, and Theorems 3 and 4:

reflectXLean 4Formally verified

/-- Reflection in the `x`-axis: `(a, b) ↦ (a, -b)`. -/
def reflectX (P : Point) : Point := ⟨P.x, -P.y⟩

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflectYLean 4Formally verified

/-- Reflection in the `y`-axis: `(a, b) ↦ (-a, b)`. -/
def reflectY (P : Point) : Point := ⟨-P.x, P.y⟩

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

example_reflectionsLean 4Proved here from basic factsFormally verified

/-- Reflecting `(3, 2)` in the `x`-axis gives `(3, -2)`; in the `y`-axis, `(-3, 2)`. -/
theorem example_reflections : reflectX ⟨3, 2⟩ = ⟨3, -2⟩ ∧ reflectY ⟨3, 2⟩ = ⟨-3, 2⟩ := by
  decide +kernel

Axioms used: propext, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflectX_twiceLean 4Proved here from basic factsFormally verified

/-- Reflecting twice in the same axis brings every point back: `-(-b) = b`. -/
theorem reflectX_twice (P : Point) : reflectX (reflectX P) = P := by
  rw [point_eq_iff]
  exact ⟨rfl, Rat.neg_neg P.y⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflectY_twiceLean 4Proved here from basic factsFormally verified

/-- Reflecting twice in the `y`-axis brings every point back. -/
theorem reflectY_twice (P : Point) : reflectY (reflectY P) = P := by
  rw [point_eq_iff]
  exact ⟨Rat.neg_neg P.x, rfl⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflectX_reflectYLean 4Proved here from basic factsFormally verified

/-- Reflecting in the `y`-axis and then in the `x`-axis sends `(a, b)` to `(-a, -b)`: a half
turn about the origin. -/
theorem reflectX_reflectY (P : Point) : reflectX (reflectY P) = ⟨-P.x, -P.y⟩ := rfl

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflections_commuteLean 4Proved here from basic factsFormally verified

/-- The two reflections can be done in either order: both orders give `(-a, -b)`. -/
theorem reflections_commute (P : Point) : reflectX (reflectY P) = reflectY (reflectX P) := rfl

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

reflectX_fixed_iffLean 4Proved here from basic factsFormally verified

/-- The points that reflection in the `x`-axis leaves where they are are exactly the points
**on** the `x`-axis: `(a, -b) = (a, b)` exactly when `b = 0`. -/
theorem reflectX_fixed_iff (P : Point) : reflectX P = P ↔ P.y = 0 := by
  rw [point_eq_iff]
  constructor
  · intro ⟨_, h⟩
    -- `h` says `-b = b`, which forces `b = 0`.
    simp only [reflectX] at h
    grind
  · intro h
    exact ⟨rfl, by simp only [reflectX]; rw [h]; rfl⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

mirrorQuadrantLean 4Formally verified

/-- How reflection in the `x`-axis relabels quadrants: `1 ↔ 4` and `2 ↔ 3` (and the axes,
labelled `0`, stay on the axes). -/
def mirrorQuadrant : Nat → Nat
  | 1 => 4
  | 2 => 3
  | 3 => 2
  | 4 => 1
  | _ => 0

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

quadrant_reflectXLean 4Proved here from basic factsFormally verified

/-- **Reflection in the `x`-axis swaps quadrants 1 and 4, and 2 and 3.** The sign of `x` is
kept and the sign of `y` is reversed. Proof: try every combination of signs. -/
theorem quadrant_reflectX (P : Point) : quadrant (reflectX P) = mirrorQuadrant (quadrant P) := by
  unfold quadrant reflectX
  simp only
  by_cases h1 : 0 < P.x <;> by_cases h2 : 0 < P.y <;> by_cases h3 : P.x < 0 <;>
    by_cases h4 : P.y < 0 <;> simp_all [mirrorQuadrant] <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

Distances: absolute value, Theorem 2, the example that crosses an axis, the grid distance, Theorems 5 and 6, and the count of grid lines.

absQLean 4Formally verified

/-- Absolute value: the distance of a number from `0` on the number line. -/
def absQ (q : Rat) : Rat := if 0 ≤ q then q else -q

Axioms used: propext, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

abs_sub_commLean 4Proved here from basic factsFormally verified

/-- The distance between `a` and `c` on a number line does not depend on the order:
`|a - c| = |c - a|`. -/
theorem abs_sub_comm (a c : Rat) : absQ (a - c) = absQ (c - a) := by
  unfold absQ
  split <;> split <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

horizontal_distance_exampleLean 4Proved here from basic factsFormally verified

/-- From `(-3, 2)` to `(4, 2)` is `|-3 - 4| = 7` units — **not** `4 - 3 = 1`: the path
crosses the `y`-axis, 3 units on one side and 4 on the other. -/
theorem horizontal_distance_example : absQ (-3 - 4) = 7 := by decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

gridDistLean 4Formally verified

/-- The distance between two points when you may only travel along grid lines (horizontal
and vertical steps, like a taxi in a city of square blocks): `|a - c| + |b - d|`. -/
def gridDist (P Q : Point) : Rat := absQ (P.x - Q.x) + absQ (P.y - Q.y)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

gridDist_horizontalLean 4Proved here from basic factsFormally verified

/-- For two points on the same horizontal line, `(a, b)` and `(c, b)`, the distance is
`|a - c|`. -/
theorem gridDist_horizontal (P Q : Point) (h : P.y = Q.y) :
    gridDist P Q = absQ (P.x - Q.x) := by
  unfold gridDist
  rw [h, Rat.sub_self]
  unfold absQ
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

gridDist_reflectXLean 4Proved here from basic factsFormally verified

/-- **Reflections keep distances.** Reflecting two points in the `x`-axis does not change the
grid distance between them, because `|(-b) - (-d)| = |d - b| = |b - d|`. -/
theorem gridDist_reflectX (P Q : Point) : gridDist (reflectX P) (reflectX Q) = gridDist P Q := by
  unfold gridDist reflectX
  simp only
  rw [show -P.y - -Q.y = Q.y - P.y by grind, abs_sub_comm Q.y P.y]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

abs_add_leLean 4Proved here from basic factsFormally verified

/-- The triangle inequality on the number line: `|a + b| ≤ |a| + |b|`. Proof: check every
combination of signs of `a`, `b` and `a + b`. -/
theorem abs_add_le (a b : Rat) : absQ (a + b) ≤ absQ a + absQ b := by
  unfold absQ
  split <;> split <;> split <;> grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

gridDist_triangleLean 4Proved here from basic factsFormally verified

/-- **A detour never helps:** going from `P` to `R` along grid lines is never longer than going
from `P` to `Q` and then from `Q` to `R`. Apply `abs_add_le` to the horizontal and the vertical
parts separately. -/
theorem gridDist_triangle (P Q R : Point) : gridDist P R ≤ gridDist P Q + gridDist Q R := by
  unfold gridDist
  have h1 := abs_add_le (P.x - Q.x) (Q.x - R.x)
  have h2 := abs_add_le (P.y - Q.y) (Q.y - R.y)
  rw [show P.x - Q.x + (Q.x - R.x) = P.x - R.x by grind] at h1
  rw [show P.y - Q.y + (Q.y - R.y) = P.y - R.y by grind] at h2
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

grid_lines_vs_stepsLean 4Applies a library theoremFormally verified

/-- **Count the gaps, not the lines.** Walking `n` unit steps from `a` passes the `n + 1` grid
lines `a, a + 1, …, a + n`: one more line than the distance. This applies core Lean's
`List.length_range'`. -/
theorem grid_lines_vs_steps (a n : Nat) : (List.range' a (n + 1)).length = n + 1 :=
  List.length_range'

Axioms used: No axiomsformal/Lumenary/CoordinatePlane.leanTry it in the Lean web editor

Everything except the last is proved here from the rules of arithmetic for rational numbers; the last applies a library fact about lists. What is not formalised: the geometric half of Theorem 1 (that perpendicular lines through the axes meet in exactly one point). In Lean we define a point to be a pair of numbers, which builds Theorem 1 in from the start; that is exactly how coordinate geometry turns pictures into algebra. Mathlib works with the real plane ℝ × ℝ, where |x| is abs x.

ComputationC

Checking every point of a grid

Reflections and grid distances, point by pointPythonExact computationExhaustive finite checkComputationally tested

"""Reflections and grid distances on every point of a small grid.

The experiment takes all 121 points (a, b) with whole-number coordinates from
-5 to 5, plus a few points with fraction coordinates, and checks: reflecting
twice returns each point; reflection in the x-axis swaps quadrants 1 and 4 and
2 and 3; the points it leaves fixed are exactly those on the x-axis; and the
reflections, the half turn and the coordinate swap (a, b) -> (b, a) keep the
grid ("taxicab") distance |a - c| + |b - d| between every pair of points. It
also counts grid lines against unit steps. Exact arithmetic over a finite
grid: exhaustive evidence for these points, not a proof for all points.
"""

from fractions import Fraction
from itertools import product

def reflect_x(p):
    """Reflection in the x-axis: (a, b) -> (a, -b)."""
    return (p[0], -p[1])

def reflect_y(p):
    """Reflection in the y-axis: (a, b) -> (-a, b)."""
    return (-p[0], p[1])

def half_turn(p):
    """Half turn about the origin: (a, b) -> (-a, -b)."""
    return (-p[0], -p[1])

def swap(p):
    """Swap the coordinates: (a, b) -> (b, a), reflection in y = x."""
    return (p[1], p[0])

def stretch_x(p):
    """A non-example: stretch horizontally, (a, b) -> (2a, b)."""
    return (2 * p[0], p[1])

def quadrant(p):
    """1, 2, 3 or 4, or 0 for a point on an axis."""
    a, b = p
    if a > 0 and b > 0:
        return 1
    if a < 0 < b:
        return 2
    if a < 0 and b < 0:
        return 3
    if a > 0 > b:
        return 4
    return 0

def grid_distance(p, q):
    """Distance along grid lines: |a - c| + |b - d|."""
    return abs(p[0] - q[0]) + abs(p[1] - q[1])

def grid_points(radius):
    """All points with whole-number coordinates from -radius to radius."""
    r = range(-radius, radius + 1)
    return [(a, b) for a, b in product(r, r)]

def keeps_distance(move, points):
    """Number of pairs (p, q) whose grid distance changes under ``move``."""
    return sum(grid_distance(move(p), move(q)) != grid_distance(p, q)
               for p in points for q in points)

def lines_and_steps(a, c):
    """(unit steps, grid lines crossed) walking from a to c on a number line."""
    lo, hi = min(a, c), max(a, c)
    return hi - lo, len(range(lo, hi + 1))

def main():
    pts = grid_points(5)
    fracs = [(Fraction(1, 2), Fraction(-7, 3)), (Fraction(-5, 4), Fraction(2))]
    every = pts + fracs
    print(f"Points checked: {len(pts)} whole-number points and {len(fracs)} "
          "fraction points")
    twice = all(reflect_x(reflect_x(p)) == p and reflect_y(reflect_y(p)) == p
                for p in every)
    print(f"Reflecting twice returns every point: {twice}")
    moves = {}
    for p in every:
        key = (quadrant(p), quadrant(reflect_x(p)))
        moves[key] = moves.get(key, 0) + 1
    print("Quadrant before -> after reflecting in the x-axis (number of points):")
    print("  " + ", ".join(f"{a}->{b}: {n}" for (a, b), n in sorted(moves.items())))
    fixed = [p for p in pts if reflect_x(p) == p]
    print(f"Points fixed by the x-axis reflection: {len(fixed)}, all with y = 0:"
          f" {all(b == 0 for _, b in fixed)}")
    same = [p for p in pts if swap(p) == p]
    print(f"Points with (a, b) = (b, a): {len(same)}, all on the line y = x")
    print()
    print(f"Grid distance changes among all {len(pts) ** 2} pairs of points:")
    for name, move in [("reflect in x-axis", reflect_x),
                       ("reflect in y-axis", reflect_y),
                       ("half turn", half_turn), ("swap (a, b)", swap)]:
        print(f"  {name:<18} {keeps_distance(move, pts)} pairs changed")
    print(f"  {'stretch x by 2':<18} {keeps_distance(stretch_x, pts)} pairs"
          " changed (a non-example)")
    print()
    steps, lines = lines_and_steps(-3, 4)
    print(f"From x = -3 to x = 4: {steps} unit steps, but {lines} grid lines.")
    print()
    print("Epistemic status: exact, exhaustive checks on the points listed. They")
    print("cannot cover every point of the plane; the lesson's proofs (and the")
    print("Lean proofs) show the same facts for all points with any rational")
    print("coordinates.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Every check passes, and the horizontal stretch $(a, b) \mapsto (2a, b)$ shows that the distance check is not trivially true: a move that is not a rigid motion fails it for most pairs. Still, $121$ points are not the whole plane — the checks are exhaustive only for the points listed. The proofs above, and their Lean versions, cover every point with rational coordinates.

Explore

Explore: reflections in the axes

Move the sliders for $a$ and $b$ to move the point $P = (a, b)$ . $P'$ is its reflection in the $x$ -axis, $P''$ its reflection in the $y$ -axis, and $P'''$ its image under a half turn about the origin. The coloured segments join $P$ to each image.

Things to try: put $P$ in each quadrant in turn and say which quadrants the images land in. Make $b = 0$ : what happens to $P'$ ? Check that each axis cuts the segment joining $P$ to its mirror image exactly in half, at a right angle.

Reflecting a point in the axes

A point moves along the curve as t changes: x and y are both functions of t.

P to P′ (reflect in the x-axis)
P to P″ (reflect in the y-axis)
P to P‴ (half turn)

aa = 3bb = 2

Move along tt = 0.13

(3, 1.5)
(2.25, 2)
(2.25, 1.5)

Exercises

1. The coordinate plane

Warm-upHuman

In which quadrant is the point $(-3, 5)$ ?

Choose one

Quadrant IQuadrant IIQuadrant IIIQuadrant IV

2. The coordinate plane

Warm-upHuman

Reflect the point $(4, -7)$ in the $y$ -axis. Where does it land?

Choose one

(-4, -7)

(4, 7)

(-4, 7)

(-7, 4)

3. The coordinate plane

Warm-upHuman

What is the distance between $(-6, 3)$ and $(5, 3)$ ?

4. The coordinate plane

CoreHuman

A cyclist in a city of square blocks rides from $(-2, -3)$ to $(4, 5)$ along the streets, never doubling back. How many blocks does she ride?

5. The coordinate plane

CoreHuman

A point $P$ is reflected in the $x$ -axis and then the result is reflected in the $y$ -axis. It ends up at $(-2, 5)$ . Where was $P$ ?

Choose one

(2, -5)

(-2, 5)

(2, 5)

(-2, -5)

6. The coordinate plane

Warm-upHuman

Kofi was asked to plot $(3, 2)$ . He started at the origin, went up 3 and then right 2. Which point did he actually plot?

Choose one

(2, 3)

(3, 2)

(-3, 2)

(3, 3)

7. The coordinate plane

CoreHuman

Which point is exactly halfway between $(-3, 2)$ and $(4, 2)$ ?

Choose one

(\tfrac{1}{2}, 2)

(1, 2)

(3\tfrac{1}{2}, 2)

(\tfrac{1}{2}, 0)

8. The coordinate plane

StretchHuman

Which statements are true for every point $(a, b)$ ? (Choose all that apply.)

Choose all that apply

Reflecting in the

x

-axis and then the

y

-axis gives the same point as the other order.Reflection in the

x

-axis keeps the

x

-coordinate.Reflection in the

x

-axis keeps the point in the same quadrant.The distance from

(a, b)

(-a, b)

2|a|

.The distance from

(a, b)

(-a, b)

2a

9. The coordinate plane

CoreFormal

In the Lean file, reflectX P is the reflection of the point P in the $x$ -axis. Which statement says that reflecting twice in the $x$ -axis brings every point back?

Choose one

∀ P : Point, reflectX (reflectX P) = P∀ P : Point, reflectX P = P∀ P : Point, reflectX (reflectY P) = P∃ P : Point, reflectX (reflectX P) = P

10. The coordinate plane

StretchComputational

Write a function quadrant(x, y) that returns 1, 2, 3 or 4 for a point in quadrant I, II, III or IV, and 0 for a point on an axis. It should work for fractions too.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

Swapping the coordinates: plotting $(3, 2)$ at $(2, 3)$ . The first number is always the horizontal ( $x$ ) position, the second the vertical ( $y$ ) position — “along the corridor, then up the stairs”. Swapping them moves the point to its mirror image in the line $y = x$ , which is a different point unless the two coordinates are equal.

Misconception

Counting grid lines instead of unit intervals. From $x = -3$ to $x = 4$ you pass $8$ grid lines ( $-3, -2, \dots, 4$ ) but take only $7$ unit steps. Distance counts the gaps between grid lines, not the lines themselves — like fence panels and fence posts.

Misconception

“The distance from $-3$ to $4$ is $4 - 3 = 1$ .” Ignoring the sign gives the wrong answer when the points lie on opposite sides of an axis. Subtract the coordinates themselves and take the absolute value: $|4 - (-3)| = 7$ .

Misconception

“Reflecting in the $x$ -axis changes the $x$ -coordinate.” It is the other way round: reflecting in the $x$ -axis flips the point across the $x$ -axis, so it changes the sign of $y$ and keeps $x$ . Picture the axis as a mirror lying along the $x$ -direction.

ViewpointsH

Other ways of seeing

Algebra— Points you can add

Once points are pairs of numbers, we can calculate with them. Adding $(a, b) + (c, d) = (a + c, b + d)$ means “do one journey, then the other”; multiplying by a number, $k \cdot (a, b) = (ka, kb)$ , stretches a journey. With these operations the plane becomes the vector space $\R^2$ , and reflections become simple formulas: the reflection in the $x$ -axis is the rule $(a, b) \mapsto (a, -b)$ . This is the doorway to vectors and linear algebra, where whole geometric transformations are written as tables of numbers called matrices.

Geometry— Which distance?

Grid distance and straight-line distance are two different ways to measure the same plane, and they give two different geometries. Reflections in the axes, half turns and swapping the coordinates keep both kinds of distance. But a turn through $45^\circ$ keeps straight-line distance and changes grid distance: the point $(1, 0)$ , at grid distance 1 from the origin, turns into a point at grid distance $\sqrt{2} \approx 1.41$ . Felix Klein's insight (1872) was that a geometry is described by the transformations that keep its measurements — see transformation geometry.

Set-theoretic connectionH

The plane as a set of pairs

For any two sets $A$ and $B$ , the Cartesian product $A \times B$ is the set of all ordered pairs $(a, b)$ with $a \in A$ and $b \in B$ . The coordinate plane is the Cartesian product $\R \times \R = \R^2$ of the real number line with itself, and the grid of points with whole-number coordinates is $\Z \times \Z$ . Theorem 1 says that the points of the geometric plane and the elements of $\R \times \R$ match up exactly. The name “Cartesian” honours Descartes (in Latin, Cartesius). See sets.

Wonder Trails

Optional, and never graded: a question that leads somewhere further.

Wonder Trail · Optional · never gradedLife on a torusIn some video games, walking off the right edge of the screen brings you back on the left, and walking off the top brings you back at the bottom. If that world were a real surface, what shape would it be?Follow the trail

History & global context

History and global context

Maps. Claudius Ptolemy's Geography (Alexandria, 2nd century CE) located about 8000 places by latitude and longitude — two numbers per place. In China, the cartographer Pei Xiu (3rd century CE) is credited with principles of map-making that included a rectangular grid for measuring distances.
Graphs. In the 14th century, Nicole Oresme in France drew pictures of how a quantity, such as speed, changes over time, using horizontal and vertical lengths — an early form of a graph.
Coordinate geometry. In the 1630s René Descartes (La Géométrie, 1637) and Pierre de Fermat (whose Introduction to Plane and Solid Loci circulated in manuscript around the same time) independently showed how to describe curves by equations relating two coordinates, uniting algebra and geometry. Neither used our modern picture with two perpendicular axes and negative coordinates on both; that settled into its familiar form over the following century.
Distances. Around 1900 Hermann Minkowski studied geometries with unusual distances, including the grid distance; the name “taxicab geometry” came later.

Where exactly?

Two number lines at right angles

Definitions

Worked examples

Why it all works

Taxicab geometry: a different distance

The coordinate plane in Lean

Checking every point of a grid

Explore: reflections in the axes

Exercises

Common misconceptions

Other ways of seeing

The plane as a set of pairs

Wonder Trails

History and global context

Further reading