Midpoint

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

def ConwaySoifer.Simplified.cornerCoordinates : Point →ᵃ[ℝ] Point

The affine local coordinate system at the first target corner.

Equations

• ConwaySoifer.Simplified.cornerCoordinates = (-ConwaySoifer.reflL).toAffineMap + AffineMap.const ℝ ConwaySoifer.Point (1, 1)

theorem ConwaySoifer.Simplified.cornerCoordinates_apply (p : Point) : cornerCoordinates p = (1 - p.2, 1 - p.1)

theorem ConwaySoifer.Simplified.cornerCoordinates_isometry (p q : Point) : sqDist (cornerCoordinates p) (cornerCoordinates q) = sqDist p q

theorem ConwaySoifer.Simplified.midpoint_exclusion {u : ℝ} (hu0 : 0 < u) (hu : u ≤ 1 / 2) {Q : EquilateralTriangle} (hQ : 0 < Q.side) (hQ1 : Q.side < 1) (hw : corner 0 ∈ Q.carrier) (hs : linePoint (corner 0) (cornerDirection 0 1) u ∈ Q.carrier) (hp : linePoint (vertex 0) (sideDirection 0 true) u ∈ Q.carrier) (hm : extMid0 ∈ Q.carrier) : False

The forbidden midpoint used in canonical normalization, now by geometry.

theorem ConwaySoifer.Simplified.half_midpoints_base {Q : EquilateralTriangle} {u : ℝ} (hQ : 0 < Q.side) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (h0 : (0, 0) ∈ Q.carrier) (he : (1 / 2, 0) ∈ Q.carrier) (hf : (0, 1 / 2) ∈ Q.carrier) (hp : (1 - u, u) ∈ Q.carrier) : 1 ≤ Q.side

A triangle containing a corner and both half-edge points misses the base.