Bridge to the vendored oblique-coordinate library

toOblique (a, b) = (a + b/2, b) is the linear change of coordinates from the triangular coordinates of this project to the oblique coordinates of the vendored SevenTriangles library (pinned commit b17ca52a395519f43fc15f83fb49a5dd69996225). It preserves sqDist, maps the hexagon onto unitHexagon, the six vertices onto the six vertices with the same index, and has determinant one, so it preserves Lebesgue measure. Consequently every nondegenerate triangle of this project is a triangle of the vendored library with the same side, and the 120-degree wedge area-loss lemma transfers verbatim.

noncomputable def ConwaySoifer.ofOblique (p : Point) : Point

The inverse linear coordinate change from oblique to triangular coordinates.

Equations

• ConwaySoifer.ofOblique p = (p.1 - p.2 / 2, p.2)

@[simp]

theorem ConwaySoifer.ofOblique_toOblique (p : Point) : ofOblique (toOblique p) = p

@[simp]

theorem ConwaySoifer.toOblique_ofOblique (p : Point) : toOblique (ofOblique p) = p

theorem ConwaySoifer.toOblique_add (p q : Point) : toOblique (p + q) = toOblique p + toOblique q

theorem ConwaySoifer.toOblique_sub (p q : Point) : toOblique (p - q) = toOblique p - toOblique q

theorem ConwaySoifer.toOblique_smul (t : ℝ) (p : Point) : toOblique (t • p) = t • toOblique p

@[simp]

theorem ConwaySoifer.toOblique_zero : toOblique 0 = 0

noncomputable def ConwaySoifer.obliqueL : Point →ₗ[ℝ] Point

The determinant-one linear coordinate change to the borrowed oblique-coordinate geometry.

Equations

• ConwaySoifer.obliqueL = { toFun := ConwaySoifer.toOblique, map_add' := ConwaySoifer.toOblique_add, map_smul' := ConwaySoifer.toOblique_smul }

@[simp]

theorem ConwaySoifer.obliqueL_apply (p : Point) : obliqueL p = toOblique p

theorem ConwaySoifer.toOblique_injective : Function.Injective toOblique

theorem ConwaySoifer.toOblique_surjective : Function.Surjective toOblique

theorem ConwaySoifer.toOblique_bijective : Function.Bijective toOblique

theorem ConwaySoifer.sqDist_oblique (p q : Point) : SevenTriangles.sqDist (toOblique p) (toOblique q) = sqDist p q

theorem ConwaySoifer.toOblique_vertex (i : Fin 6) : toOblique (vertex i) = SevenTriangles.vertex i

theorem ConwaySoifer.mem_unitHexagon_toOblique (p : Point) : toOblique p ∈ SevenTriangles.unitHexagon ↔ p ∈ hexagon

theorem ConwaySoifer.image_hexagon : toOblique '' hexagon = SevenTriangles.unitHexagon

theorem ConwaySoifer.det_obliqueL : LinearMap.det obliqueL = 1

theorem ConwaySoifer.volume_image_toOblique (s : Set Point) : MeasureTheory.volume (toOblique '' s) = MeasureTheory.volume s

noncomputable def ConwaySoifer.EquilateralTriangle.toST (T : EquilateralTriangle) (hs : 0 < T.side) : SevenTriangles.EquilateralTriangle

A nondegenerate triangle of this project as a triangle of the vendored library.

Equations

• T.toST hs = { vertices := fun (j : Fin 3) => ConwaySoifer.toOblique (T.vertices j), side := T.side, side_pos := hs, equilateral := ⋯ }

theorem ConwaySoifer.EquilateralTriangle.carrier_toST (T : EquilateralTriangle) (hs : 0 < T.side) : (T.toST hs).carrier = toOblique '' T.carrier

theorem ConwaySoifer.EquilateralTriangle.mem_carrier_toST (T : EquilateralTriangle) (hs : 0 < T.side) (p : Point) : toOblique p ∈ (T.toST hs).carrier ↔ p ∈ T.carrier

theorem ConwaySoifer.EquilateralTriangle.volume_diff_toST (T : EquilateralTriangle) (hs : 0 < T.side) : MeasureTheory.volume ((T.toST hs).carrier \ SevenTriangles.unitHexagon) = MeasureTheory.volume (T.carrier \ hexagon)

theorem ConwaySoifer.toOblique_sidePoint (i : Fin 6) (right : Bool) (t : ℝ) : toOblique (linePoint (vertex i) (sideDirection i right) t) = SevenTriangles.vertex i + t • (SevenTriangles.vertex (neighbor i right) - SevenTriangles.vertex i)

theorem ConwaySoifer.neighbor_false (i : Fin 6) : neighbor i false = SevenTriangles.previous i

theorem ConwaySoifer.neighbor_true (i : Fin 6) : neighbor i true = SevenTriangles.next i

theorem ConwaySoifer.wedge_area_weak (i : Fin 6) (T : EquilateralTriangle) (hs : 0 < T.side) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hv : vertex i ∈ T.carrier) (hpa : linePoint (vertex i) (sideDirection i false) a ∈ T.carrier) (hpb : linePoint (vertex i) (sideDirection i true) b ∈ T.carrier) : min (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ hexagon)).toReal

The weak 120-degree wedge area-loss lemma in triangular coordinates: a triangle containing vertex i and the points at ray parameters a (towards vertex (i+5)) and b (towards vertex (i+1)) loses volume at least min(a², b²)/2 outside the hexagon.

theorem ConwaySoifer.wedge_area_strong (i : Fin 6) (T : EquilateralTriangle) (hs : 0 < T.side) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hv : vertex i ∈ T.carrier) (hpa : linePoint (vertex i) (sideDirection i false) a ∈ T.carrier) (hpb : linePoint (vertex i) (sideDirection i true) b ∈ T.carrier) (hab : T.side < a + b) : max (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ hexagon)).toReal

The strong version, valid when the two contained lengths exceed the side.