Terminal-color closure at the maximal-gap use site

This file formalizes Sections 6--8 of the project's internal multi-agent proof draft. It closes the three terminal-color obligations left after TailClosure.lean: (1,2)-d₁, (2,1)-d₁, and (2,1)-d₂.

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

Strict order of squared Euclidean distances is strict order of distances.

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

Weak order of squared Euclidean distances is weak order of distances.

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

Strict order of Euclidean distances is strict order of their squares.

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

Four increasing offsets, not necessarily starting at zero, form a strict convex quadrilateral.

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

Every later offset lies in the inward open half-plane of any preceding consecutive boundary pair.

theorem LeanPool.Erdos132ConvexK3.equal_radius_arc_strict_order {a b r₁ r₂ : Point ℝ} (hquad : StrictConvexQuad a b r₁ r₂) (heq : sqDist a r₁ = sqDist a r₂) : sqDist b r₁ < sqDist b r₂

Equal radii from the first vertex of a strict convex quadrilateral are strictly ordered from its consecutive second vertex. This is the kernel form of project proof-draft Lemma 3.4.

theorem LeanPool.Erdos132ConvexK3.fixed_radii_offset_card_le_one {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hInjective : Function.Injective P) (base a b : Fin n) (hab : P a ≠ P b) {S : Finset (Fin n)} {radiusA radiusB : ℝ} (hhalf : ∀ k ∈ S, InLeftOpenHalfPlane (P a) (P b) (P (cyclicAdvance base ↑k))) (hradii : ∀ k ∈ S, sqDist (P a) (P (cyclicAdvance base ↑k)) = radiusA ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = radiusB) : S.card ≤ 1

Fixed radii from two centers determine at most one cyclic offset when all candidate points lie in the same open half-plane.

theorem LeanPool.Erdos132ConvexK3.two_fixed_radius_pairs_card_le_two {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hInjective : Function.Injective P) (base a b : Fin n) (hab : P a ≠ P b) {S : Finset (Fin n)} {a₁ b₁ a₂ b₂ : ℝ} (hhalf : ∀ k ∈ S, InLeftOpenHalfPlane (P a) (P b) (P (cyclicAdvance base ↑k))) (hpairs : ∀ k ∈ S, sqDist (P a) (P (cyclicAdvance base ↑k)) = a₁ ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = b₁ ∨ sqDist (P a) (P (cyclicAdvance base ↑k)) = a₂ ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = b₂) : S.card ≤ 2

Two allowed fixed-radius pairs give at most two cyclic offsets.

theorem LeanPool.Erdos132ConvexK3.three_fixed_radius_pairs_card_le_three {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hInjective : Function.Injective P) (base a b : Fin n) (hab : P a ≠ P b) {S : Finset (Fin n)} {a₁ b₁ a₂ b₂ a₃ b₃ : ℝ} (hhalf : ∀ k ∈ S, InLeftOpenHalfPlane (P a) (P b) (P (cyclicAdvance base ↑k))) (hpairs : ∀ k ∈ S, sqDist (P a) (P (cyclicAdvance base ↑k)) = a₁ ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = b₁ ∨ sqDist (P a) (P (cyclicAdvance base ↑k)) = a₂ ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = b₂ ∨ sqDist (P a) (P (cyclicAdvance base ↑k)) = a₃ ∧ sqDist (P b) (P (cyclicAdvance base ↑k)) = b₃) : S.card ≤ 3

Three allowed fixed-radius pairs give at most three cyclic offsets.

noncomputable def LeanPool.Erdos132ConvexK3.erlvUOffset {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : ℕ

Offset of the first counterclockwise neighbor of x+3, measured from the selected maximal-gap vertex x.

Equations

• LeanPool.Erdos132ConvexK3.erlvUOffset S = 3 + LeanPool.Erdos132ConvexK3.firstNeighborGap P d₁ d₂ d₃ (LeanPool.Erdos132ConvexK3.cyclicAdvance S.x 3)

noncomputable def LeanPool.Erdos132ConvexK3.erlvZOffset {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : ℕ

Offset of the first clockwise neighbor of x, measured counterclockwise from x.

Equations

• LeanPool.Erdos132ConvexK3.erlvZOffset S = n - ↑(LeanPool.Erdos132ConvexK3.firstClockwiseNeighborOffset P d₁ d₂ d₃ S.x)

theorem LeanPool.Erdos132ConvexK3.erlv_u_z_offset_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : 3 < erlvUOffset S ∧ erlvUOffset S + 3 ≤ erlvZOffset S ∧ erlvZOffset S < n ∧ firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3) = cyclicAdvance S.x (erlvUOffset S) ∧ firstClockwiseNeighbor P d₁ d₂ d₃ S.x = cyclicAdvance S.x (erlvZOffset S)

The maximal-gap budget locates u and z with three spare boundary sides between them.

theorem LeanPool.Erdos132ConvexK3.erlv_x_head_card_le {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (β : ℕ) (hβ : β ≤ 1) : {k ∈ ccwNeighborOffsets P d₁ d₂ d₃ S.x | ↑k ≤ erlvUOffset S + β}.card ≤ 4 + β

At most 4+β neighbors of the maximal-gap vertex occur through the offset u+β, for β≤1.

theorem LeanPool.Erdos132ConvexK3.erlv_x_degree_le_of_tail_card {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (β tailCap : ℕ) (hβ : β ≤ 1) (htail : {k ∈ ccwNeighborOffsets P d₁ d₂ d₃ S.x | erlvUOffset S + β < ↑k}.card ≤ tailCap) : vertexDegree P d₁ d₂ d₃ S.x ≤ 4 + β + tailCap

A bound on the offsets after u+β combines with the maximal-gap head count to bound the degree of x.

noncomputable def LeanPool.Erdos132ConvexK3.erlvPUOffset {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : ℕ

The first-neighbor u has offset uoff-1 from p=x+1.

Equations

• LeanPool.Erdos132ConvexK3.erlvPUOffset S = LeanPool.Erdos132ConvexK3.erlvUOffset S - 1

theorem LeanPool.Erdos132ConvexK3.erlv_p_u_offset_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : 2 < erlvPUOffset S ∧ erlvPUOffset S < n ∧ firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3) = cyclicAdvance (cyclicAdvance S.x 1) (erlvPUOffset S)

theorem LeanPool.Erdos132ConvexK3.erlv_p_degree_le_of_arc_cards {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (leftCap tipCap rightCap : ℕ) (hleft : {k ∈ ccwNeighborOffsets P d₁ d₂ d₃ (cyclicAdvance S.x 1) | ↑k < erlvPUOffset S}.card ≤ leftCap) (htip : {k ∈ ccwNeighborOffsets P d₁ d₂ d₃ (cyclicAdvance S.x 1) | ↑k = erlvPUOffset S}.card ≤ tipCap) (hright : {k ∈ ccwNeighborOffsets P d₁ d₂ d₃ (cyclicAdvance S.x 1) | erlvPUOffset S < ↑k}.card ≤ rightCap) : vertexDegree P d₁ d₂ d₃ (cyclicAdvance S.x 1) ≤ leftCap + tipCap + rightCap

Splitting all p-neighbor offsets at u converts two open-arc bounds and the single endpoint bound into a degree bound.

theorem LeanPool.Erdos132ConvexK3.erlv_case12_other_d1_bzero_impossible {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (h12 : S.Case12) (hOther : sqDist (P (cyclicRetreat (firstClockwiseNeighbor P d₁ d₂ d₃ S.x) S.pair.first.leftMoves)) (P (cyclicAdvance S.x 1)) = d₁) (hBZero : S.pair.first.leftMoves = 0) : False

Section 6.1: the no-outer-move part of terminal color (1,2)-d₁.

theorem LeanPool.Erdos132ConvexK3.erlv_case12_other_d1_bone_impossible {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (h12 : S.Case12) (hOther : sqDist (P (cyclicRetreat (firstClockwiseNeighbor P d₁ d₂ d₃ S.x) S.pair.first.leftMoves)) (P (cyclicAdvance S.x 1)) = d₁) (hBOne : S.pair.first.leftMoves = 1) : False

Section 6.2: the one-outer-move part of terminal color (1,2)-d₁.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case12_other_d1_impossible_of_tail : ErLVAtVertexCase12OtherD1Impossible

Session-9 obligation 1/8: terminal color (1,2)-d₁.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case21_other_d1_impossible_of_tail : ErLVAtVertexCase21OtherD1Impossible

Session-9 obligation 3/8: terminal color (2,1)-d₁ (project proof-draft Section 7).

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case21_other_d2_impossible_of_tail : ErLVAtVertexCase21OtherD2Impossible

Session-9 obligation 4/8: terminal color (2,1)-d₂ (project proof-draft Section 8).

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_exceptional_branches_impossible_of_tail : ErLVAtVertexExceptionalBranchesImpossible

All eight terminal-color obligations are now kernel proofs.

theorem LeanPool.Erdos132ConvexK3.erlv_inner_endpoint_separation_complete_of_tail : ErLVInnerEndpointSeparationComplete

The closed eight-color gate proves the source's strict inner-endpoint order without the formerly postulated coordinated exchange.

theorem LeanPool.Erdos132ConvexK3.erlv_majorant_arc_nesting_complete_of_tail : ErLVMajorantArcNestingComplete

The full source-facing ErLV majorant arc-nesting proposition is now an unconditional kernel theorem.