Affine

Geometry and verified arithmetic for the Conway–Soifer covering theorem at n = 3.

def ConwaySoifer.EquilateralTriangle.mapAffineIso (T : EquilateralTriangle) (f : Point →ᵃ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) : EquilateralTriangle

Transport a filled equilateral triangle by an affine distance-preserving map.

Equations

• T.mapAffineIso f hf = { vertices := fun (i : Fin 3) => f (T.vertices i), side := T.side, side_nonneg := ⋯, equilateral := ⋯ }

theorem ConwaySoifer.EquilateralTriangle.carrier_mapAffineIso (T : EquilateralTriangle) (f : Point →ᵃ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) : (T.mapAffineIso f hf).carrier = ⇑f '' T.carrier

theorem ConwaySoifer.EquilateralTriangle.mem_mapAffineIso (T : EquilateralTriangle) (f : Point →ᵃ[ℝ] Point) (hf : ∀ (p q : Point), sqDist (f p) (f q) = sqDist p q) {p : Point} (hp : p ∈ T.carrier) : f p ∈ (T.mapAffineIso f hf).carrier

def ConwaySoifer.Simplified.receiverLinear : Point →ₗ[ℝ] Point

The linear part of the side-owner receiver coordinate change.

Equations

• ConwaySoifer.Simplified.receiverLinear = { toFun := fun (p : ConwaySoifer.Point) => (-p.1, p.1 + p.2), map_add' := ⋯, map_smul' := ⋯ }

def ConwaySoifer.Simplified.receiverCoordinates (s : ℝ) : Point →ᵃ[ℝ] Point

The affine coordinates at the minimal side-owner receiver.

Equations

• ConwaySoifer.Simplified.receiverCoordinates s = ConwaySoifer.Simplified.receiverLinear.toAffineMap + AffineMap.const ℝ ConwaySoifer.Point (1, s - 1)

theorem ConwaySoifer.Simplified.receiverCoordinates_apply (s : ℝ) (p : Point) : (receiverCoordinates s) p = (1 - p.1, p.1 + p.2 + s - 1)

theorem ConwaySoifer.Simplified.receiverCoordinates_isometry (s : ℝ) (p q : Point) : sqDist ((receiverCoordinates s) p) ((receiverCoordinates s) q) = sqDist p q