The 120-degree wedge and the area-loss lemma

sideForm i is the linear form whose level set = 1 is the hexagon side [vertex i, vertex (next i)]. wedge i is the closed 120-degree wedge at vertex i bounded by the two sides through it; it contains the hexagon. The area-loss lemma bounds the part of an equilateral triangle outside the wedge in terms of the lengths of its intersections with the two rays.

Human proof: notes/waste_cycle_reduction.md §1 (geometric) and notes/one_rise_area_reduction_2026_09_06.md §2 (normalised linear forms). In skew units the physical statement |T \ W| ≥ (√3/4)·min(a², b²) reads volume ≥ min(a², b²)/2.

noncomputable def ConwaySoifer.SevenTriangles.sideForm : Fin 6 → Form

The six unit-hexagon facet functionals, each normalized to level one.

Equations

• ConwaySoifer.SevenTriangles.sideForm = ![(1, 1 / 2), (0, 1), (-1, 1 / 2), (-1, -1 / 2), (0, -1), (1, -1 / 2)]

theorem ConwaySoifer.SevenTriangles.sideForm_vertex (i : Fin 6) : formEval (sideForm i) (vertex i) = 1

theorem ConwaySoifer.SevenTriangles.sideForm_vertex_next (i : Fin 6) : formEval (sideForm i) (vertex (next i)) = 1

theorem ConwaySoifer.SevenTriangles.mem_unitHexagon_iff (p : Point) : p ∈ unitHexagon ↔ ∀ (i : Fin 6), formEval (sideForm i) p ≤ 1

def ConwaySoifer.SevenTriangles.wedge (i : Fin 6) : Set Point

The closed 120-degree wedge at vertex i bounded by the two incident sides.

Equations

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

theorem ConwaySoifer.SevenTriangles.unitHexagon_subset_wedge (i : Fin 6) : unitHexagon ⊆ wedge i

theorem ConwaySoifer.SevenTriangles.continuous_formEval (l : Form) : Continuous fun (p : Point) => formEval l p

theorem ConwaySoifer.SevenTriangles.isClosed_wedge (i : Fin 6) : IsClosed (wedge i)

theorem ConwaySoifer.SevenTriangles.measurableSet_wedge (i : Fin 6) : MeasurableSet (wedge i)

Toolkit: membership in a filled triangle

theorem ConwaySoifer.SevenTriangles.mem_convexHull_triangle_of_weights (a b c p : Point) {w₁ w₂ w₃ : ℝ} (h₁ : 0 ≤ w₁) (h₂ : 0 ≤ w₂) (h₃ : 0 ≤ w₃) (hsum : w₁ + w₂ + w₃ = 1) (hp : p = w₁ • a + w₂ • b + w₃ • c) : p ∈ (convexHull ℝ) {a, b, c}

A convex combination of three points lies in their hull.

theorem ConwaySoifer.SevenTriangles.coordDet_barycentric_sum (a b c p : Point) : coordDet (c - b) (p - b) + coordDet (a - c) (p - c) + coordDet (b - a) (p - a) = coordDet (b - a) (c - a)

theorem ConwaySoifer.SevenTriangles.coordDet_barycentric_point (a b c p : Point) : coordDet (b - a) (c - a) • p = coordDet (c - b) (p - b) • a + coordDet (a - c) (p - c) • b + coordDet (b - a) (p - a) • c

theorem ConwaySoifer.SevenTriangles.mem_convexHull_triangle (a b c p : Point) (hdet : 0 < coordDet (b - a) (c - a)) (h₁ : 0 ≤ coordDet (b - a) (p - a)) (h₂ : 0 ≤ coordDet (c - b) (p - b)) (h₃ : 0 ≤ coordDet (a - c) (p - c)) : p ∈ (convexHull ℝ) {a, b, c}

Half-plane description of a positively oriented triangle: the three edge inequalities put a point into the filled triangle.

The polygon in ray coordinates

Write points of the wedge at vertex i as vertex i + α • u + β • w with u, w the unit directions of the two rays. The three edge functionals of an equilateral triangle become σₖ + cₖ α + c_{k+1} β (the coefficient along the second ray is the cyclic shift of the first), with σ₀ + σ₁ + σ₂ = s², c₀ + c₁ + c₂ = 0, c₀² + c₁² + c₂² = 2 s². Everything below is pure algebra in these coordinates; Point = ℝ × ℝ is reused for ray coordinates, coordDet for areas.

def ConwaySoifer.SevenTriangles.InPoly (σ₀ σ₁ σ₂ c₀ c₁ c₂ : ℝ) (q : Point) : Prop

Membership in T ∩ W in ray coordinates.

Equations

• ConwaySoifer.SevenTriangles.InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ q = (0 ≤ q.1 ∧ 0 ≤ q.2 ∧ 0 ≤ σ₀ + c₀ * q.1 + c₁ * q.2 ∧ 0 ≤ σ₁ + c₁ * q.1 + c₂ * q.2 ∧ 0 ≤ σ₂ + c₂ * q.1 + c₀ * q.2)

theorem ConwaySoifer.SevenTriangles.inPoly_shift (σ₀ σ₁ σ₂ c₀ c₁ c₂ : ℝ) (q : Point) : InPoly σ₁ σ₂ σ₀ c₁ c₂ c₀ q ↔ InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ q

noncomputable def ConwaySoifer.SevenTriangles.triArea (q₁ q₂ q₃ : Point) : ℝ

Area of a triangle in ray coordinates.

Equations

• ConwaySoifer.SevenTriangles.triArea q₁ q₂ q₃ = |ConwaySoifer.SevenTriangles.coordDet (q₂ - q₁) (q₃ - q₁)| / 2

theorem ConwaySoifer.SevenTriangles.triArea_nonneg (q₁ q₂ q₃ : Point) : 0 ≤ triArea q₁ q₂ q₃

theorem ConwaySoifer.SevenTriangles.triArea_self (q : Point) : triArea q q q = 0

theorem ConwaySoifer.SevenTriangles.triArea_of_nonneg {q₁ q₂ q₃ : Point} (h : 0 ≤ coordDet (q₂ - q₁) (q₃ - q₁)) : triArea q₁ q₂ q₃ = coordDet (q₂ - q₁) (q₃ - q₁) / 2

def ConwaySoifer.SevenTriangles.CoverBound (σ₀ σ₁ σ₂ c₀ c₁ c₂ A : ℝ) : Prop

The polygon is covered by three (possibly degenerate) triangles of total area at most A.

Equations

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

theorem ConwaySoifer.SevenTriangles.CoverBound.mono {σ₀ σ₁ σ₂ c₀ c₁ c₂ A B : ℝ} (h : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ A) (hAB : A ≤ B) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ B

theorem ConwaySoifer.SevenTriangles.CoverBound.shift {σ₀ σ₁ σ₂ c₀ c₁ c₂ A : ℝ} (h : CoverBound σ₁ σ₂ σ₀ c₁ c₂ c₀ A) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ A

theorem ConwaySoifer.SevenTriangles.coverBound_same_side (σ₀ σ₁ σ₂ c₀ c₁ c₂ a b σ c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hσ : 0 < σ) (hca : σ + c * a = 0) (hdb : σ + d * b = 0) (hL : ∀ (q : Point), InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ q → 0 ≤ σ + c * q.1 + d * q.2) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (a * b / 2)

Both rays exit through the same side σ + c α + d β = 0: the polygon is the triangle O, A, B.

theorem ConwaySoifer.SevenTriangles.quadDet_pos {c₀ c₁ : ℝ} (h : c₀ ≠ 0) : 0 < c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2

Positivity of the determinant c₀² + c₀ c₁ + c₁² of two adjacent edge normals.

theorem ConwaySoifer.SevenTriangles.coverBound_quad (c₀ c₁ σ₁ a b : ℝ) (hc₀ : c₀ < 0) (ha : 0 < a) (hb : 0 < b) (hL₀B : 0 < -c₀ * a + c₁ * b) (hL₂A : 0 < -c₀ * b + (-c₀ - c₁) * a) : CoverBound (-c₀ * a) σ₁ (-c₀ * b) c₀ c₁ (-c₀ - c₁) (c₀ * (2 * c₀ * a * b + (c₀ + c₁) * a ^ 2 - c₁ * b ^ 2) / (2 * (c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2)))

Quadrilateral case: the first ray exits through side 0, the second through side 2, and the common vertex V₀ of these sides lies strictly inside the wedge. Two triangles O A V₀, O V₀ B.

theorem ConwaySoifer.SevenTriangles.coverBound_pent (c₀ c₂ σ₂ a b : ℝ) (hc₀ : c₀ < 0) (hc₂ : c₂ < 0) (ha : 0 < a) (hb : 0 < b) (hσ₂ : σ₂ = c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2 + c₀ * a + c₂ * b) (hL₂A : 0 ≤ σ₂ + c₂ * a) (hL₂B : 0 < σ₂ + c₀ * b) : CoverBound (-c₀ * a) (-c₂ * b) σ₂ c₀ (-c₀ - c₂) c₂ (((c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2) ^ 2 - (-c₀ * (-c₀ - c₂) * a ^ 2 + 2 * c₀ * c₂ * a * b - c₂ * (-c₀ - c₂) * b ^ 2)) / (2 * (c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2)))

Pentagonal case: the first ray exits through side 0, the second through side 1, and the common vertex V₁ of these sides is outside the wedge; the other two vertices V₀, V₂ are inside. Three triangles O A V₀, O V₀ B, V₀ V₂ B. Here c₁ = -c₀ - c₂ and σ₂ = D + c₀ a + c₂ b.

theorem ConwaySoifer.SevenTriangles.strong_core (s X Z a b : ℝ) (hs : 0 < s) (hX : 0 < X) (hZ : 0 ≤ Z) (ha : 0 ≤ a) (hb : 0 ≤ b) (hD : s ^ 2 = X ^ 2 + X * Z + Z ^ 2) (h : (X + Z) * a + X * b < s * (a + b)) : 0 ≤ (X + Z) * b ^ 2 + 2 * Z * a * b - X * a ^ 2

Algebraic core of the strengthened bound: with s² = X² + X Z + Z² and (X + Z) a + X b < s (a + b), the quadratic form (X+Z) b² + 2 Z a b - X a² is nonnegative.

The polynomial inequalities behind the two bounds

theorem ConwaySoifer.SevenTriangles.quad_core_weak (X c₁ a b : ℝ) (hX : 0 < X) (ha : 0 < a) (hb : 0 < b) (hσ₁ : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b)) (h1 : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b) + c₁ * a) (h2 : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b) + (X - c₁) * b) : (X ^ 2 - X * c₁ + c₁ ^ 2) * min (a ^ 2) (b ^ 2) ≤ (X ^ 2 - X * c₁ + c₁ ^ 2) ^ 2 - X * (2 * X * a * b + (X - c₁) * a ^ 2 + c₁ * b ^ 2)

Quadrilateral, weak bound: D · min(a², b²) ≤ D² - X (2 X a b + (X - c₁) a² + c₁ b²) with D = X² - X c₁ + c₁².

theorem ConwaySoifer.SevenTriangles.quad_core_strong (s X c₁ a b : ℝ) (hs : 0 < s) (hX : 0 < X) (ha : 0 < a) (hb : 0 < b) (hD : s ^ 2 = X ^ 2 - X * c₁ + c₁ ^ 2) (hσ₁ : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b)) (h1 : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b) + c₁ * a) (h2 : 0 ≤ X ^ 2 - X * c₁ + c₁ ^ 2 - X * (a + b) + (X - c₁) * b) (hL₀B : 0 < X * a + c₁ * b) (hL₂A : 0 < X * b + (X - c₁) * a) (hab : s < a + b) : (X ^ 2 - X * c₁ + c₁ ^ 2) * max (a ^ 2) (b ^ 2) ≤ (X ^ 2 - X * c₁ + c₁ ^ 2) ^ 2 - X * (2 * X * a * b + (X - c₁) * a ^ 2 + c₁ * b ^ 2)

Quadrilateral, strong bound (s < a + b).

theorem ConwaySoifer.SevenTriangles.pent_core_weak (X Z a b : ℝ) (hX : 0 < X) (hZ : 0 < Z) (ha : 0 < a) (hb : 0 < b) : (X ^ 2 + X * Z + Z ^ 2) * min (a ^ 2) (b ^ 2) ≤ X * (X + Z) * a ^ 2 + 2 * X * Z * a * b + Z * (X + Z) * b ^ 2

Pentagon, weak bound: D · min ≤ Q' with Q' = X C a² + 2 X Z a b + Z C b², C = X + Z.

theorem ConwaySoifer.SevenTriangles.pent_core_strong (s X Z a b : ℝ) (hs : 0 < s) (hX : 0 < X) (hZ : 0 < Z) (ha : 0 < a) (hb : 0 < b) (hD : s ^ 2 = X ^ 2 + X * Z + Z ^ 2) (h1 : (X + Z) * a + Z * b ≤ X ^ 2 + X * Z + Z ^ 2) (h2 : X * a + (X + Z) * b < X ^ 2 + X * Z + Z ^ 2) (hab : s < a + b) : (X ^ 2 + X * Z + Z ^ 2) * max (a ^ 2) (b ^ 2) ≤ X * (X + Z) * a ^ 2 + 2 * X * Z * a * b + Z * (X + Z) * b ^ 2

Pentagon, strong bound (s < a + b), with D ≥ C a + Z b and D > X a + C b.

theorem ConwaySoifer.SevenTriangles.quad_bound (s c₀ c₁ a b : ℝ) (hs : 0 < s) (hc₀ : c₀ < 0) (ha : 0 < a) (hb : 0 < b) (hD : s ^ 2 = c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2) (hσ₁ : 0 ≤ c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2 + c₀ * (a + b)) (hL₁A : 0 ≤ c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2 + c₀ * (a + b) + c₁ * a) (hL₁B : 0 ≤ c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2 + c₀ * (a + b) + (-c₀ - c₁) * b) (hL₀B : 0 < -c₀ * a + c₁ * b) (hL₂A : 0 < -c₀ * b + (-c₀ - c₁) * a) : c₀ * (2 * c₀ * a * b + (c₀ + c₁) * a ^ 2 - c₁ * b ^ 2) / (2 * (c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2)) ≤ s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2 ∧ (s < a + b → c₀ * (2 * c₀ * a * b + (c₀ + c₁) * a ^ 2 - c₁ * b ^ 2) / (2 * (c₀ ^ 2 + c₀ * c₁ + c₁ ^ 2)) ≤ s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2)

The quadrilateral area bound in the form produced by coverBound_quad.

theorem ConwaySoifer.SevenTriangles.pent_bound (s c₀ c₂ σ₂ a b : ℝ) (hs : 0 < s) (hc₀ : c₀ < 0) (hc₂ : c₂ < 0) (ha : 0 < a) (hb : 0 < b) (hD : s ^ 2 = c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2) (hσ₂ : σ₂ = c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2 + c₀ * a + c₂ * b) (hL₂A : 0 ≤ σ₂ + c₂ * a) (hL₂B : 0 < σ₂ + c₀ * b) : ((c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2) ^ 2 - (-c₀ * (-c₀ - c₂) * a ^ 2 + 2 * c₀ * c₂ * a * b - c₂ * (-c₀ - c₂) * b ^ 2)) / (2 * (c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2)) ≤ s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2 ∧ (s < a + b → ((c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2) ^ 2 - (-c₀ * (-c₀ - c₂) * a ^ 2 + 2 * c₀ * c₂ * a * b - c₂ * (-c₀ - c₂) * b ^ 2)) / (2 * (c₀ ^ 2 + c₀ * c₂ + c₂ ^ 2)) ≤ s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2)

The pentagon area bound in the form produced by coverBound_pent.

theorem ConwaySoifer.SevenTriangles.same_side_bound (s a b : ℝ) (hdiam : a ^ 2 + a * b + b ^ 2 ≤ s ^ 2) : a * b / 2 ≤ s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2 ∧ a * b / 2 ≤ s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2

Same-side bound from the diameter.

theorem ConwaySoifer.SevenTriangles.coverBound_zero (s σ₀ σ₁ σ₂ c₀ c₁ c₂ a b : ℝ) (hs : 0 < s) (hσ₀ : 0 ≤ σ₀) (hσ₁ : 0 ≤ σ₁) (hσ₂ : 0 ≤ σ₂) (hsum : σ₀ + σ₁ + σ₂ = s ^ 2) (hc : c₀ + c₁ + c₂ = 0) (hc2 : c₀ ^ 2 + c₁ ^ 2 + c₂ ^ 2 = 2 * s ^ 2) (ha : 0 < a) (hb : 0 < b) (hA : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (a, 0)) (hB : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (0, b)) (hc₀ : c₀ < 0) (hexA : σ₀ + c₀ * a = 0) (hexB : σ₀ + c₁ * b = 0 ∧ c₁ < 0 ∨ σ₁ + c₂ * b = 0 ∧ c₂ < 0 ∨ σ₂ + c₀ * b = 0 ∧ c₀ < 0) (hdiam : a ^ 2 + a * b + b ^ 2 ≤ s ^ 2) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2) ∧ (s < a + b → CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2))

The case tree when the first ray exits through side 0.

theorem ConwaySoifer.SevenTriangles.coverBound_full (s σ₀ σ₁ σ₂ c₀ c₁ c₂ a b : ℝ) (hs : 0 < s) (hσ₀ : 0 ≤ σ₀) (hσ₁ : 0 ≤ σ₁) (hσ₂ : 0 ≤ σ₂) (hsum : σ₀ + σ₁ + σ₂ = s ^ 2) (hc : c₀ + c₁ + c₂ = 0) (hc2 : c₀ ^ 2 + c₁ ^ 2 + c₂ ^ 2 = 2 * s ^ 2) (ha : 0 < a) (hb : 0 < b) (hA : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (a, 0)) (hB : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (0, b)) (hexA : σ₀ + c₀ * a = 0 ∧ c₀ < 0 ∨ σ₁ + c₁ * a = 0 ∧ c₁ < 0 ∨ σ₂ + c₂ * a = 0 ∧ c₂ < 0) (hexB : σ₀ + c₁ * b = 0 ∧ c₁ < 0 ∨ σ₁ + c₂ * b = 0 ∧ c₂ < 0 ∨ σ₂ + c₀ * b = 0 ∧ c₀ < 0) (hdiam : a ^ 2 + a * b + b ^ 2 ≤ s ^ 2) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2) ∧ (s < a + b → CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2))

The case tree for an arbitrary exit side of the first ray, by cyclic relabelling.

theorem ConwaySoifer.SevenTriangles.exists_full_length (σ₀ σ₁ σ₂ c₀ c₁ c₂ a : ℝ) (hσ₀ : 0 ≤ σ₀) (hσ₁ : 0 ≤ σ₁) (hσ₂ : 0 ≤ σ₂) (hneg : c₀ < 0 ∨ c₁ < 0 ∨ c₂ < 0) (ha : 0 ≤ a) (h0 : 0 ≤ σ₀ + c₀ * a) (h1 : 0 ≤ σ₁ + c₁ * a) (h2 : 0 ≤ σ₂ + c₂ * a) : ∃ (a' : ℝ), a ≤ a' ∧ 0 ≤ σ₀ + c₀ * a' ∧ 0 ≤ σ₁ + c₁ * a' ∧ 0 ≤ σ₂ + c₂ * a' ∧ (σ₀ + c₀ * a' = 0 ∧ c₀ < 0 ∨ σ₁ + c₁ * a' = 0 ∧ c₁ < 0 ∨ σ₂ + c₂ * a' = 0 ∧ c₂ < 0)

Extension of a contained length to the full length: the first side hit along the ray.

theorem ConwaySoifer.SevenTriangles.abstract_bound (s σ₀ σ₁ σ₂ c₀ c₁ c₂ a b : ℝ) (hs : 0 < s) (hσ₀ : 0 ≤ σ₀) (hσ₁ : 0 ≤ σ₁) (hσ₂ : 0 ≤ σ₂) (hsum : σ₀ + σ₁ + σ₂ = s ^ 2) (hc : c₀ + c₁ + c₂ = 0) (hc2 : c₀ ^ 2 + c₁ ^ 2 + c₂ ^ 2 = 2 * s ^ 2) (ha : 0 < a) (hb : 0 < b) (hA : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (a, 0)) (hB : InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (0, b)) (hdiam : ∀ (a' b' : ℝ), 0 ≤ a' → 0 ≤ b' → InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (a', 0) → InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (0, b') → a' ^ 2 + a' * b' + b' ^ 2 ≤ s ^ 2) : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - min (a ^ 2) (b ^ 2) / 2) ∧ (s < a + b → CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ (s ^ 2 / 2 - max (a ^ 2) (b ^ 2) / 2))

The abstract wedge lemma: from contained lengths a, b > 0 to a cover of the polygon by three triangles with the required total area.

Concrete filled triangles: half-plane description

theorem ConwaySoifer.SevenTriangles.convex_coordDet_left (g P : Point) : Convex ℝ {p : Point | 0 ≤ coordDet g (p - P)}

theorem ConwaySoifer.SevenTriangles.convex_coordDet_right (g P : Point) : Convex ℝ {p : Point | 0 ≤ coordDet (p - P) g}

theorem ConwaySoifer.SevenTriangles.rotate60_rotateNeg60 (p : Point) : rotate60 (rotateNeg60 p) = p

theorem ConwaySoifer.SevenTriangles.mem_tri_iff (A e p : Point) (he : 0 < sqDist e (0, 0)) : p ∈ (convexHull ℝ) {A, A + e, A + rotate60 e} ↔ 0 ≤ coordDet e (p - A) ∧ 0 ≤ coordDet (rotate60 e - e) (p - (A + e)) ∧ 0 ≤ coordDet (p - A) (rotate60 e)

Half-plane description of the positively oriented filled triangle A, A + e, A + rotate60 e.

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.exists_normal_form (T : EquilateralTriangle) : ∃ (A : Point) (e : Point), sqDist e (0, 0) = T.side ^ 2 ∧ T.carrier = (convexHull ℝ) {A, A + e, A + rotate60 e}

Every filled equilateral triangle is a positively oriented A, A + e, A + rotate60 e.

Ray coordinates at a hexagon vertex

noncomputable def ConwaySoifer.SevenTriangles.rayU (i : Fin 6) : Point

Unit direction of the ray from vertex i towards vertex (previous i).

Equations

• ConwaySoifer.SevenTriangles.rayU i = ConwaySoifer.SevenTriangles.vertex (ConwaySoifer.SevenTriangles.previous i) - ConwaySoifer.SevenTriangles.vertex i

noncomputable def ConwaySoifer.SevenTriangles.rayW (i : Fin 6) : Point

Unit direction of the ray from vertex i towards vertex (next i).

Equations

• ConwaySoifer.SevenTriangles.rayW i = ConwaySoifer.SevenTriangles.vertex (ConwaySoifer.SevenTriangles.next i) - ConwaySoifer.SevenTriangles.vertex i

noncomputable def ConwaySoifer.SevenTriangles.alphaCoord (i : Fin 6) (p : Point) : ℝ

Coordinate along rayU i (vanishes on the side [vertex i, vertex (next i)]).

Equations

• ConwaySoifer.SevenTriangles.alphaCoord i p = 1 - ConwaySoifer.SevenTriangles.formEval (ConwaySoifer.SevenTriangles.sideForm i) p

noncomputable def ConwaySoifer.SevenTriangles.betaCoord (i : Fin 6) (p : Point) : ℝ

Coordinate along rayW i (vanishes on the side [vertex (previous i), vertex i]).

Equations

• ConwaySoifer.SevenTriangles.betaCoord i p = 1 - ConwaySoifer.SevenTriangles.formEval (ConwaySoifer.SevenTriangles.sideForm (ConwaySoifer.SevenTriangles.previous i)) p

theorem ConwaySoifer.SevenTriangles.mem_wedge_iff (i : Fin 6) (p : Point) : p ∈ wedge i ↔ 0 ≤ alphaCoord i p ∧ 0 ≤ betaCoord i p

theorem ConwaySoifer.SevenTriangles.ray_decomp (i : Fin 6) (p : Point) : p = vertex i + (alphaCoord i p • rayU i + betaCoord i p • rayW i)

theorem ConwaySoifer.SevenTriangles.alphaCoord_rayU (i : Fin 6) (a : ℝ) : alphaCoord i (vertex i + a • rayU i) = a

theorem ConwaySoifer.SevenTriangles.betaCoord_rayU (i : Fin 6) (a : ℝ) : betaCoord i (vertex i + a • rayU i) = 0

theorem ConwaySoifer.SevenTriangles.alphaCoord_rayW (i : Fin 6) (b : ℝ) : alphaCoord i (vertex i + b • rayW i) = 0

theorem ConwaySoifer.SevenTriangles.betaCoord_rayW (i : Fin 6) (b : ℝ) : betaCoord i (vertex i + b • rayW i) = b

theorem ConwaySoifer.SevenTriangles.coordDet_rayU_rayW (i : Fin 6) : coordDet (rayU i) (rayW i) = -1

theorem ConwaySoifer.SevenTriangles.sqDist_rays (i : Fin 6) (a b : ℝ) : sqDist (vertex i + a • rayU i) (vertex i + b • rayW i) = a ^ 2 + a * b + b ^ 2

theorem ConwaySoifer.SevenTriangles.edge_decomp (i : Fin 6) (A e p : Point) : coordDet e (p - A) = coordDet e (vertex i - A) + coordDet e (rayU i) * alphaCoord i p + coordDet (rotate60 e - e) (rayU i) * betaCoord i p ∧ coordDet (rotate60 e - e) (p - (A + e)) = coordDet (rotate60 e - e) (vertex i - (A + e)) + coordDet (rotate60 e - e) (rayU i) * alphaCoord i p + coordDet (-rotate60 e) (rayU i) * betaCoord i p ∧ coordDet (p - A) (rotate60 e) = coordDet (vertex i - A) (rotate60 e) + coordDet (-rotate60 e) (rayU i) * alphaCoord i p + coordDet e (rayU i) * betaCoord i p

The three edge functionals of the triangle A, A+e, A+rotate60 e in ray coordinates at vertex i: the coefficient along the second ray is the cyclic shift of the one along the first.

theorem ConwaySoifer.SevenTriangles.edge_sum (A e p : Point) : coordDet e (p - A) + coordDet (rotate60 e - e) (p - (A + e)) + coordDet (p - A) (rotate60 e) = sqDist e (0, 0)

theorem ConwaySoifer.SevenTriangles.coef_sum (i : Fin 6) (e : Point) : coordDet e (rayU i) + coordDet (rotate60 e - e) (rayU i) + coordDet (-rotate60 e) (rayU i) = 0

theorem ConwaySoifer.SevenTriangles.coef_sq (i : Fin 6) (e : Point) : coordDet e (rayU i) ^ 2 + coordDet (rotate60 e - e) (rayU i) ^ 2 + coordDet (-rotate60 e) (rayU i) ^ 2 = 2 * sqDist e (0, 0)

The affine ray map and areas

noncomputable def ConwaySoifer.SevenTriangles.rayMap (i : Fin 6) : ℝ × ℝ →ᵃ[ℝ] Point

q ↦ vertex i + q.1 • rayU i + q.2 • rayW i as an affine map.

Equations

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

theorem ConwaySoifer.SevenTriangles.rayMap_apply (i : Fin 6) (q : ℝ × ℝ) : (rayMap i) q = vertex i + (q.1 • rayU i + q.2 • rayW i)

theorem ConwaySoifer.SevenTriangles.rayMap_image_hull (i : Fin 6) (q₁ q₂ q₃ : ℝ × ℝ) : ⇑(rayMap i) '' (convexHull ℝ) {q₁, q₂, q₃} = (convexHull ℝ) {(rayMap i) q₁, (rayMap i) q₂, (rayMap i) q₃}

theorem ConwaySoifer.SevenTriangles.coordDet_rayMap (i : Fin 6) (q₁ q₂ q₃ : ℝ × ℝ) : coordDet ((rayMap i) q₂ - (rayMap i) q₁) ((rayMap i) q₃ - (rayMap i) q₁) = -coordDet (q₂ - q₁) (q₃ - q₁)

theorem ConwaySoifer.SevenTriangles.volume_rayMap_hull (i : Fin 6) (q₁ q₂ q₃ : ℝ × ℝ) : MeasureTheory.volume (⇑(rayMap i) '' (convexHull ℝ) {q₁, q₂, q₃}) = ENNReal.ofReal (triArea q₁ q₂ q₃)

theorem ConwaySoifer.SevenTriangles.volume_inter_wedge_le (i : Fin 6) (T : EquilateralTriangle) {X : ℝ} (q₁ q₂ q₃ q₄ q₅ q₆ q₇ q₈ q₉ : ℝ × ℝ) (hcov : ∀ p ∈ T.carrier ∩ wedge i, p ∈ ⇑(rayMap i) '' (convexHull ℝ) {q₁, q₂, q₃} ∨ p ∈ ⇑(rayMap i) '' (convexHull ℝ) {q₄, q₅, q₆} ∨ p ∈ ⇑(rayMap i) '' (convexHull ℝ) {q₇, q₈, q₉}) (harea : triArea q₁ q₂ q₃ + triArea q₄ q₅ q₆ + triArea q₇ q₈ q₉ ≤ X) : MeasureTheory.volume (T.carrier ∩ wedge i) ≤ ENNReal.ofReal X

Subadditivity: a cover of T ∩ W by three images of ray-coordinate triangles.

theorem ConwaySoifer.SevenTriangles.volume_diff_ge (i : Fin 6) (T : EquilateralTriangle) {X : ℝ} (hX : 0 ≤ X) (h : MeasureTheory.volume (T.carrier ∩ wedge i) ≤ ENNReal.ofReal X) : T.side ^ 2 / 2 - X ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal

From an upper bound on T ∩ W to a lower bound on T \ W.

theorem ConwaySoifer.SevenTriangles.volume_diff_ge_of_coverBound (i : Fin 6) (T : EquilateralTriangle) (σ₀ σ₁ σ₂ c₀ c₁ c₂ X : ℝ) (hmem : ∀ p ∈ T.carrier ∩ wedge i, InPoly σ₀ σ₁ σ₂ c₀ c₁ c₂ (alphaCoord i p, betaCoord i p)) (hcb : CoverBound σ₀ σ₁ σ₂ c₀ c₁ c₂ X) : T.side ^ 2 / 2 - X ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal

A cover bound in ray coordinates yields the area-loss bound.

theorem ConwaySoifer.SevenTriangles.wedge_area_both (i : Fin 6) (T : EquilateralTriangle) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hv : vertex i ∈ T.carrier) (hpa : vertex i + a • rayU i ∈ T.carrier) (hpb : vertex i + b • rayW i ∈ T.carrier) : min (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal ∧ (T.side < a + b → max (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal)

Both area-loss bounds for positive contained lengths.

theorem ConwaySoifer.SevenTriangles.ray_length_le_side (i : Fin 6) (T : EquilateralTriangle) {b : ℝ} (hv : vertex i ∈ T.carrier) (hpb : vertex i + b • rayW i ∈ T.carrier) : b ≤ T.side

A contained length along a unit ray is at most the side.

theorem ConwaySoifer.SevenTriangles.ray_length_le_side' (i : Fin 6) (T : EquilateralTriangle) {a : ℝ} (hv : vertex i ∈ T.carrier) (hpa : vertex i + a • rayU i ∈ T.carrier) : a ≤ T.side

theorem ConwaySoifer.SevenTriangles.wedge_area_weak (i : Fin 6) (T : EquilateralTriangle) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hv : vertex i ∈ T.carrier) (hpa : vertex i + a • (vertex (previous i) - vertex i) ∈ T.carrier) (hpb : vertex i + b • (vertex (next i) - vertex i) ∈ T.carrier) : min (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal

Weak area-loss bound. a is a length along the ray towards vertex (previous i), b along the ray towards vertex (next i); both rays are unit length in sqDist. Any contained lengths may be used (the bound is monotone), not only the full intersection lengths.

theorem ConwaySoifer.SevenTriangles.wedge_area_strong (i : Fin 6) (T : EquilateralTriangle) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hv : vertex i ∈ T.carrier) (hpa : vertex i + a • (vertex (previous i) - vertex i) ∈ T.carrier) (hpb : vertex i + b • (vertex (next i) - vertex i) ∈ T.carrier) (hab : T.side < a + b) : max (a ^ 2) (b ^ 2) / 2 ≤ (MeasureTheory.volume (T.carrier \ wedge i)).toReal

Strong area-loss bound, valid when the two contained lengths exceed the side.

theorem ConwaySoifer.SevenTriangles.volume_diff_wedge_le (i : Fin 6) (T : EquilateralTriangle) : (MeasureTheory.volume (T.carrier \ wedge i)).toReal ≤ (MeasureTheory.volume (T.carrier \ unitHexagon)).toReal

Loss outside the hexagon dominates loss outside the wedge.