The ErLV reduction at its actual use site

The global proof uses the majorant diagram only inside the contradiction branch in which every vertex has degree at least seven. It does not need an abstract exchange producing a cheaper majorant pair. This file therefore keeps ErLVCoordinatedMajorantExchangeComplete as the documented stronger open statement and names the weaker obligation actually needed: an exceptional jointly minimal pair at the selected maximal-gap vertex is impossible.

The use-site package keeps only the data consumed by the branch proofs.

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

All data present where the ErLV diagram is actually invoked: a convex top-three configuration in the high-minimum-degree contradiction branch, a maximal-gap vertex x, and the jointly minimal pair selected around x and x+3.

• convex : CyclicStrictConvex P
• classes : HasTopThreeDistanceClasses P d₁ d₂ d₃
• highDegree (v : Fin n) : 7 ≤ vertexDegree P d₁ d₂ d₃ v
• x : Fin n

  Selected vertex with maximal first-neighbor gap.

• maximalGap (v : Fin n) : firstNeighborGap P d₁ d₂ d₃ v ≤ firstNeighborGap P d₁ d₂ d₃ self.x
• pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ self.x) self.x (cyclicAdvance self.x 3) (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance self.x 3))

  Jointly minimal pair of facing majorant paths.

noncomputable def LeanPool.Erdos132ConvexK3.erlvAtVertexUseSiteOfHighDegree {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hHigh : ∀ (v : Fin n), 7 ≤ vertexDegree P d₁ d₂ d₃ v) (x : Fin n) (hMax : ∀ (v : Fin n), firstNeighborGap P d₁ d₂ d₃ v ≤ firstNeighborGap P d₁ d₂ d₃ x) (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ x) x (cyclicAdvance x 3) (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3))) : ErLVAtVertexUseSite P d₁ d₂ d₃

Package an actual contradiction-branch use site.

Equations

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

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

The exceptional branch with inner endpoint move counts (1,2).

Equations

• S.Case12 = (S.pair.first.rightMoves = 1 ∧ S.pair.second.leftMoves = 2)

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

The exceptional branch with inner endpoint move counts (2,1).

Equations

• S.Case21 = (S.pair.first.rightMoves = 2 ∧ S.pair.second.leftMoves = 1)

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

The exceptional branch with inner endpoint move counts (2,2).

Equations

• S.Case22 = (S.pair.first.rightMoves = 2 ∧ S.pair.second.leftMoves = 2)

def LeanPool.Erdos132ConvexK3.ErLVAtVertexExceptionalBranchesImpossible : Prop

The exact weakened lemma needed at the reduction use site. A direct geometric contradiction is enough; no cheaper pair need be constructed.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase12Impossible : Prop

The (1,2) exceptional branch is impossible at the use site.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase21Impossible : Prop

The (2,1) exceptional branch is impossible at the use site.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase22Impossible : Prop

The (2,2) exceptional branch is impossible at the use site.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_exceptional_branches_impossible_iff_cases : ErLVAtVertexExceptionalBranchesImpossible ↔ ErLVAtVertexCase12Impossible ∧ ErLVAtVertexCase21Impossible ∧ ErLVAtVertexCase22Impossible

The at-use-site obligation is exactly the conjunction of the three rigid branches and nothing stronger.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_exceptional_branches_impossible_of_exchange (hExchange : ErLVCoordinatedMajorantExchangeComplete) : ErLVAtVertexExceptionalBranchesImpossible

The old exchange statement implies the narrowed use-site statement, so the pivot weakens the missing obligation rather than changing the theorem.

theorem LeanPool.Erdos132ConvexK3.erlv_inner_endpoint_separation_complete_of_at_vertex_closure (hClose : ErLVAtVertexExceptionalBranchesImpossible) : ErLVInnerEndpointSeparationComplete

Killing the three branches directly at the use site supplies the strict inner-endpoint order required by the already-proved nesting geometry.

theorem LeanPool.Erdos132ConvexK3.erlv_majorant_arc_nesting_complete_of_at_vertex_closure (hClose : ErLVAtVertexExceptionalBranchesImpossible) : ErLVMajorantArcNestingComplete

Use-site branch closure therefore reaches the existing source-facing arc-nesting interface.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.sqDist_le_terminal {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (path : K3CoverSequence P i j leftMoves rightMoves) : sqDist (P i) (P j) ≤ sqDist (P (cyclicRetreat i leftMoves)) (P (cyclicAdvance j rightMoves))

Every cover sequence weakly increases squared distance from its starting edge to its terminal edge.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.sqDist_lt_terminal_of_positive {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (path : K3CoverSequence P i j leftMoves rightMoves) (hpositive : 0 < leftMoves + rightMoves) : sqDist (P i) (P j) < sqDist (P (cyclicRetreat i leftMoves)) (P (cyclicAdvance j rightMoves))

A nonempty cover sequence strictly increases squared distance.

theorem LeanPool.Erdos132ConvexK3.K3MajorantWitness.terminal_rank_top_two_of_positive {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) (W : K3MajorantWitness P d₁ d₂ d₃ i j) (hpositive : 0 < W.leftMoves + W.rightMoves) : sqDist (P (cyclicRetreat i W.leftMoves)) (P (cyclicAdvance j W.rightMoves)) = d₁ ∨ sqDist (P (cyclicRetreat i W.leftMoves)) (P (cyclicAdvance j W.rightMoves)) = d₂

A positive-length majorant path cannot terminate in the smallest of the three graph ranks. Its terminal edge is d₁ or d₂, but one move alone does not determine which.

theorem LeanPool.Erdos132ConvexK3.ErLVAtVertexUseSite.first_start_adjacent {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) : TopThreeAdjacent P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ S.x) S.x

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

theorem LeanPool.Erdos132ConvexK3.erlv_case12_shared_tip_rank_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (h12 : S.Case12) : 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 (cyclicRetreat z S.pair.first.leftMoves)) (P (cyclicAdvance S.x 1)) = d₁ ∨ sqDist (P (cyclicRetreat z S.pair.first.leftMoves)) (P (cyclicAdvance S.x 1)) = d₂) ∧ sqDist (P (cyclicAdvance S.x 2)) (P u) = d₂

Exact shared-tip data in case (1,2). The second chain supplies a d₂ rung at x+2 and a d₁ terminal at the common tip x+1. The other edge incident to that tip is only forced into d₁ ∨ d₂; its color is not fixed. Thus the rigid branch does not itself supply the claimed forced d₂+d₁ pair at the common vertex.

theorem LeanPool.Erdos132ConvexK3.erlv_case21_shared_tip_rank_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (h21 : S.Case21) : have z := firstClockwiseNeighbor P d₁ d₂ d₃ S.x; have u := firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance S.x 3); sqDist (P z) (P (cyclicAdvance S.x 2)) = d₁ ∧ (sqDist (P (cyclicAdvance S.x 2)) (P (cyclicAdvance u S.pair.second.rightMoves)) = d₁ ∨ sqDist (P (cyclicAdvance S.x 2)) (P (cyclicAdvance u S.pair.second.rightMoves)) = d₂) ∧ sqDist (P z) (P (cyclicAdvance S.x 1)) = d₂

Mirror shared-tip data in case (2,1). Again one incident terminal is d₁, while the other is only d₁ ∨ d₂; the forced d₂ rung is based at the adjacent vertex x+1, not at the common tip x+2.

theorem LeanPool.Erdos132ConvexK3.equal_d3_avoiding_edges_force_cross_top_two {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {a b c d : Fin n} (hquad : StrictConvexQuad (P a) (P b) (P c) (P d)) (hab : TopThreeAdjacent P d₁ d₂ d₃ a b) (hcd : TopThreeAdjacent P d₁ d₂ d₃ c d) (habRank : sqDist (P a) (P b) = d₃) (hcdRank : sqDist (P c) (P d) = d₃) : (sqDist (P a) (P c) = d₁ ∨ sqDist (P a) (P c) = d₂) ∨ sqDist (P b) (P d) = d₁ ∨ sqDist (P b) (P d) = d₂

Strict ED on two equal d₃ avoiding sides forces one cross edge into the top two classes, not merely into the top-three graph.

theorem LeanPool.Erdos132ConvexK3.erlv_case22_cross_top_two_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 t := cyclicAdvance S.x 3; have u := firstCounterclockwiseNeighbor P d₁ d₂ d₃ t; (sqDist (P z) (P t) = d₁ ∨ sqDist (P z) (P t) = d₂) ∨ sqDist (P S.x) (P u) = d₁ ∨ sqDist (P S.x) (P u) = d₂

Exact ED output in case (2,2): the inserted cross edge is d₁ ∨ d₂. The kernel does not force the d₂ color required to enter the terminal d₂-cage directly.

theorem LeanPool.Erdos132ConvexK3.erlv_exceptional_use_site_localization_short_arc {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (hExceptional : 3 ≤ S.pair.first.rightMoves + S.pair.second.leftMoves) (M : ℕ) (hM : M ≤ S.pair.second.rightMoves) : have D := erlvK3MaximalGapSetupOfMajorants S.pair.first S.pair.second ⋯ M hM; D.yzSides ≤ 5

Once an exceptional inner-count branch has the missing outer localization, its arithmetic is already in the direct short-arc branch. It does not produce one of the five exceptional rows.

theorem LeanPool.Erdos132ConvexK3.erlv_exceptional_use_site_localization_avoids_five_rows {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (S : ErLVAtVertexUseSite P d₁ d₂ d₃) (hExceptional : 3 ≤ S.pair.first.rightMoves + S.pair.second.leftMoves) (M : ℕ) (hM : M ≤ S.pair.second.rightMoves) : have D := erlvK3MaximalGapSetupOfMajorants S.pair.first S.pair.second ⋯ M hM; ¬IsExceptionalMajorantRow (↑D.first.leftMoves) (↑D.first.rightMoves) D.L ↑D.M

Kernel check against the five-row enumeration: after outer localization, none of the rigid (1,2)/(2,1)/(2,2) inner-count cases realizes a table row. The two partitions concern different variables.

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase12OtherD1Impossible : Prop

The two exact color subcases left at the shared tip in (1,2).

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase12OtherD2Impossible : Prop

The remaining d₂ terminal color is impossible in the (1,2) branch.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case12_impossible_of_terminal_colors (hD1 : ErLVAtVertexCase12OtherD1Impossible) (hD2 : ErLVAtVertexCase12OtherD2Impossible) : ErLVAtVertexCase12Impossible

Closing both actual terminal colors would close the (1,2) branch.

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase21OtherD1Impossible : Prop

The mirror terminal-color split left at the shared tip in (2,1).

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase21OtherD2Impossible : Prop

The remaining d₂ terminal color is impossible in the (2,1) branch.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case21_impossible_of_terminal_colors (hD1 : ErLVAtVertexCase21OtherD1Impossible) (hD2 : ErLVAtVertexCase21OtherD2Impossible) : ErLVAtVertexCase21Impossible

Closing both actual terminal colors would close the (2,1) branch.

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase22ZTD1Impossible : Prop

Four exact top-two cross-color subcases left in (2,2). The d₂ subcases are the only ones even color-compatible with the terminal d₂ cage; the d₁ subcases require a different full-two-rung adapter.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase22ZTD2Impossible : Prop

The zt = d₂ cross-color subcase is impossible in the (2,2) branch.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase22XUD1Impossible : Prop

The xu = d₁ cross-color subcase is impossible in the (2,2) branch.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVAtVertexCase22XUD2Impossible : Prop

The xu = d₂ cross-color subcase is impossible in the (2,2) branch.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_case22_impossible_of_cross_colors (hZTD1 : ErLVAtVertexCase22ZTD1Impossible) (hZTD2 : ErLVAtVertexCase22ZTD2Impossible) (hXUD1 : ErLVAtVertexCase22XUD1Impossible) (hXUD2 : ErLVAtVertexCase22XUD2Impossible) : ErLVAtVertexCase22Impossible

The strengthened ED theorem reduces (2,2) exactly to the four named cross-edge/color obligations.

theorem LeanPool.Erdos132ConvexK3.erlv_at_vertex_exceptional_branches_impossible_of_color_cases (h12D1 : ErLVAtVertexCase12OtherD1Impossible) (h12D2 : ErLVAtVertexCase12OtherD2Impossible) (h21D1 : ErLVAtVertexCase21OtherD1Impossible) (h21D2 : ErLVAtVertexCase21OtherD2Impossible) (h22ZTD1 : ErLVAtVertexCase22ZTD1Impossible) (h22ZTD2 : ErLVAtVertexCase22ZTD2Impossible) (h22XUD1 : ErLVAtVertexCase22XUD1Impossible) (h22XUD2 : ErLVAtVertexCase22XUD2Impossible) : ErLVAtVertexExceptionalBranchesImpossible

The exact remaining use-site boundary after the rigid branch analysis: two terminal colors in each shared-tip branch and four cross-edge/color possibilities in the (2,2) branch. Discharging these eight propositions is sufficient for the at-the-vertex replacement of the abstract exchange.

theorem LeanPool.Erdos132ConvexK3.erlv_majorant_arc_nesting_complete_of_at_vertex_color_cases (h12D1 : ErLVAtVertexCase12OtherD1Impossible) (h12D2 : ErLVAtVertexCase12OtherD2Impossible) (h21D1 : ErLVAtVertexCase21OtherD1Impossible) (h21D2 : ErLVAtVertexCase21OtherD2Impossible) (h22ZTD1 : ErLVAtVertexCase22ZTD1Impossible) (h22ZTD2 : ErLVAtVertexCase22ZTD2Impossible) (h22XUD1 : ErLVAtVertexCase22XUD1Impossible) (h22XUD2 : ErLVAtVertexCase22XUD2Impossible) : ErLVMajorantArcNestingComplete

The same exact eight-subcase boundary, connected all the way to the source-facing nesting interface used by the global reduction.