Maximal-gap tail closure

This file formalizes the counting and elementary geometry in Lemma 4.1 of the project's internal multi-agent proof draft. The argument splits the neighbors of the maximal-gap vertex at the first counterclockwise neighbor of x + 3: the head has at most four offsets, while strict edge--diagonal comparison and same-half-plane two-circle uniqueness leave at most two tail slots (one under the strict anchor).

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_injective {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (hn : 3 ≤ n) : Function.Injective P

Strict cyclic convexity makes the labelled boundary map injective.

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_quad_zero_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {b c d : ℕ} (hb : 0 < b) (hbc : b < c) (hcd : c < d) (hdn : d < n) : StrictConvexQuad (P base) (P (cyclicAdvance base b)) (P (cyclicAdvance base c)) (P (cyclicAdvance base d))

Four increasing offsets in one turn form a strict convex quadrilateral.

theorem LeanPool.Erdos132ConvexK3.cyclic_offset_in_left_open_half_plane {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {k : ℕ} (hk : 1 < k) (hkn : k < n) : InLeftOpenHalfPlane (P base) (P (cyclicAdvance base 1)) (P (cyclicAdvance base k))

Every positive offset past the next vertex is in the common open half-plane of the consecutive centers base, base + 1.

theorem LeanPool.Erdos132ConvexK3.cyclic_fixed_radii_offset_card_le_one {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (hn : 3 ≤ n) (base : Fin n) {S : Finset (Fin n)} {radiusBase radiusNext : ℝ} (hlower : ∀ k ∈ S, 1 < ↑k) (hradii : ∀ k ∈ S, sqDist (P base) (P (cyclicAdvance base ↑k)) = radiusBase ∧ sqDist (P (cyclicAdvance base 1)) (P (cyclicAdvance base ↑k)) = radiusNext) : S.card ≤ 1

A fixed ordered pair of radii contributes at most one cyclic offset in the open half-plane beyond the next vertex.

theorem LeanPool.Erdos132ConvexK3.ccw_neighbor_offset_le_clockwise_boundary {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v k : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) (hk : k ∈ ccwNeighborOffsets P d₁ d₂ d₃ v) : ↑k + ↑(firstClockwiseNeighborOffset P d₁ d₂ d₃ v) ≤ n

A counterclockwise neighbor cannot pass the offset representing the first clockwise neighbor.

theorem LeanPool.Erdos132ConvexK3.euclideanDist_eq_of_sqDist_eq {a b c d : Point ℝ} (h : sqDist a b = sqDist c d) : euclideanDist a b = euclideanDist c d

Equality of squared distances is equality of ordinary Euclidean distances.

theorem LeanPool.Erdos132ConvexK3.edge_diagonal_inequality_rotated {x p u r : Point ℝ} (hquad : StrictConvexQuad x p u r) : euclideanDist p u + euclideanDist x r < euclideanDist p r + euclideanDist x u

The second strict edge--diagonal inequality, obtained by rotating the four cyclic vertices once.

theorem LeanPool.Erdos132ConvexK3.far_arc_strict_center_comparison {x p u r : Point ℝ} (hquad : StrictConvexQuad x p u r) (hanchor : sqDist x u ≤ sqDist p u) : sqDist x r < sqDist p r

If the anchor from the first center is no longer than the anchor from the next center, strict edge--diagonal comparison reverses that order at a point on the far arc.

theorem LeanPool.Erdos132ConvexK3.strict_top_three_rank_slots {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {x p r : Fin n} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hxr : TopThreeAdjacent P d₁ d₂ d₃ x r) (hpr : TopThreeAdjacent P d₁ d₂ d₃ p r) (hlt : sqDist (P x) (P r) < sqDist (P p) (P r)) : sqDist (P x) (P r) = d₂ ∧ sqDist (P p) (P r) = d₁ ∨ sqDist (P x) (P r) = d₃ ∧ sqDist (P p) (P r) = d₁ ∨ sqDist (P x) (P r) = d₃ ∧ sqDist (P p) (P r) = d₂

With exactly three ranked distances, a strict comparison has only the three ordered radius slots used in the project proof draft.

theorem LeanPool.Erdos132ConvexK3.maximal_gap_tail_degree_bounds {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (hpu : sqDist (P (cyclicAdvance S.x 1)) (P (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3))) = d₁) (hxz : sqDist (P S.x) (P (firstClockwiseNeighbor P d₁ d₂ d₃ S.x)) = d₃) (hpz : sqDist (P (cyclicAdvance S.x 1)) (P (firstClockwiseNeighbor P d₁ d₂ d₃ S.x)) = d₂) : (sqDist (P S.x) (P (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3))) = d₁ → vertexDegree P d₁ d₂ d₃ S.x ≤ 6) ∧ (sqDist (P S.x) (P (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3))) = d₂ → vertexDegree P d₁ d₂ d₃ S.x ≤ 5)

Maximal-gap tail lemma (project proof-draft Lemma 4.1). Suppose p = x + 1, u is the first counterclockwise neighbor of x + 3, and z is the first clockwise neighbor of x. Under the three displayed ladder colors, an xu = d₁ anchor gives degree at most six, while xu = d₂ gives degree at most five.

theorem LeanPool.Erdos132ConvexK3.erlv_x_p_u_z_strict_convex_quad {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : StrictConvexQuad (P S.x) (P (cyclicAdvance S.x 1)) (P (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3))) (P (firstClockwiseNeighbor P d₁ d₂ d₃ S.x))

The four vertices x, x+1, u, z used by the tail lemma occur in strict cyclic order at every maximal-gap degree-seven use site.

theorem LeanPool.Erdos132ConvexK3.d1_d3_opposite_sides_force_xu_top_two {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {x p u z : Fin n} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hquad : StrictConvexQuad (P x) (P p) (P u) (P z)) (hxzAdj : TopThreeAdjacent P d₁ d₂ d₃ x z) (hpu : sqDist (P p) (P u) = d₁) (hxz : sqDist (P x) (P z) = d₃) (hpz : sqDist (P p) (P z) = d₂) : sqDist (P x) (P u) = d₁ ∨ sqDist (P x) (P u) = d₂

If the opposite sides pu,zx have ranks d₁,d₃ and the diagonal pz has rank d₂, strict ED forces the other diagonal xu into d₁ ∨ d₂.

theorem LeanPool.Erdos132ConvexK3.erlv_case22_tail_rank_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (h22 : S.Case22) : have z := firstClockwiseNeighbor P d₁ d₂ d₃ S.x; have u := firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3); sqDist (P (cyclicAdvance S.x 1)) (P u) = d₁ ∧ sqDist (P S.x) (P z) = d₃ ∧ sqDist (P (cyclicAdvance S.x 1)) (P z) = d₂ ∧ (sqDist (P S.x) (P u) = d₁ ∨ sqDist (P S.x) (P u) = d₂)

The rigid (2,2) ladders supply every hypothesis of the tail lemma and force xu into one of its two clauses.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_impossible_of_tail : ErLVAtVertexCase22Impossible

The maximal-gap tail lemma closes the whole rigid (2,2) branch.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_zt_d1_impossible_of_tail : ErLVAtVertexCase22ZTD1Impossible

Session-9 obligation 5/8, discharged by unconditional branch closure.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_zt_d2_impossible_of_tail : ErLVAtVertexCase22ZTD2Impossible

Session-9 obligation 6/8, discharged by unconditional branch closure.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_xu_d1_impossible_of_tail : ErLVAtVertexCase22XUD1Impossible

Session-9 obligation 7/8, discharged by unconditional branch closure.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_xu_d2_impossible_of_tail : ErLVAtVertexCase22XUD2Impossible

Session-9 obligation 8/8, discharged by unconditional branch closure.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.one_left_one_right_end_at_d1 {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j : Fin n} (hStart : TopThreeAdjacent P d₁ d₂ d₃ i j) (path : K3CoverSequence P i j 1 1) : sqDist (P (cyclicRetreat i 1)) (P (cyclicAdvance j 1)) = d₁

A path with one left and one right cover has made two strict rank increases, regardless of their order, so it ends in d₁.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case12_other_d2_impossible_of_tail : ErLVAtVertexCase12OtherD2Impossible

The tail lemma closes the (1,2) shared-tip subcase whose other terminal edge has color d₂.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_exceptional_branches_impossible_of_remaining_three (h12D1 : ErLVAtVertexCase12OtherD1Impossible) (h21D1 : ErLVAtVertexCase21OtherD1Impossible) (h21D2 : ErLVAtVertexCase21OtherD2Impossible) : ErLVAtVertexExceptionalBranchesImpossible

Session-11 boundary: after the maximal-gap tail port, only the three shared-tip colors (1,2)-d₁, (2,1)-d₁, and (2,1)-d₂ remain.