Algebra of support forms

A single normal proves a bound only at its own triangle orientation. A global bound needs an additional support-edge theorem plus ALL candidate directions. This file does not silently replace that quantifier with one normal.

@[reducible, inline]

abbrev ConwaySoifer.SevenTriangles.Form : Type

Coordinate coefficients of a real linear functional in oblique coordinates.

Equations

• ConwaySoifer.SevenTriangles.Form = (ℝ × ℝ)

def ConwaySoifer.SevenTriangles.formEval (l : Form) (p : Point) : ℝ

Apply a coordinate linear functional to a point.

Equations

• ConwaySoifer.SevenTriangles.formEval l p = l.1 * p.1 + l.2 * p.2

noncomputable def ConwaySoifer.SevenTriangles.formRotate120 (l : Form) : Form

Rotate a linear functional through 120 degrees in the dual metric.

Equations

• ConwaySoifer.SevenTriangles.formRotate120 l = (-l.1 / 2 - l.2, 3 * l.1 / 4 - l.2 / 2)

noncomputable def ConwaySoifer.SevenTriangles.formNormSq (l : Form) : ℝ

Squared dual norm of a coordinate linear functional.

Equations

• ConwaySoifer.SevenTriangles.formNormSq l = 3 / 4 * l.1 ^ 2 + l.2 ^ 2

noncomputable def ConwaySoifer.SevenTriangles.formNorm (l : Form) : ℝ

The nonnegative dual norm of a coordinate linear functional.

Equations

• ConwaySoifer.SevenTriangles.formNorm l = √(ConwaySoifer.SevenTriangles.formNormSq l)

noncomputable def ConwaySoifer.SevenTriangles.formInner (l m : Form) : ℝ

The dual metric inner product of two coordinate linear functionals.

Equations

• ConwaySoifer.SevenTriangles.formInner l m = 3 / 4 * l.1 * m.1 + l.2 * m.2

def ConwaySoifer.SevenTriangles.formDet (l m : Form) : ℝ

The coordinate determinant of two linear-functional coefficient vectors.

Equations

• ConwaySoifer.SevenTriangles.formDet l m = l.1 * m.2 - l.2 * m.1

def ConwaySoifer.SevenTriangles.formNeg (l : Form) : Form

Negate a coordinate linear functional.

Equations

• ConwaySoifer.SevenTriangles.formNeg l = (-l.1, -l.2)

def ConwaySoifer.SevenTriangles.vectorNormal (p : Point) : Form

The determinant functional associated with a planar direction.

Equations

• ConwaySoifer.SevenTriangles.vectorNormal p = (-p.2, p.1)

def ConwaySoifer.SevenTriangles.edgeNormal (p q : Point) : Form

The determinant normal associated with an oriented edge.

Equations

• ConwaySoifer.SevenTriangles.edgeNormal p q = ConwaySoifer.SevenTriangles.vectorNormal (q - p)

noncomputable def ConwaySoifer.SevenTriangles.metricInner (p q : Point) : ℝ

The Euclidean inner product expressed in oblique coordinates.

Equations

• ConwaySoifer.SevenTriangles.metricInner p q = p.1 * q.1 + 3 / 4 * p.2 * q.2

def ConwaySoifer.SevenTriangles.coordDet (p q : Point) : ℝ

The coordinate determinant used for affine area calculations.

Equations

• ConwaySoifer.SevenTriangles.coordDet p q = p.1 * q.2 - p.2 * q.1

noncomputable def ConwaySoifer.SevenTriangles.rotateNeg60 (p : Point) : Point

Rotation through negative 60 degrees in oblique coordinates.

Equations

• ConwaySoifer.SevenTriangles.rotateNeg60 p = (p.1 / 2 + 3 * p.2 / 4, -p.1 + p.2 / 2)

theorem ConwaySoifer.SevenTriangles.rotated_form_sum (l : Form) (p : Point) : formEval l p + formEval (formRotate120 l) p + formEval (formRotate120 (formRotate120 l)) p = 0

theorem ConwaySoifer.SevenTriangles.formNormSq_rotate (l : Form) : formNormSq (formRotate120 l) = formNormSq l

theorem ConwaySoifer.SevenTriangles.formNormSq_neg (l : Form) : formNormSq (formNeg l) = formNormSq l

theorem ConwaySoifer.SevenTriangles.formNormSq_nonneg (l : Form) : 0 ≤ formNormSq l

theorem ConwaySoifer.SevenTriangles.formNormSq_pos_left_of_det_pos {l m : Form} (h : 0 < formDet l m) : 0 < formNormSq l

theorem ConwaySoifer.SevenTriangles.formNormSq_pos_right_of_det_pos {l m : Form} (h : 0 < formDet l m) : 0 < formNormSq m

theorem ConwaySoifer.SevenTriangles.formNorm_nonneg (l : Form) : 0 ≤ formNorm l

theorem ConwaySoifer.SevenTriangles.formNorm_sq (l : Form) : formNorm l ^ 2 = formNormSq l

theorem ConwaySoifer.SevenTriangles.form_inner_lagrange (l m : Form) : formNormSq l * formNormSq m - formInner l m ^ 2 = 3 / 4 * (l.1 * m.2 - l.2 * m.1) ^ 2

theorem ConwaySoifer.SevenTriangles.formInner_le_norm_mul_norm (l m : Form) : formInner l m ≤ formNorm l * formNorm m

theorem ConwaySoifer.SevenTriangles.formNorm_add_le (l m : Form) : formNorm (l + m) ≤ formNorm l + formNorm m

theorem ConwaySoifer.SevenTriangles.formNorm_nonneg_smul (a : ℝ) (ha : 0 ≤ a) (l : Form) : formNorm (a • l) = a * formNorm l

theorem ConwaySoifer.SevenTriangles.exists_nonneg_combo_of_det {u v l : Form} (huv : 0 < formDet u v) (hul : 0 ≤ formDet u l) (hlv : 0 ≤ formDet l v) : ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ l = a • u + b • v

Determinant signs give the explicit nonnegative coordinates of a vector inside a two-dimensional cone.

noncomputable def ConwaySoifer.SevenTriangles.supportNumerator (l : Form) (p₀ p₁ p₂ : Point) : ℝ

The sum of support values at three successive equilateral-triangle normals.

Equations

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

theorem ConwaySoifer.SevenTriangles.supportNumerator_add (l m : Form) (p₀ p₁ p₂ : Point) : supportNumerator (l + m) p₀ p₁ p₂ = supportNumerator l p₀ p₁ p₂ + supportNumerator m p₀ p₁ p₂

theorem ConwaySoifer.SevenTriangles.supportNumerator_smul (a : ℝ) (l : Form) (p₀ p₁ p₂ : Point) : supportNumerator (a • l) p₀ p₁ p₂ = a * supportNumerator l p₀ p₁ p₂

theorem ConwaySoifer.SevenTriangles.support_bound_on_cone {u v l : Form} {p₀ p₁ p₂ : Point} (hu : formNorm u ≤ supportNumerator u p₀ p₁ p₂) (hv : formNorm v ≤ supportNumerator v p₀ p₁ p₂) (huv : 0 < formDet u v) (hul : 0 ≤ formDet u l) (hlv : 0 ≤ formDet l v) : formNorm l ≤ supportNumerator l p₀ p₁ p₂

Endpoint support certificates propagate to every direction in their cone. This is the algebraic completeness step used by the finite orientation fan.

theorem ConwaySoifer.SevenTriangles.formEval_neg (l : Form) (p : Point) : formEval (formNeg l) p = -formEval l p

theorem ConwaySoifer.SevenTriangles.formRotate120_neg (l : Form) : formRotate120 (formNeg l) = formNeg (formRotate120 l)

theorem ConwaySoifer.SevenTriangles.edgeNormal_reverse (p q : Point) : edgeNormal q p = formNeg (edgeNormal p q)

theorem ConwaySoifer.SevenTriangles.formNormSq_edgeNormal (p q : Point) : formNormSq (edgeNormal p q) = sqDist p q

theorem ConwaySoifer.SevenTriangles.edgeNormal_equal_on_endpoints (p q : Point) : formEval (edgeNormal p q) p = formEval (edgeNormal p q) q

theorem ConwaySoifer.SevenTriangles.edgeNormal_eval_gap (p q r : Point) : formEval (edgeNormal p q) r - formEval (edgeNormal p q) p = (q.1 - p.1) * (r.2 - p.2) - (q.2 - p.2) * (r.1 - p.1)

theorem ConwaySoifer.SevenTriangles.formRotate120_vectorNormal (p : Point) : formRotate120 (vectorNormal p) = vectorNormal (rotate60 p - p)

theorem ConwaySoifer.SevenTriangles.formRotate120_twice_vectorNormal (p : Point) : formRotate120 (formRotate120 (vectorNormal p)) = vectorNormal (-rotate60 p)

theorem ConwaySoifer.SevenTriangles.formRotate120_vectorNormal_clockwise (p : Point) : formRotate120 (vectorNormal p) = vectorNormal (-rotateNeg60 p)

theorem ConwaySoifer.SevenTriangles.formRotate120_twice_vectorNormal_clockwise (p : Point) : formRotate120 (formRotate120 (vectorNormal p)) = vectorNormal (rotateNeg60 p - p)

theorem ConwaySoifer.SevenTriangles.metric_lagrange (p q : Point) : sqDist p (0, 0) * sqDist q (0, 0) - metricInner p q ^ 2 = 3 / 4 * coordDet p q ^ 2

theorem ConwaySoifer.SevenTriangles.metricInner_rotate60 (p : Point) : metricInner p (rotate60 p) = sqDist p (0, 0) / 2

theorem ConwaySoifer.SevenTriangles.coordDet_rotate60 (p : Point) : coordDet p (rotate60 p) = sqDist p (0, 0)

theorem ConwaySoifer.SevenTriangles.metricInner_rotateNeg60 (p : Point) : metricInner p (rotateNeg60 p) = sqDist p (0, 0) / 2

theorem ConwaySoifer.SevenTriangles.coordDet_rotateNeg60 (p : Point) : coordDet p (rotateNeg60 p) = -sqDist p (0, 0)

theorem ConwaySoifer.SevenTriangles.point_eq_of_inner_det_eq {e p q : Point} (he : 0 < sqDist e (0, 0)) (hinner : metricInner e p = metricInner e q) (hdet : coordDet e p = coordDet e q) : p = q

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.edge_support_gap_sq (T : EquilateralTriangle) : (formEval (edgeNormal (T.vertices 0) (T.vertices 1)) (T.vertices 2) - formEval (edgeNormal (T.vertices 0) (T.vertices 1)) (T.vertices 0)) ^ 2 = T.side ^ 4

For an equilateral triangle, the support gap normal to one edge has absolute value side². This algebraic identity is the normalization used by the finite orientation certificates.

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.edge_support_gap_cases (T : EquilateralTriangle) : have gap := formEval (edgeNormal (T.vertices 0) (T.vertices 1)) (T.vertices 2) - formEval (edgeNormal (T.vertices 0) (T.vertices 1)) (T.vertices 0); gap = T.side ^ 2 ∨ gap = -T.side ^ 2

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.thirdVertex_orientation (T : EquilateralTriangle) : T.vertices 2 - T.vertices 0 = rotate60 (T.vertices 1 - T.vertices 0) ∨ T.vertices 2 - T.vertices 0 = rotateNeg60 (T.vertices 1 - T.vertices 0)

The equilateral equations classify the third vertex into the two genuine orientations. No alignment or orientation is assumed.

theorem ConwaySoifer.SevenTriangles.convex_formEval_superlevel (l : Form) (c : ℝ) : Convex ℝ {p : Point | c ≤ formEval l p}

A lower support half-plane is convex in the rational coordinate model.

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.formEval_lower_bound (T : EquilateralTriangle) (l : Form) (c : ℝ) (hvertices : ∀ (i : Fin 3), c ≤ formEval l (T.vertices i)) {p : Point} (hp : p ∈ T.carrier) : c ≤ formEval l p

A linear support inequality checked at all three vertices holds on the entire filled triangle. This is the trusted bridge from support calculations to the carrier, rather than an assumption that a witness lies at a vertex.

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.formEval_upper_bound (T : EquilateralTriangle) (l : Form) (c : ℝ) (hvertices : ∀ (i : Fin 3), formEval l (T.vertices i) ≤ c) {p : Point} (hp : p ∈ T.carrier) : formEval l p ≤ c

The analogous upper support inequality on a filled triangle.

theorem ConwaySoifer.SevenTriangles.ccw_edge_gaps (a e : Point) : have b := a + e; have c := a + rotate60 e; formEval (edgeNormal a b) c - formEval (edgeNormal a b) a = sqDist e (0, 0) ∧ formEval (edgeNormal b c) a - formEval (edgeNormal b c) b = sqDist e (0, 0) ∧ formEval (edgeNormal c a) b - formEval (edgeNormal c a) c = sqDist e (0, 0)

theorem ConwaySoifer.SevenTriangles.cw_edge_gaps (a e : Point) : have b := a + e; have c := a + rotateNeg60 e; formEval (edgeNormal b a) c - formEval (edgeNormal b a) b = sqDist e (0, 0) ∧ formEval (edgeNormal a c) b - formEval (edgeNormal a c) a = sqDist e (0, 0) ∧ formEval (edgeNormal c b) a - formEval (edgeNormal c b) c = sqDist e (0, 0)

theorem ConwaySoifer.SevenTriangles.ccw_support_min_sum (a e : Point) : have b := a + e; have c := a + rotate60 e; have l := vectorNormal e; formEval l a + formEval (formRotate120 l) b + formEval (formRotate120 (formRotate120 l)) c = -sqDist e (0, 0)

theorem ConwaySoifer.SevenTriangles.cw_support_min_sum (a e : Point) : have b := a + e; have c := a + rotateNeg60 e; have l := vectorNormal e; formEval (formNeg l) b + formEval (formRotate120 (formNeg l)) a + formEval (formRotate120 (formRotate120 (formNeg l))) c = -sqDist e (0, 0)

theorem ConwaySoifer.SevenTriangles.EquilateralTriangle.exists_own_orientation_support_bound (T : EquilateralTriangle) : ∃ (l : Form), 0 < formNorm l ∧ ∀ {p₀ p₁ p₂ : Point}, p₀ ∈ T.carrier → p₁ ∈ T.carrier → p₂ ∈ T.carrier → supportNumerator l p₀ p₁ p₂ ≤ T.side * formNorm l

Every equilateral triangle has one inward support orientation, independent of the three contained points subsequently tested. Both chiralities are derived from the equilateral equations.

theorem ConwaySoifer.SevenTriangles.candidate_bound {N D : ℝ} (hN : 0 ≤ N) (hD : 0 < D) (hgap : D ≤ N ^ 2) : 1 ≤ N / √D

Exact algebra behind the certificate test N >= 0, N*N >= D.

theorem ConwaySoifer.SevenTriangles.support_sum_bound (l : Form) (p₀ p₁ p₂ c : Point) (s₀ s₁ s₂ r D : ℝ) (h₀ : 0 ≤ formEval l p₀ - formEval l c + s₀) (h₁ : 0 ≤ formEval (formRotate120 l) p₁ - formEval (formRotate120 l) c + s₁) (h₂ : 0 ≤ formEval (formRotate120 (formRotate120 l)) p₂ - formEval (formRotate120 (formRotate120 l)) c + s₂) (hs : s₀ + s₁ + s₂ = r * √D) : -(formEval l p₀ + formEval (formRotate120 l) p₁ + formEval (formRotate120 (formRotate120 l)) p₂) ≤ r * √D

Sum three chosen support inequalities. No minimizer-selection assumption is needed.