Support forms and orientations of equilateral triangles in triangular coordinates

The support value of a direction e at a point q is the determinant cross e q; the three edge directions of an equilateral triangle are e, rot e, rot (rot e) where rot is the rotation by 120 degrees, rot (a, b) = (-a-b, a). The Orientation structure records an exact description of a nondegenerate filled triangle as the intersection of three halfspaces with these normals; the sum of the three offsets equals side · |e|. This is the geometric fact behind the certificate checker: three chosen mandatory points give a lower bound for the side of any triangle of this orientation containing them, and the endpoint/forbidden-point contact conditions are inherited from Halfspaces.lean.

The algebra of the cone lemma (support_bound_on_cone) is adapted from SevenTriangles/Geometry/Support.lean (commit b17ca52a) to the metric a² + ab + b².

def ConwaySoifer.rot (p : Point) : Point

Rotation by 120 degrees.

Equations

• ConwaySoifer.rot p = (-p.1 - p.2, p.1)

def ConwaySoifer.rot60 (p : Point) : Point

Rotation by 60 degrees.

Equations

• ConwaySoifer.rot60 p = (-p.2, p.1 + p.2)

def ConwaySoifer.rotNeg60 (p : Point) : Point

Rotation by -60 degrees.

Equations

• ConwaySoifer.rotNeg60 p = (p.1 + p.2, -p.1)

def ConwaySoifer.rotPow : Fin 3 → Point → Point

rotPow j is rot iterated j times.

Equations

• ConwaySoifer.rotPow = ![id, ConwaySoifer.rot, ConwaySoifer.rot ∘ ConwaySoifer.rot]

@[simp]

theorem ConwaySoifer.rotPow_zero (p : Point) : rotPow 0 p = p

@[simp]

theorem ConwaySoifer.rotPow_one (p : Point) : rotPow 1 p = rot p

@[simp]

theorem ConwaySoifer.rotPow_two (p : Point) : rotPow 2 p = rot (rot p)

theorem ConwaySoifer.rot_rot_rot (p : Point) : rot (rot (rot p)) = p

theorem ConwaySoifer.rot_add (p q : Point) : rot (p + q) = rot p + rot q

theorem ConwaySoifer.rot_sub (p q : Point) : rot (p - q) = rot p - rot q

theorem ConwaySoifer.rot_smul (t : ℝ) (p : Point) : rot (t • p) = t • rot p

theorem ConwaySoifer.rot_neg (p : Point) : rot (-p) = -rot p

theorem ConwaySoifer.rot_sum (p : Point) : p + rot p + rot (rot p) = 0

theorem ConwaySoifer.rotPow_add (j : Fin 3) (p q : Point) : rotPow j (p + q) = rotPow j p + rotPow j q

theorem ConwaySoifer.rotPow_smul (j : Fin 3) (t : ℝ) (p : Point) : rotPow j (t • p) = t • rotPow j p

theorem ConwaySoifer.rot60_rot60 (p : Point) : rot60 (rot60 p) = rot p

theorem ConwaySoifer.rot_rot60 (p : Point) : rot (rot60 p) = -p

theorem ConwaySoifer.rot_rotNeg60 (p : Point) : rot (rotNeg60 p) = rot60 p

theorem ConwaySoifer.rotNeg60_eq (p : Point) : rotNeg60 p = p - rot60 p

Bilinearity of cross and the metric

theorem ConwaySoifer.cross_add_left (u v w : Point) : cross (u + v) w = cross u w + cross v w

theorem ConwaySoifer.cross_add_right (u v w : Point) : cross u (v + w) = cross u v + cross u w

theorem ConwaySoifer.cross_sub_right (u v w : Point) : cross u (v - w) = cross u v - cross u w

theorem ConwaySoifer.cross_sub_left (u v w : Point) : cross (u - v) w = cross u w - cross v w

theorem ConwaySoifer.cross_smul_left (t : ℝ) (u v : Point) : cross (t • u) v = t * cross u v

theorem ConwaySoifer.cross_smul_right (t : ℝ) (u v : Point) : cross u (t • v) = t * cross u v

theorem ConwaySoifer.cross_neg_left (u v : Point) : cross (-u) v = -cross u v

theorem ConwaySoifer.cross_anticomm (u v : Point) : cross u v = -cross v u

theorem ConwaySoifer.cross_rot (u v : Point) : cross (rot u) (rot v) = cross u v

theorem ConwaySoifer.cross_rotPow (j : Fin 3) (u v : Point) : cross (rotPow j u) (rotPow j v) = cross u v

def ConwaySoifer.normSq (u : Point) : ℝ

Squared length of a vector.

Equations

• ConwaySoifer.normSq u = u.1 ^ 2 + u.1 * u.2 + u.2 ^ 2

theorem ConwaySoifer.normSq_eq_sqDist (u : Point) : normSq u = sqDist u (0, 0)

theorem ConwaySoifer.normSq_nonneg (u : Point) : 0 ≤ normSq u

theorem ConwaySoifer.normSq_rot (u : Point) : normSq (rot u) = normSq u

theorem ConwaySoifer.normSq_rotPow (j : Fin 3) (u : Point) : normSq (rotPow j u) = normSq u

theorem ConwaySoifer.normSq_smul (t : ℝ) (u : Point) : normSq (t • u) = t ^ 2 * normSq u

theorem ConwaySoifer.normSq_neg (u : Point) : normSq (-u) = normSq u

theorem ConwaySoifer.normSq_eq_zero_iff (u : Point) : normSq u = 0 ↔ u = 0

theorem ConwaySoifer.normSq_pos_iff (u : Point) : 0 < normSq u ↔ u ≠ 0

noncomputable def ConwaySoifer.metricInner (u v : Point) : ℝ

The metric inner product.

Equations

• ConwaySoifer.metricInner u v = u.1 * v.1 + (u.1 * v.2 + u.2 * v.1) / 2 + u.2 * v.2

theorem ConwaySoifer.metricInner_self (u : Point) : metricInner u u = normSq u

theorem ConwaySoifer.lagrange (u v : Point) : normSq u * normSq v - metricInner u v ^ 2 = 3 / 4 * cross u v ^ 2

theorem ConwaySoifer.normSq_add (u v : Point) : normSq (u + v) = normSq u + normSq v + 2 * metricInner u v

noncomputable def ConwaySoifer.len (u : Point) : ℝ

Euclidean length.

Equations

• ConwaySoifer.len u = √(ConwaySoifer.normSq u)

theorem ConwaySoifer.len_nonneg (u : Point) : 0 ≤ len u

theorem ConwaySoifer.len_sq (u : Point) : len u ^ 2 = normSq u

theorem ConwaySoifer.len_pos_iff (u : Point) : 0 < len u ↔ u ≠ 0

theorem ConwaySoifer.metricInner_le_len_mul_len (u v : Point) : metricInner u v ≤ len u * len v

theorem ConwaySoifer.len_add_le (u v : Point) : len (u + v) ≤ len u + len v

theorem ConwaySoifer.len_smul_nonneg {t : ℝ} (ht : 0 ≤ t) (u : Point) : len (t • u) = t * len u

theorem ConwaySoifer.len_rotPow (j : Fin 3) (u : Point) : len (rotPow j u) = len u

Cones

theorem ConwaySoifer.exists_nonneg_combo_of_cross {u v l : Point} (huv : 0 < cross u v) (hul : 0 ≤ cross u l) (hlv : 0 ≤ cross l v) : ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ l = a • u + b • v

Nonnegative coordinates of a vector inside a two-dimensional cone.

def ConwaySoifer.supportNum (e p₀ p₁ p₂ : Point) : ℝ

The support numerator of a direction for three chosen points.

Equations

• ConwaySoifer.supportNum e p₀ p₁ p₂ = ConwaySoifer.cross e p₀ + ConwaySoifer.cross (ConwaySoifer.rot e) p₁ + ConwaySoifer.cross (ConwaySoifer.rot (ConwaySoifer.rot e)) p₂

theorem ConwaySoifer.supportNum_add (e f p₀ p₁ p₂ : Point) : supportNum (e + f) p₀ p₁ p₂ = supportNum e p₀ p₁ p₂ + supportNum f p₀ p₁ p₂

theorem ConwaySoifer.supportNum_smul (t : ℝ) (e p₀ p₁ p₂ : Point) : supportNum (t • e) p₀ p₁ p₂ = t * supportNum e p₀ p₁ p₂

theorem ConwaySoifer.support_bound_on_cone {u v l p₀ p₁ p₂ : Point} (hu : len u ≤ supportNum u p₀ p₁ p₂) (hv : len v ≤ supportNum v p₀ p₁ p₂) (huv : 0 < cross u v) (hul : 0 ≤ cross u l) (hlv : 0 ≤ cross l v) : len l ≤ supportNum l p₀ p₁ p₂

Endpoint support certificates propagate to every direction of their cone.

The two chiralities of an equilateral triangle

theorem ConwaySoifer.metricInner_rot60 (u : Point) : metricInner u (rot60 u) = normSq u / 2

theorem ConwaySoifer.cross_rot60 (u : Point) : cross u (rot60 u) = normSq u

theorem ConwaySoifer.metricInner_rotNeg60 (u : Point) : metricInner u (rotNeg60 u) = normSq u / 2

theorem ConwaySoifer.cross_rotNeg60 (u : Point) : cross u (rotNeg60 u) = -normSq u

theorem ConwaySoifer.point_eq_of_inner_cross_eq {e p q : Point} (he : 0 < normSq e) (hinner : metricInner e p = metricInner e q) (hcross : cross e p = cross e q) : p = q

theorem ConwaySoifer.sqDist_eq_normSq_sub (p q : Point) : sqDist p q = normSq (p - q)

theorem ConwaySoifer.EquilateralTriangle.thirdVertex_orientation (T : EquilateralTriangle) : T.vertices 2 - T.vertices 0 = rot60 (T.vertices 1 - T.vertices 0) ∨ T.vertices 2 - T.vertices 0 = rotNeg60 (T.vertices 1 - T.vertices 0)

The third vertex of an equilateral triangle is obtained from the first edge by a rotation of ±60 degrees.

Orientations

theorem ConwaySoifer.forall_fin3 {P : Fin 3 → Prop} : (∀ (j : Fin 3), P j) ↔ P 0 ∧ P 1 ∧ P 2

theorem ConwaySoifer.vec3_zero (a b c : ℝ) : ![a, b, c] 0 = a

theorem ConwaySoifer.vec3_one (a b c : ℝ) : ![a, b, c] 1 = b

theorem ConwaySoifer.vec3_two (a b c : ℝ) : ![a, b, c] 2 = c

theorem ConwaySoifer.neg_rot_eq (p : Point) : -rot p = p - rot60 p

theorem ConwaySoifer.rot_rotNeg60_sub (p : Point) : rot (rotNeg60 p - p) = p

theorem ConwaySoifer.rot_eq_neg_rotNeg60 (p : Point) : rot p = -rotNeg60 p

structure ConwaySoifer.Orientation (T : EquilateralTriangle) : Type

An exact halfspace description of a filled triangle whose outward edge directions are the three successive 120-degree rotations of dir, together with the side identity.

• dir : Point

  An outward edge direction in triangular coordinates.

• offset : Fin 3 → ℝ

  The three bounds for the successive rotated edge directions.

• dir_pos : 0 < normSq self.dir
• mem_iff (q : Point) : q ∈ T.carrier ↔ ∀ (j : Fin 3), cross (rotPow j self.dir) q ≤ self.offset j
• sum_offset : self.offset 0 + self.offset 1 + self.offset 2 = T.side * len self.dir

theorem ConwaySoifer.EquilateralTriangle.exists_orientation (T : EquilateralTriangle) (hs : 0 < T.side) : Nonempty (Orientation T)

Consequences used by the checker

theorem ConwaySoifer.Orientation.cross_le {T : EquilateralTriangle} (O : Orientation T) (j : Fin 3) {q : Point} (hq : q ∈ T.carrier) : cross (rotPow j O.dir) q ≤ O.offset j

theorem ConwaySoifer.Orientation.supportNum_le {T : EquilateralTriangle} (O : Orientation T) {p₀ p₁ p₂ : Point} (h₀ : p₀ ∈ T.carrier) (h₁ : p₁ ∈ T.carrier) (h₂ : p₂ ∈ T.carrier) : supportNum O.dir p₀ p₁ p₂ ≤ T.side * len O.dir

Three contained points bound the side from below.

theorem ConwaySoifer.Orientation.len_dir_pos {T : EquilateralTriangle} (O : Orientation T) : 0 < len O.dir

theorem ConwaySoifer.Orientation.one_le_side_of_bound {T : EquilateralTriangle} (O : Orientation T) {p₀ p₁ p₂ : Point} (h₀ : p₀ ∈ T.carrier) (h₁ : p₁ ∈ T.carrier) (h₂ : p₂ ∈ T.carrier) (hb : len O.dir ≤ supportNum O.dir p₀ p₁ p₂) : 1 ≤ T.side

Any direction-form certificate len l ≤ supportNum l … for three contained points forces 1 ≤ side, provided l is a positive multiple of the orientation direction.

def ConwaySoifer.Orientation.system {T : EquilateralTriangle} (O : Orientation T) : HalfspaceSystem (Fin 3)

The halfspace system of an orientation.

Equations

• O.system = { normal := fun (j : Fin 3) => ConwaySoifer.linearForm (-(ConwaySoifer.rotPow j O.dir).2, (ConwaySoifer.rotPow j O.dir).1), offset := O.offset }

theorem ConwaySoifer.Orientation.system_normal_apply {T : EquilateralTriangle} (O : Orientation T) (j : Fin 3) (q : Point) : (O.system.normal j) q = cross (rotPow j O.dir) q

theorem ConwaySoifer.Orientation.carrier_eq_system {T : EquilateralTriangle} (O : Orientation T) : T.carrier = O.system.carrier

theorem ConwaySoifer.Orientation.full_endpoint {T : EquilateralTriangle} (O : Orientation T) {v d : Point} (hv : v ∈ T.carrier) (hd : sqDist d (0, 0) = 1) : ∃ (j : Fin 3), 0 < cross (rotPow j O.dir) d ∧ ∀ q ∈ T.carrier, cross (rotPow j O.dir) q ≤ cross (rotPow j O.dir) (linePoint v d (rayLen T v d))

A full ray endpoint has an outward edge direction with positive exit derivative that is supported at the endpoint.

theorem ConwaySoifer.Orientation.forbidden {T : EquilateralTriangle} (O : Orientation T) {v d : Point} (hv : v ∈ T.carrier) {t : ℝ} (ht : 0 < t) (hout : linePoint v d t ∉ T.carrier) : ∃ (j : Fin 3), 0 < cross (rotPow j O.dir) d ∧ ∀ q ∈ T.carrier, cross (rotPow j O.dir) q < cross (rotPow j O.dir) (linePoint v d t)

A forbidden point on a positive ray from a contained point has a strictly separating outward edge direction with positive exit derivative.

The three 120-degree cones cover the plane

def ConwaySoifer.eastDir : Point

The constant east vector in triangular coordinates.

Equations

• ConwaySoifer.eastDir = (1, 0)

theorem ConwaySoifer.rot_eastDir : rot eastDir = (-1, 1)

theorem ConwaySoifer.cone_cover_of_rot (e : Point) : 0 ≤ cross eastDir e ∧ 0 ≤ cross e (rot eastDir) ∨ 0 ≤ cross eastDir (rot e) ∧ 0 ≤ cross (rot e) (rot eastDir) ∨ 0 ≤ cross eastDir (rot (rot e)) ∧ 0 ≤ cross (rot (rot e)) (rot eastDir)

Relabelling the faces and choosing a representative in the first cone

theorem ConwaySoifer.rotPow_succ (j : Fin 3) (p : Point) : rotPow j (rot p) = rotPow (j + 1) p

def ConwaySoifer.Orientation.rotate {T : EquilateralTriangle} (O : Orientation T) : Orientation T

The same triangle with the faces relabelled cyclically: dir ↦ rot dir.

Equations

• O.rotate = { dir := ConwaySoifer.rot O.dir, offset := fun (j : Fin 3) => O.offset (j + 1), dir_pos := ⋯, mem_iff := ⋯, sum_offset := ⋯ }

theorem ConwaySoifer.EquilateralTriangle.exists_orientation_in_arc (T : EquilateralTriangle) (hs : 0 < T.side) : ∃ (O : Orientation T), 0 ≤ cross eastDir O.dir ∧ 0 ≤ cross O.dir (rot eastDir)

Every nondegenerate triangle has an orientation whose direction lies in the closed cone from eastDir to rot eastDir.

Parallel vectors inside the first cone

theorem ConwaySoifer.exists_parallel_of_cross_eq_zero {u l : Point} (hu : u ≠ 0) (h : cross u l = 0) : ∃ (t : ℝ), l = t • u

theorem ConwaySoifer.pos_of_parallel_in_arc {u l : Point} (hu : u ≠ 0) (hl : l ≠ 0) (hu₁ : 0 ≤ cross eastDir u) (hu₂ : 0 ≤ cross u (rot eastDir)) (hl₁ : 0 ≤ cross eastDir l) (hl₂ : 0 ≤ cross l (rot eastDir)) (h : cross u l = 0) : ∃ (t : ℝ), 0 < t ∧ l = t • u

In the closed cone from eastDir to rot eastDir, a nonzero vector parallel to another nonzero vector of the cone is a positive multiple of it.