Coordinated ErLV majorants

This file makes the proposed repair to ErLV's Figure 4 precise. Majorant witnesses carry actual strict-cover paths, and the two paths are selected jointly to minimize the moves made by their facing endpoints. The finite minimum exists. The remaining exchange statement is isolated exactly.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.left_left_of_counts {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (path : K3CoverSequence P i j 2 0) : IsLeftCover P i j ∧ IsLeftCover P (cyclicRetreat i 1) j

A two-left-move path really contains the two successive strict covers.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.right_right_of_counts {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (path : K3CoverSequence P i j 0 2) : IsRightCover P i j ∧ IsRightCover P i (cyclicAdvance j 1)

A two-right-move path really contains the two successive strict covers.

theorem LeanPool.Erdos132ConvexK3.coordinated_inner_endpoint_budget_partition {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x t u : Fin n} (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ z x t u) : pair.first.rightMoves + pair.second.leftMoves < 3 ∨ pair.first.rightMoves = 1 ∧ pair.second.leftMoves = 2 ∨ pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 1 ∨ pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2

The jointly minimal pair has the same exhaustive inner-count partition as any pair, but now every branch refers to actual cover paths.

theorem LeanPool.Erdos132ConvexK3.coordinated_exceptional_count_rigidity {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x t u : Fin n} (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ z x t u) (hExceptional : 3 ≤ pair.first.rightMoves + pair.second.leftMoves) : ((pair.first.rightMoves = 1 ∧ pair.second.leftMoves = 2) ∧ (∀ (first' : K3MajorantWitness P d₁ d₂ d₃ z x), 1 ≤ first'.rightMoves) ∧ ∀ (second' : K3MajorantWitness P d₁ d₂ d₃ t u), second'.leftMoves = 2 ∧ second'.rightMoves = 0) ∨ ((pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 1) ∧ (∀ (first' : K3MajorantWitness P d₁ d₂ d₃ z x), first'.rightMoves = 2 ∧ first'.leftMoves = 0) ∧ ∀ (second' : K3MajorantWitness P d₁ d₂ d₃ t u), 1 ≤ second'.leftMoves) ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2) ∧ (∀ (first' : K3MajorantWitness P d₁ d₂ d₃ z x), first'.rightMoves = 2 ∧ first'.leftMoves = 0) ∧ ∀ (second' : K3MajorantWitness P d₁ d₂ d₃ t u), second'.leftMoves = 2 ∧ second'.rightMoves = 0

If a jointly minimal pair is exceptional, minimality rigidifies all possible substitutes in its Cartesian pool. This is the exact obstruction to a purely order-theoretic minimization proof.

theorem LeanPool.Erdos132ConvexK3.coordinated_exceptional_forced_paths {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x t u : Fin n} (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ z x t u) (hExceptional : 3 ≤ pair.first.rightMoves + pair.second.leftMoves) : (pair.first.rightMoves = 1 ∧ pair.second.leftMoves = 2) ∧ IsLeftCover P t u ∧ IsLeftCover P (cyclicRetreat t 1) u ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 1) ∧ IsRightCover P z x ∧ IsRightCover P z (cyclicAdvance x 1) ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2) ∧ IsRightCover P z x ∧ IsRightCover P z (cyclicAdvance x 1) ∧ IsLeftCover P t u ∧ IsLeftCover P (cyclicRetreat t 1) u

The selected exceptional cases contain the forced two-move paths that a geometric exchange proof would have to replace.

theorem LeanPool.Erdos132ConvexK3.coordinated_exceptional_inner_endpoints {n : ℕ} [NeZero n] (hn : 4 ≤ n) {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x u : Fin n} (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ z x (cyclicAdvance x 3) u) (hExceptional : 3 ≤ pair.first.rightMoves + pair.second.leftMoves) : (pair.first.rightMoves = 1 ∧ pair.second.leftMoves = 2) ∧ cyclicAdvance x pair.first.rightMoves = cyclicRetreat (cyclicAdvance x 3) pair.second.leftMoves ∧ cyclicAdvance x pair.first.rightMoves = cyclicAdvance x 1 ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 1) ∧ cyclicAdvance x pair.first.rightMoves = cyclicRetreat (cyclicAdvance x 3) pair.second.leftMoves ∧ cyclicAdvance x pair.first.rightMoves = cyclicAdvance x 2 ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2) ∧ cyclicAdvance x pair.first.rightMoves = cyclicAdvance x 2 ∧ cyclicRetreat (cyclicAdvance x 3) pair.second.leftMoves = cyclicAdvance x 1

The three exceptional pairs have exactly the endpoint geometry hidden by ErLV Figure 4: the inner endpoints coincide in (1,2) and (2,1), while they occur in the reverse order in (2,2). Thus terminal-majorant nonavoidance is automatic in these branches and supplies no nesting.

theorem LeanPool.Erdos132ConvexK3.right_right_cover_rank_ladder {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 0 2) : sqDist (P i) (P j) = d₃ ∧ sqDist (P i) (P (cyclicAdvance j 1)) = d₂ ∧ sqDist (P i) (P (cyclicAdvance j 2)) = d₁

Two successive right covers exhaust the three ranks exactly.

theorem LeanPool.Erdos132ConvexK3.left_left_cover_rank_ladder {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 2 0) : sqDist (P i) (P j) = d₃ ∧ sqDist (P (cyclicRetreat i 1)) (P j) = d₂ ∧ sqDist (P (cyclicRetreat i 2)) (P j) = d₁

Two successive left covers exhaust the three ranks exactly.

theorem LeanPool.Erdos132ConvexK3.right_right_intermediate_not_majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (path : K3CoverSequence P i j 0 2) : ¬IsMajorant P i (cyclicAdvance j 1)

The intermediate edge of a forced two-right-move chain is not a majorant: the second move is still a strict right cover. Thus this edge cannot be the cheaper terminal substitute suggested by an informal exchange argument.

theorem LeanPool.Erdos132ConvexK3.left_left_intermediate_not_majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (path : K3CoverSequence P i j 2 0) : ¬IsMajorant P (cyclicRetreat i 1) j

The intermediate edge of a forced two-left-move chain is not a majorant: the second move is still a strict left cover.

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_ne_of_lt {n : ℕ} [NeZero n] (i : Fin n) {a b : ℕ} (ha : a < n) (hb : b < n) (hab : a ≠ b) : cyclicRetreat i a ≠ cyclicRetreat i b

Retreats by two distinct offsets below the polygon size have distinct endpoints.

theorem LeanPool.Erdos132ConvexK3.three_side_cross_edges_outside_majorant_budget {n : ℕ} [NeZero n] (hn : 4 ≤ n) {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x u : Fin n} (first : K3MajorantWitness P d₁ d₂ d₃ z x) (second : K3MajorantWitness P d₁ d₂ d₃ (cyclicAdvance x 3) u) : cyclicAdvance x first.rightMoves ≠ cyclicAdvance x 3 ∧ cyclicRetreat (cyclicAdvance x 3) second.leftMoves ≠ x

A k=3 majorant witness has at most two moves in total, so its inner endpoint cannot be the vertex three sides away. Consequently the two cross edges forced by strict ED in case (2,2) are not terminal edges of either original cover process.

theorem LeanPool.Erdos132ConvexK3.coordinated_exceptional_rank_and_exchange_obstruction {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {z x t u : Fin n} (hFirstStart : TopThreeAdjacent P d₁ d₂ d₃ z x) (hSecondStart : TopThreeAdjacent P d₁ d₂ d₃ t u) (pair : CoordinatedK3MajorantPair P d₁ d₂ d₃ z x t u) (hExceptional : 3 ≤ pair.first.rightMoves + pair.second.leftMoves) : (pair.first.rightMoves = 1 ∧ pair.second.leftMoves = 2) ∧ sqDist (P t) (P u) = d₃ ∧ sqDist (P (cyclicRetreat t 1)) (P u) = d₂ ∧ sqDist (P (cyclicRetreat t 2)) (P u) = d₁ ∧ ¬IsMajorant P (cyclicRetreat t 1) u ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 1) ∧ sqDist (P z) (P x) = d₃ ∧ sqDist (P z) (P (cyclicAdvance x 1)) = d₂ ∧ sqDist (P z) (P (cyclicAdvance x 2)) = d₁ ∧ ¬IsMajorant P z (cyclicAdvance x 1) ∨ (pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2) ∧ sqDist (P z) (P x) = d₃ ∧ sqDist (P z) (P (cyclicAdvance x 1)) = d₂ ∧ sqDist (P z) (P (cyclicAdvance x 2)) = d₁ ∧ sqDist (P t) (P u) = d₃ ∧ sqDist (P (cyclicRetreat t 1)) (P u) = d₂ ∧ sqDist (P (cyclicRetreat t 2)) (P u) = d₁ ∧ ¬IsMajorant P z (cyclicAdvance x 1) ∧ ¬IsMajorant P (cyclicRetreat t 1) u

Exact kernel boundary in the three exceptional coordinated cases. Each forced two-move chain has the only possible rank ladder d₃ → d₂ → d₁, while its named intermediate exchange edge is still covered and therefore is not a majorant. In (2,2) both failures occur simultaneously.

This theorem does not claim that a full minimum-degree-seven configuration realizing one of the cases exists. It records exactly why the local swap proposed after the rigidification does not produce the cheaper pair required by ErLVCoordinatedMajorantExchangeComplete.

theorem LeanPool.Erdos132ConvexK3.equal_avoiding_edges_force_cross_top_three {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) (hEqual : sqDist (P a) (P b) = sqDist (P c) (P d)) : TopThreeAdjacent P d₁ d₂ d₃ a c ∨ TopThreeAdjacent P d₁ d₂ d₃ b d

Strict ED does produce a cross top-three edge from two equal avoiding sides. It does not say that this diagonal is an immediate endpoint cover, which is precisely why it does not by itself furnish the required exchange path.

theorem LeanPool.Erdos132ConvexK3.erlv_start_edges_strict_convex_quad {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (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) : StrictConvexQuad (P (cyclicAdvance x 3)) (P (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3))) (P (firstClockwiseNeighbor P d₁ d₂ d₃ x)) (P x)

In the maximal-gap setup the two starting edges tu and zx occur as opposite sides of the strict convex quadrilateral t,u,z,x. This is the exact cyclic order needed to instantiate strict ED in the rigid (2,2) branch.

theorem LeanPool.Erdos132ConvexK3.coordinated_exceptional_22_forces_cross_top_three {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))) (h22 : pair.first.rightMoves = 2 ∧ pair.second.leftMoves = 2) : TopThreeAdjacent P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ x) (cyclicAdvance x 3) ∨ TopThreeAdjacent P d₁ d₂ d₃ x (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3))

In the rigid (2,2) case, strict ED is fully exhausted: the two equal d₃ starting sides force one of the nonlocal cross edges zt or xu into the top-three graph. These cross edges move an inner endpoint by three polygon sides; the theorem deliberately does not misidentify either one as an immediate cover in a two-move majorant path.

def LeanPool.Erdos132ConvexK3.ErLVCoordinatedMajorantExchangeComplete : Prop

Exact exchange claim missing from the printed proof: every exceptional joint minimum admits another actual pair with fewer facing-endpoint moves. Neither ErLV89 p.548 nor the 1986 preprint states a selection rule or proves this replacement.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_inner_endpoint_separation_complete_of_coordinated_exchange (hExchange : ErLVCoordinatedMajorantExchangeComplete) : ErLVInnerEndpointSeparationComplete

A proof of the missing exchange would discharge the coordinated strict inner order and hence the already-kernelized arc-nesting geometry.