Raw geometric exceptional-word closures

This file connects the local algebraic kernels to finite polygon geometry. Realization records contain only labelled vertices, distance classes, strict quadrilateral and half-plane facts, and pointwise arc partitions. All degree and cardinality bounds are conclusions of the theorems below.

noncomputable def LeanPool.Erdos132ConvexK3.normalizeAlong (a b p : Point ℝ) : Point ℝ

Translate the first center to the origin and rotate the directed center line onto the positive horizontal axis.

Equations

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

theorem LeanPool.Erdos132ConvexK3.normalizeAlong_sqDist {a b : Point ℝ} (hab : a ≠ b) (p q : Point ℝ) : sqDist (normalizeAlong a b p) (normalizeAlong a b q) = sqDist p q

The hand-rolled normalization is an exact Euclidean isometry.

theorem LeanPool.Erdos132ConvexK3.normalizeAlong_turn {a b : Point ℝ} (hab : a ≠ b) (p q r : Point ℝ) : turn (normalizeAlong a b p) (normalizeAlong a b q) (normalizeAlong a b r) = turn p q r

The chosen rotation preserves signed orientation.

theorem LeanPool.Erdos132ConvexK3.normalizeAlong_vertexDegree {n : ℕ} {P : Fin n → Point ℝ} {a b : Point ℝ} (hab : a ≠ b) (d₁ d₂ d₃ : ℝ) (i : Fin n) : vertexDegree (fun (j : Fin n) => normalizeAlong a b (P j)) d₁ d₂ d₃ i = vertexDegree P d₁ d₂ d₃ i

Normalization preserves the executable degree in the top-three graph.

theorem LeanPool.Erdos132ConvexK3.normalizeAlong_top_three_classes {n : ℕ} {P : Fin n → Point ℝ} {a b : Point ℝ} (hab : a ≠ b) {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) : HasTopThreeDistanceClasses (fun (j : Fin n) => normalizeAlong a b (P j)) d₁ d₂ d₃

The three distinguished squared-distance classes survive normalization.

structure LeanPool.Erdos132ConvexK3.Row1B32WordRealization {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) : Type

Raw row-1 terminal B:3→2 geometry from draft Section 6.4.

• pointsInjective : Function.Injective P
• classes : HasTopThreeDistanceClasses P d₁ d₂ d₃
• x : Fin n

  First diameter center.

• vertex : Fin n

  Vertex whose top-three degree is bounded.

• t : Fin n

  Second diameter center.

• w : Fin n

  Penultimate rung point.

• s : Fin n

  Shared terminal tip.

• x_ne_vertex : self.x ≠ self.vertex
• t_ne_vertex : self.t ≠ self.vertex
• x_ne_t : self.x ≠ self.t
• x_ne_w : self.x ≠ self.w
• x_ne_s : self.x ≠ self.s
• t_ne_w : self.t ≠ self.w
• t_ne_s : self.t ≠ self.s
• w_ne_s : self.w ≠ self.s
• w_ne_vertex : self.w ≠ self.vertex
• s_ne_vertex : self.s ≠ self.vertex
• leftArc : Finset (Fin n)

  Boundary vertices on the first-center side.

• rightArc : Finset (Fin n)

  Boundary vertices on the second-center side.

• arcPartition (j : Fin n) : j ≠ self.vertex → j ∈ self.leftArc ∨ j = self.w ∨ j = self.s ∨ j ∈ self.rightArc
• leftHalfPlane (j : Fin n) : j ∈ self.leftArc → InLeftOpenHalfPlane (P self.x) (P self.vertex) (P j)
• left_x_ne (j : Fin n) : j ∈ self.leftArc → self.x ≠ j
• rightHalfPlane (j : Fin n) : j ∈ self.rightArc → InLeftOpenHalfPlane (P self.vertex) (P self.t) (P j)

  The return arc lies to the left of the reversed chord vertex ⟶ t.

• right_t_ne (j : Fin n) : j ∈ self.rightArc → self.t ≠ j
• leftQuad (j : Fin n) : j ∈ self.leftArc → StrictConvexQuad (P self.vertex) (P j) (P self.s) (P self.x)
• rightQuad (j : Fin n) : j ∈ self.rightArc → StrictConvexQuad (P self.t) (P self.s) (P j) (P self.vertex)
• centralLeftQuad : StrictConvexQuad (P self.vertex) (P self.w) (P self.s) (P self.x)
• centralRightQuad : StrictConvexQuad (P self.t) (P self.w) (P self.s) (P self.vertex)
• terminalQuad : StrictConvexQuad (P self.t) (P self.w) (P self.s) (P self.x)
• shortLeftQuad (j : Fin n) : j ∈ self.leftArc → StrictConvexQuad (P self.vertex) (P j) (P self.w) (P self.x)
• xw_le : sqDist (P self.x) (P self.w) ≤ d₂
• xs : sqDist (P self.x) (P self.s) = d₂
• tw : sqDist (P self.t) (P self.w) = d₂
• ts : sqDist (P self.t) (P self.s) = d₁

theorem LeanPool.Erdos132ConvexK3.row1_B32_realization_degree_le_six {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (G : Row1B32WordRealization P d₁ d₂ d₃) : vertexDegree P d₁ d₂ d₃ G.vertex ≤ 6

The row-1 terminal B:3→2 word forces its displayed lower vertex to have degree at most six, derived only from its raw geometry.

structure LeanPool.Erdos132ConvexK3.OnePenultimateWordGeometry {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) : Type

Raw shared-tip geometry with one surviving penultimate rung.

• pointsInjective : Function.Injective P
• classes : HasTopThreeDistanceClasses P d₁ d₂ d₃
• e : Fin n

  First diameter center.

• vertex : Fin n

  Vertex whose top-three degree is bounded.

• t : Fin n

  Second diameter center.

• p : Fin n

  Surviving penultimate rung point.

• s : Fin n

  Shared tip.

• e_ne_vertex : self.e ≠ self.vertex
• t_ne_vertex : self.t ≠ self.vertex
• p_ne_vertex : self.p ≠ self.vertex
• s_ne_vertex : self.s ≠ self.vertex
• e_ne_t : self.e ≠ self.t
• e_ne_s : self.e ≠ self.s
• t_ne_p : self.t ≠ self.p
• t_ne_s : self.t ≠ self.s
• p_ne_s : self.p ≠ self.s
• leftArc : Finset (Fin n)

  Boundary vertices on the first-center side.

• rightArc : Finset (Fin n)

  Boundary vertices on the second-center side.

• arcPartition (j : Fin n) : j ≠ self.vertex → j ∈ self.leftArc ∨ j = self.s ∨ j ∈ self.rightArc
• left_e_ne (j : Fin n) : j ∈ self.leftArc → self.e ≠ j
• right_t_ne (j : Fin n) : j ∈ self.rightArc → self.t ≠ j
• left_s_ne (j : Fin n) : j ∈ self.leftArc → j ≠ self.s
• right_s_ne (j : Fin n) : j ∈ self.rightArc → j ≠ self.s
• leftHalfPlane (j : Fin n) : j ∈ self.leftArc → InLeftOpenHalfPlane (P self.e) (P self.vertex) (P j)
• rightHalfPlane (j : Fin n) : j ∈ self.rightArc → InLeftOpenHalfPlane (P self.vertex) (P self.t) (P j)

  The return arc lies to the left of the reversed chord vertex ⟶ t.

• leftQuad (j : Fin n) : j ∈ self.leftArc → StrictConvexQuad (P self.vertex) (P j) (P self.s) (P self.e)
• rightQuad (j : Fin n) : j ∈ self.rightArc → StrictConvexQuad (P self.t) (P self.s) (P j) (P self.vertex)
• rungQuad : StrictConvexQuad (P self.t) (P self.p) (P self.s) (P self.vertex)
• tipAbove : 0 < turn (P self.e) (P self.t) (P self.s)
• vertexBelow : turn (P self.e) (P self.t) (P self.vertex) < 0
• es : sqDist (P self.e) (P self.s) = d₁
• ts : sqDist (P self.t) (P self.s) = d₁
• tp : sqDist (P self.t) (P self.p) = d₂

theorem LeanPool.Erdos132ConvexK3.one_penultimate_realization_degree_le_five {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (G : OnePenultimateWordGeometry P d₁ d₂ d₃) : vertexDegree P d₁ d₂ d₃ G.vertex ≤ 5

Every raw one-penultimate realization has displayed degree at most five.

structure LeanPool.Erdos132ConvexK3.FourEdgeBranchGeometry {n : ℕ} (P : Fin n → Point ℝ) (d₁ : ℝ) (vertex center central : Fin n) : Type

One raw boundary branch in the four-edge cage. The disjunction records the two cyclic orientations that yield the same edge--diagonal inequality.

• arc : Finset (Fin n)

  Boundary arc assigned to this cage branch.

• center_ne_vertex : center ≠ vertex
• center_ne_arc (j : Fin n) : j ∈ self.arc → center ≠ j
• halfPlane : (∀ j ∈ self.arc, InLeftOpenHalfPlane (P center) (P vertex) (P j)) ∨ ∀ j ∈ self.arc, InLeftOpenHalfPlane (P vertex) (P center) (P j)

  One consistent side of the unoriented line through the two centers.

• quad (j : Fin n) : j ∈ self.arc → StrictConvexQuad (P vertex) (P j) (P central) (P center) ∨ StrictConvexQuad (P center) (P central) (P j) (P vertex)
• diameterEdge : sqDist (P center) (P central) = d₁

structure LeanPool.Erdos132ConvexK3.FourEdgeEndpointGeometry {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (x t w s : Fin n) : Type

Raw data for the two sides counted at one central cage endpoint.

• vertex : Fin n

  Central cage endpoint whose degree is counted.

• w_ne_vertex : w ≠ self.vertex
• s_ne_vertex : s ≠ self.vertex
• left : FourEdgeBranchGeometry P d₁ self.vertex x w

  First-center boundary branch.

• right : FourEdgeBranchGeometry P d₁ self.vertex t s

  Second-center boundary branch.

• arcPartition (j : Fin n) : j ≠ self.vertex → j ∈ self.left.arc ∨ j = w ∨ j = s ∨ j ∈ self.right.arc

structure LeanPool.Erdos132ConvexK3.Row4DDWordRealization {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) : Type

Raw row-4 DD four-edge cage.

• pointsInjective : Function.Injective P
• classes : HasTopThreeDistanceClasses P d₁ d₂ d₃
• x : Fin n

  First diameter center.

• t : Fin n

  Second diameter center.

• w : Fin n

  First central rung endpoint.

• s : Fin n

  Second central rung endpoint.

• w_ne_s : self.w ≠ self.s
• x_ne_w : self.x ≠ self.w
• x_ne_s : self.x ≠ self.s
• t_ne_w : self.t ≠ self.w
• t_ne_s : self.t ≠ self.s
• first : FourEdgeEndpointGeometry P d₁ d₂ d₃ self.x self.t self.w self.s

  First central cage endpoint.

• second : FourEdgeEndpointGeometry P d₁ d₂ d₃ self.x self.t self.w self.s

  Second central cage endpoint.

• first_ne_second : self.first.vertex ≠ self.second.vertex
• xSide : InLeftOpenHalfPlane (P self.w) (P self.s) (P self.x)
• tSide : InLeftOpenHalfPlane (P self.w) (P self.s) (P self.t)
• firstSide : InLeftOpenHalfPlane (P self.w) (P self.s) (P self.first.vertex)
• secondSide : InLeftOpenHalfPlane (P self.w) (P self.s) (P self.second.vertex)
• xw : sqDist (P self.x) (P self.w) = d₁
• xs : sqDist (P self.x) (P self.s) = d₂
• tw : sqDist (P self.t) (P self.w) = d₂
• ts : sqDist (P self.t) (P self.s) = d₁

theorem LeanPool.Erdos132ConvexK3.row4_DD_realization_min_degree_le_six {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (G : Row4DDWordRealization P d₁ d₂ d₃) : min (vertexDegree P d₁ d₂ d₃ G.first.vertex) (vertexDegree P d₁ d₂ d₃ G.second.vertex) ≤ 6

The row-4 DD cage closes by the exact long/short package split.

theorem LeanPool.Erdos132ConvexK3.row4_DD_realization_degree_le_six {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (G : Row4DDWordRealization P d₁ d₂ d₃) : ∃ (v : Fin n), vertexDegree P d₁ d₂ d₃ v ≤ 6

Raw row-4 DD geometry supplies an actual vertex of degree at most six.

structure LeanPool.Erdos132ConvexK3.FullTwoRungGeometry {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) : Type

Raw full-two-rung shared-tip geometry. The four arc pieces are the two open half-planes for each of the two diameter-center circle systems.

• pointsInjective : Function.Injective P
• classes : HasTopThreeDistanceClasses P d₁ d₂ d₃
• e : Fin n

  First diameter center.

• t : Fin n

  Second diameter center.

• s : Fin n

  Shared upper tip.

• w : Fin n

  Penultimate point on the first rung.

• r : Fin n

  Penultimate point on the second rung.

• vertex : Fin n

  Lower vertex whose degree is bounded.

• endpoint : Fin n

  Remaining explicitly separated boundary endpoint.

• e_ne_t : self.e ≠ self.t
• e_ne_s : self.e ≠ self.s
• t_ne_s : self.t ≠ self.s
• w_ne_s : self.w ≠ self.s
• r_ne_s : self.r ≠ self.s
• vertex_ne_e : self.vertex ≠ self.e
• vertex_ne_t : self.vertex ≠ self.t
• vertex_ne_s : self.vertex ≠ self.s
• vertex_ne_w : self.vertex ≠ self.w
• vertex_ne_r : self.vertex ≠ self.r
• tipAbove : 0 < turn (P self.e) (P self.t) (P self.s)
• vertexBelow : turn (P self.e) (P self.t) (P self.vertex) < 0
• wAbove : 0 < turn (P self.e) (P self.t) (P self.w)
• rAbove : 0 < turn (P self.e) (P self.t) (P self.r)
• wBelowTip : turn (P self.e) (P self.t) (P self.w) < turn (P self.e) (P self.t) (P self.s)
• es : sqDist (P self.e) (P self.s) = d₁
• ts : sqDist (P self.t) (P self.s) = d₁
• ew : sqDist (P self.e) (P self.w) = d₁
• tw : sqDist (P self.t) (P self.w) = d₂
• er : sqDist (P self.e) (P self.r) = d₂
• tr : sqDist (P self.t) (P self.r) = d₁
• antiSaturationQuad : StrictConvexQuad (P self.t) (P self.w) (P self.s) (P self.vertex)
• ePositiveArc : Finset (Fin n)

  First-center arc in the positive half-plane.

• eNegativeArc : Finset (Fin n)

  First-center arc in the opposite half-plane.

• tPositiveArc : Finset (Fin n)

  Second-center arc in the positive half-plane.

• tNegativeArc : Finset (Fin n)

  Second-center arc in the opposite half-plane.

• arcPartition (j : Fin n) : j ≠ self.vertex → j ∈ self.ePositiveArc ∨ j ∈ self.eNegativeArc ∨ j ∈ self.tPositiveArc ∨ j ∈ self.tNegativeArc ∨ j = self.s ∨ j = self.endpoint
• ePositive_ne_tip (j : Fin n) : j ∈ self.ePositiveArc → j ≠ self.s
• eNegative_ne_tip (j : Fin n) : j ∈ self.eNegativeArc → j ≠ self.s
• tPositive_ne_tip (j : Fin n) : j ∈ self.tPositiveArc → j ≠ self.s
• tNegative_ne_tip (j : Fin n) : j ∈ self.tNegativeArc → j ≠ self.s
• ePositive_center_ne (j : Fin n) : j ∈ self.ePositiveArc → self.e ≠ j
• eNegative_center_ne (j : Fin n) : j ∈ self.eNegativeArc → self.e ≠ j
• tPositive_center_ne (j : Fin n) : j ∈ self.tPositiveArc → self.t ≠ j
• tNegative_center_ne (j : Fin n) : j ∈ self.tNegativeArc → self.t ≠ j
• ePositiveHalfPlane (j : Fin n) : j ∈ self.ePositiveArc → InLeftOpenHalfPlane (P self.e) (P self.vertex) (P j)
• eNegativeHalfPlane (j : Fin n) : j ∈ self.eNegativeArc → InLeftOpenHalfPlane (P self.vertex) (P self.e) (P j)
• tPositiveHalfPlane (j : Fin n) : j ∈ self.tPositiveArc → InLeftOpenHalfPlane (P self.t) (P self.vertex) (P j)
• tNegativeHalfPlane (j : Fin n) : j ∈ self.tNegativeArc → InLeftOpenHalfPlane (P self.vertex) (P self.t) (P j)
• ePositiveQuad (j : Fin n) : j ∈ self.ePositiveArc → StrictConvexQuad (P self.vertex) (P j) (P self.s) (P self.e)
• eNegativeQuad (j : Fin n) : j ∈ self.eNegativeArc → StrictConvexQuad (P self.vertex) (P j) (P self.s) (P self.e)
• tPositiveQuad (j : Fin n) : j ∈ self.tPositiveArc → StrictConvexQuad (P self.t) (P self.s) (P j) (P self.vertex)
• tNegativeQuad (j : Fin n) : j ∈ self.tNegativeArc → StrictConvexQuad (P self.t) (P self.s) (P j) (P self.vertex)

theorem LeanPool.Erdos132ConvexK3.fullTwoRung_realization_degree_le_six {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (G : FullTwoRungGeometry P d₁ d₂ d₃) : vertexDegree P d₁ d₂ d₃ G.vertex ≤ 6

The full two-rung insertion theorem derived from raw polygon geometry.