Isometry Discretization

This file discretizes the space of direct planar isometries for computational purposes.

We might assume that the isometries act on worms containing the origin.

def Moser.piApprox : ℚ

Rational approximation of π (355/113 is accurate to 6 decimal places)

Equations

• Moser.piApprox = 355 / 113

def Moser.sinApprox (angle : ℚ) : ℚ

Rational approximation of sin using Taylor series (for small angles)

Equations

• Moser.sinApprox angle = angle - angle * angle * angle / 6 + angle * angle * angle * (angle * angle) / 120

def Moser.cosApprox (angle : ℚ) : ℚ

Rational approximation of cos using Taylor series (for small angles)

Equations

• Moser.cosApprox angle = 1 - angle * angle / 2 + angle * angle * (angle * angle) / 24

def Moser.rationalGrid (min max step : ℚ) : List ℚ

Generate a grid of rational numbers in a range with given step size

Equations

• Moser.rationalGrid min max step = List.map (fun (i : ℚ) => min + step * i) do let a ← List.range ((max - min) / step).ceil.toNat pure ↑a

def Moser.angleGridAux (n : ℕ) : List (ℚ × ℚ)

Helper: generate angle pairs without deduplication

Equations

• One or more equations did not get rendered due to their size.

def Moser.angleGrid (max_angle_change : ℚ) : List (ℚ × ℚ)

Generate rational points on the unit circle, so that the maximum difference in angle between adjacent points is no more than max_angle_change.

Note: Implementation using the complex squaring trick. For (a, b) we compute (a + bi)² = (a² - b²) + 2abi, then normalize to get:

• cos = (a² - b²) / (a² + b²)
• sin = 2ab / (a² + b²) This gives exact rational (cos, sin) pairs satisfying cos² + sin² = 1.

TODO: Optimize by removing points that are too close together to be unnecessary per the spec.

Equations

• Moser.angleGrid max_angle_change = (Moser.angleGridAux (max 1 (4 / max_angle_change).ceil.toNat)).dedup

theorem Moser.unit_circle_from_complex_square (a b : ℚ) (h : a * a + b * b ≠ 0) : have c := (a * a - b * b) / (a * a + b * b); have s := 2 * a * b / (a * a + b * b); c * c + s * s = 1

The core algebraic identity: for any a, b with a² + b² ≠ 0, the normalized squared complex number lies on the unit circle.

theorem Moser.angleGridAux_spec (n : ℕ) (p : ℚ × ℚ) (hp : p ∈ angleGridAux n) : p.1 * p.1 + p.2 * p.2 = 1

All elements of angleGridAux satisfy the unit circle equation.

theorem Moser.angleGrid_spec (step : ℚ) (p : ℚ × ℚ) (hp : p ∈ angleGrid step) : p.1 * p.1 + p.2 * p.2 = 1

All elements of angleGrid satisfy the unit circle equation.

def Moser.discretizeIsometries (epsilon : ℚ) : List DirectIsometry

Discretize the space of planar isometries with given granularity TODO fold into the worm manipulations and optimize more finely.

Equations

• One or more equations did not get rendered due to their size.

def Moser.defaultDiscretization : List DirectIsometry

Discretize with a default epsilon

Equations

• Moser.defaultDiscretization = Moser.discretizeIsometries (1 / 10)