Global ErLV reduction interface

This file starts the missing global bridge in draft Section 3. It fixes the cyclic notions used by the Erdos--Lovasz--Vesztergombi maximal-gap choice and states cover moves with squared distances, whose strict order agrees with the underlying Euclidean distances.

The primary-source convention is oriented: for an edge ij, a left cover retreats i by one polygon side and a right cover advances j by one side. The number of such moves is therefore exactly the side-count convention used by K3Majorant.leftMoves/rightMoves.

def LeanPool.Erdos132ConvexK3.cyclicAdvance {n : ℕ} [NeZero n] (i : Fin n) (k : ℕ) : Fin n

Advance by k polygon sides in the fixed cyclic labelling.

Equations

• LeanPool.Erdos132ConvexK3.cyclicAdvance i k = i + Fin.ofNat n k

def LeanPool.Erdos132ConvexK3.cyclicRetreat {n : ℕ} [NeZero n] (i : Fin n) (k : ℕ) : Fin n

Retreat by k polygon sides in the fixed cyclic labelling.

Equations

• LeanPool.Erdos132ConvexK3.cyclicRetreat i k = i - Fin.ofNat n k

@[simp]

theorem LeanPool.Erdos132ConvexK3.cyclicAdvance_zero {n : ℕ} [NeZero n] (i : Fin n) : cyclicAdvance i 0 = i

@[simp]

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_zero {n : ℕ} [NeZero n] (i : Fin n) : cyclicRetreat i 0 = i

theorem LeanPool.Erdos132ConvexK3.cyclicAdvance_add {n : ℕ} [NeZero n] (i : Fin n) (a b : ℕ) : cyclicAdvance (cyclicAdvance i a) b = cyclicAdvance i (a + b)

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_add {n : ℕ} [NeZero n] (i : Fin n) (a b : ℕ) : cyclicRetreat (cyclicRetreat i a) b = cyclicRetreat i (a + b)

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

Nonzero counterclockwise offsets from v that lead to a neighbor in G(S,3). The order on Fin n is the order of representatives 0,1,...,n-1, so its minimum is the first counterclockwise neighbor.

Equations

• LeanPool.Erdos132ConvexK3.ccwNeighborOffsets P d₁ d₂ d₃ v = {k : Fin n | k ≠ 0 ∧ LeanPool.Erdos132ConvexK3.TopThreeAdjacent P d₁ d₂ d₃ v (LeanPool.Erdos132ConvexK3.cyclicAdvance v ↑k)}

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

Nonzero clockwise offsets from v that lead to a graph neighbor.

Equations

• LeanPool.Erdos132ConvexK3.cwNeighborOffsets P d₁ d₂ d₃ v = {k : Fin n | k ≠ 0 ∧ LeanPool.Erdos132ConvexK3.TopThreeAdjacent P d₁ d₂ d₃ v (LeanPool.Erdos132ConvexK3.cyclicRetreat v ↑k)}

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

First counterclockwise neighbor offset; zero is the explicit sentinel when the vertex is isolated.

Equations

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

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

First clockwise neighbor offset, with zero as the isolated sentinel.

Equations

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

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

The first-neighbor gap g(v), measured in polygon sides.

Equations

• LeanPool.Erdos132ConvexK3.firstNeighborGap P d₁ d₂ d₃ v = ↑(LeanPool.Erdos132ConvexK3.firstNeighborOffset P d₁ d₂ d₃ v)

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

First counterclockwise graph neighbor, with the vertex itself as the isolated-vertex sentinel.

Equations

• LeanPool.Erdos132ConvexK3.firstCounterclockwiseNeighbor P d₁ d₂ d₃ v = LeanPool.Erdos132ConvexK3.cyclicAdvance v (LeanPool.Erdos132ConvexK3.firstNeighborGap P d₁ d₂ d₃ v)

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

First clockwise graph neighbor, with the vertex itself as the isolated-vertex sentinel.

Equations

• LeanPool.Erdos132ConvexK3.firstClockwiseNeighbor P d₁ d₂ d₃ v = LeanPool.Erdos132ConvexK3.cyclicRetreat v ↑(LeanPool.Erdos132ConvexK3.firstClockwiseNeighborOffset P d₁ d₂ d₃ v)

theorem LeanPool.Erdos132ConvexK3.top_three_adjacent_of_strictly_longer {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j p q : Fin n} (hij : TopThreeAdjacent P d₁ d₂ d₃ i j) (hgrow : sqDist (P i) (P j) < sqDist (P p) (P q)) : TopThreeAdjacent P d₁ d₂ d₃ p q

Strictly increasing a top-three edge produces another top-three edge. This is the rank fact behind termination of the primary-source cover process.

theorem LeanPool.Erdos132ConvexK3.topThreeAdjacent_symm {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {i j : Fin n} (h : TopThreeAdjacent P d₁ d₂ d₃ i j) : TopThreeAdjacent P d₁ d₂ d₃ j i

theorem LeanPool.Erdos132ConvexK3.ccwNeighborOffsets_nonempty_of_degree_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) : (ccwNeighborOffsets P d₁ d₂ d₃ v).Nonempty

Positive degree makes the first-neighbor offset set nonempty.

theorem LeanPool.Erdos132ConvexK3.cwNeighborOffsets_nonempty_of_degree_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) : (cwNeighborOffsets P d₁ d₂ d₃ v).Nonempty

theorem LeanPool.Erdos132ConvexK3.firstNeighborOffset_mem {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (h : (ccwNeighborOffsets P d₁ d₂ d₃ v).Nonempty) : firstNeighborOffset P d₁ d₂ d₃ v ∈ ccwNeighborOffsets P d₁ d₂ d₃ v

With a nonempty neighbor-offset set, the selected offset is one of its members and therefore is the genuine first counterclockwise graph neighbor.

theorem LeanPool.Erdos132ConvexK3.firstClockwiseNeighborOffset_mem {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (h : (cwNeighborOffsets P d₁ d₂ d₃ v).Nonempty) : firstClockwiseNeighborOffset P d₁ d₂ d₃ v ∈ cwNeighborOffsets P d₁ d₂ d₃ v

theorem LeanPool.Erdos132ConvexK3.firstNeighborOffset_spec_of_degree_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) : firstNeighborOffset P d₁ d₂ d₃ v ≠ 0 ∧ TopThreeAdjacent P d₁ d₂ d₃ v (cyclicAdvance v (firstNeighborGap P d₁ d₂ d₃ v))

Positive degree gives a nonzero first-neighbor gap and an actual graph neighbor at that cyclic offset.

theorem LeanPool.Erdos132ConvexK3.firstCounterclockwiseNeighbor_adjacent_of_degree_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) : TopThreeAdjacent P d₁ d₂ d₃ v (firstCounterclockwiseNeighbor P d₁ d₂ d₃ v)

theorem LeanPool.Erdos132ConvexK3.firstClockwiseNeighbor_adjacent_of_degree_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 0 < vertexDegree P d₁ d₂ d₃ v) : TopThreeAdjacent P d₁ d₂ d₃ v (firstClockwiseNeighbor P d₁ d₂ d₃ v)

theorem LeanPool.Erdos132ConvexK3.exists_maximal_firstNeighborGap {n : ℕ} [NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) : ∃ (x : Fin n), ∀ (v : Fin n), firstNeighborGap P d₁ d₂ d₃ v ≤ firstNeighborGap P d₁ d₂ d₃ x

Every finite cyclic configuration admits a vertex maximizing the chosen first-neighbor gap (including the isolated-vertex sentinel convention).

def LeanPool.Erdos132ConvexK3.IsLeftCover {K : Type u_1} [Ring K] [LT K] {n : ℕ} [NeZero n] (P : Fin n → Point K) (i j : Fin n) : Prop

A primary-source left cover of the oriented edge ij: retreating the left endpoint by one side strictly increases the squared distance.

Equations

• LeanPool.Erdos132ConvexK3.IsLeftCover P i j = (LeanPool.Erdos132ConvexK3.sqDist (P i) (P j) < LeanPool.Erdos132ConvexK3.sqDist (P (LeanPool.Erdos132ConvexK3.cyclicRetreat i 1)) (P j))

def LeanPool.Erdos132ConvexK3.IsRightCover {K : Type u_1} [Ring K] [LT K] {n : ℕ} [NeZero n] (P : Fin n → Point K) (i j : Fin n) : Prop

A primary-source right cover of the oriented edge ij: advancing the right endpoint by one side strictly increases the squared distance.

Equations

• LeanPool.Erdos132ConvexK3.IsRightCover P i j = (LeanPool.Erdos132ConvexK3.sqDist (P i) (P j) < LeanPool.Erdos132ConvexK3.sqDist (P i) (P (LeanPool.Erdos132ConvexK3.cyclicAdvance j 1)))

def LeanPool.Erdos132ConvexK3.IsMajorant {K : Type u_1} [Ring K] [LT K] {n : ℕ} [NeZero n] (P : Fin n → Point K) (i j : Fin n) : Prop

An oriented edge is a majorant when neither legal endpoint cover raises its distance.

Equations

• LeanPool.Erdos132ConvexK3.IsMajorant P i j = (¬LeanPool.Erdos132ConvexK3.IsLeftCover P i j ∧ ¬LeanPool.Erdos132ConvexK3.IsRightCover P i j)

inductive LeanPool.Erdos132ConvexK3.K3CoverSequence {n : ℕ} [NeZero n] (P : Fin n → Point ℝ) : Fin n → Fin n → ℕ → ℕ → Prop

An actual sequence of strict ErLV cover moves. The indices count moves at the left and right endpoints; their order is retained by the proof tree. This prevents a terminal edge with compatible endpoint counts from being mistaken for a majorant reached from the stated starting edge.

• nil {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (i j : Fin n) : K3CoverSequence P i j 0 0
• left {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (hCover : IsLeftCover P i j) (tail : K3CoverSequence P (cyclicRetreat i 1) j leftMoves rightMoves) : K3CoverSequence P i j (leftMoves + 1) rightMoves
• right {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (hCover : IsRightCover P i j) (tail : K3CoverSequence P i (cyclicAdvance j 1) leftMoves rightMoves) : K3CoverSequence P i j leftMoves (rightMoves + 1)

theorem LeanPool.Erdos132ConvexK3.heptagon_nondiameter_edge_is_majorant : CyclicStrictConvex Witnesses.heptagon ∧ HasTopThreeDistanceClasses Witnesses.heptagon 7225 6649 5353 ∧ sqDist (Witnesses.heptagon 0) (Witnesses.heptagon 5) = 6649 ∧ 6649 ≠ 7225 ∧ IsMajorant Witnesses.heptagon 0 5

Kernel counterexample to the stronger but non-source claim that every non-diameter top-three edge admits a cover. In the exact attempt-2 heptagon, the d₂ edge (0,5) is already a majorant: both permitted endpoint moves strictly shorten it. ErLV majorant existence therefore uses finite rank ascent with a terminal case; it does not use such a universal extension lemma.

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

Endpoint counts and terminal edge produced by the cover process.

• leftMoves : ℕ

  Number of cover moves made at the left endpoint.

• rightMoves : ℕ

  Number of cover moves made at the right endpoint.

• coverBudget : self.leftMoves + self.rightMoves ≤ 2
• path : K3CoverSequence P i j self.leftMoves self.rightMoves
• adjacent : TopThreeAdjacent P d₁ d₂ d₃ (cyclicRetreat i self.leftMoves) (cyclicAdvance j self.rightMoves)
• terminal : IsMajorant P (cyclicRetreat i self.leftMoves) (cyclicAdvance j self.rightMoves)

theorem LeanPool.Erdos132ConvexK3.left_cover_top_three_adjacent {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j : Fin n} (hAdj : TopThreeAdjacent P d₁ d₂ d₃ i j) (hCover : IsLeftCover P i j) : TopThreeAdjacent P d₁ d₂ d₃ (cyclicRetreat i 1) j

A left cover preserves membership in the top-three graph.

theorem LeanPool.Erdos132ConvexK3.right_cover_top_three_adjacent {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j : Fin n} (hAdj : TopThreeAdjacent P d₁ d₂ d₃ i j) (hCover : IsRightCover P i j) : TopThreeAdjacent P d₁ d₂ d₃ i (cyclicAdvance j 1)

A right cover preserves membership in the top-three graph.

theorem LeanPool.Erdos132ConvexK3.two_covers_end_at_d₁ {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i₀ j₀ i₁ j₁ i₂ j₂ : Fin n} (h₀ : TopThreeAdjacent P d₁ d₂ d₃ i₀ j₀) (h₁ : TopThreeAdjacent P d₁ d₂ d₃ i₁ j₁) (h₂ : TopThreeAdjacent P d₁ d₂ d₃ i₂ j₂) (hgrow₁ : sqDist (P i₀) (P j₀) < sqDist (P i₁) (P j₁)) (hgrow₂ : sqDist (P i₁) (P j₁) < sqDist (P i₂) (P j₂)) : sqDist (P i₂) (P j₂) = d₁

Two strict cover moves among exactly three distance ranks must end in the largest class.

theorem LeanPool.Erdos132ConvexK3.d₁_edge_is_majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j : Fin n} (hAdj : TopThreeAdjacent P d₁ d₂ d₃ i j) (hd₁ : sqDist (P i) (P j) = d₁) : IsMajorant P i j

A diameter-class edge is terminal for the cover process because every interpoint squared distance is at most d₁.

theorem LeanPool.Erdos132ConvexK3.left_or_right_cover_of_not_majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (h : ¬IsMajorant P i j) : IsLeftCover P i j ∨ IsRightCover P i j

theorem LeanPool.Erdos132ConvexK3.exists_k3_majorant {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) : Nonempty (K3MajorantWitness P d₁ d₂ d₃ i j)

Primary-source majorant existence for G(S,3): strict covers stay in the top-three graph and at most two such rank raises are possible.

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

A jointly selected pair of actual majorant paths. The objective is the number of moves made by the two facing endpoints in ErLV Figure 4.

• first : K3MajorantWitness P d₁ d₂ d₃ z x

  Majorant path starting from the first oriented edge zx.

• second : K3MajorantWitness P d₁ d₂ d₃ t u

  Majorant path starting from the second oriented edge tu.

• minimalInnerMoves (first' : K3MajorantWitness P d₁ d₂ d₃ z x) (second' : K3MajorantWitness P d₁ d₂ d₃ t u) : self.first.rightMoves + self.second.leftMoves ≤ first'.rightMoves + second'.leftMoves

theorem LeanPool.Erdos132ConvexK3.exists_coordinated_k3_majorant_pair {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {z x t u : Fin n} (hFirst : Nonempty (K3MajorantWitness P d₁ d₂ d₃ z x)) (hSecond : Nonempty (K3MajorantWitness P d₁ d₂ d₃ t u)) : Nonempty (CoordinatedK3MajorantPair P d₁ d₂ d₃ z x t u)

The nonempty Cartesian pool of actual majorant paths has a pair minimizing the total number of moves at the two facing endpoints.

theorem LeanPool.Erdos132ConvexK3.all_degrees_at_least_seven_of_no_degree_six {n : ℕ} [_nonzero : NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hNoLow : ¬∃ (v : Fin n), vertexDegree P d₁ d₂ d₃ v ≤ 6) (v : Fin n) : 7 ≤ vertexDegree P d₁ d₂ d₃ v

If no degree-six vertex exists, every vertex has degree at least seven.

theorem LeanPool.Erdos132ConvexK3.exists_maximal_gap_two_majorants {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hHigh : ∀ (v : Fin n), 7 ≤ vertexDegree P d₁ d₂ d₃ v) : ∃ (x : Fin n), (∀ (v : Fin n), firstNeighborGap P d₁ d₂ d₃ v ≤ firstNeighborGap P d₁ d₂ d₃ x) ∧ Nonempty (K3MajorantWitness P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ x) x) ∧ Nonempty (K3MajorantWitness P d₁ d₂ d₃ (cyclicAdvance x 3) (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3)))

In the high-minimum-degree branch, a maximal-gap vertex and both primary-source majorants exist. The first witness is oriented z ⟶ x, so its endpoint counts are reversed when compared with the draft's (a,b) convention.

theorem LeanPool.Erdos132ConvexK3.exists_maximal_gap_coordinated_majorants {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hHigh : ∀ (v : Fin n), 7 ≤ vertexDegree P d₁ d₂ d₃ v) : ∃ (x : Fin n), (∀ (v : Fin n), firstNeighborGap P d₁ d₂ d₃ v ≤ firstNeighborGap P d₁ d₂ d₃ x) ∧ Nonempty (CoordinatedK3MajorantPair P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ x) x (cyclicAdvance x 3) (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3)))

The high-minimum-degree branch admits a maximal-gap vertex together with a jointly minimal pair of actual cover paths.

def LeanPool.Erdos132ConvexK3.K3MajorantWitness.toK3Majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {i j : Fin n} (W : K3MajorantWitness P d₁ d₂ d₃ i j) : K3Majorant

Convert a witness without changing endpoint orientation.

Equations

• W.toK3Majorant = { leftMoves := W.leftMoves, rightMoves := W.rightMoves, coverBudget := ⋯ }

def LeanPool.Erdos132ConvexK3.K3MajorantWitness.toFirstK3Majorant {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {i j : Fin n} (W : K3MajorantWitness P d₁ d₂ d₃ i j) : K3Majorant

Convert the first source majorant z ⟶ x to the draft convention: a counts moves at x, while b counts moves at z.

Equations

• W.toFirstK3Majorant = { leftMoves := W.rightMoves, rightMoves := W.leftMoves, coverBudget := ⋯ }

noncomputable def LeanPool.Erdos132ConvexK3.erlvK3MaximalGapSetupOfMajorants {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {x z t u : Fin n} (first : K3MajorantWitness P d₁ d₂ d₃ z x) (second : K3MajorantWitness P d₁ d₂ d₃ t u) (hgap : firstNeighborGap P d₁ d₂ d₃ t ≤ firstNeighborGap P d₁ d₂ d₃ x) (M : ℕ) (hM : M ≤ second.rightMoves) : ErLVK3MaximalGapSetup

Build the arithmetic record once the source's arc-nesting conclusion s = u+M, M≤β has been supplied.

Equations

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

def LeanPool.Erdos132ConvexK3.ErLVMajorantArcNestingComplete : Prop

Exact first unresolved source fact. If x maximizes the first-neighbor gap, z is its first clockwise neighbor, t=x+3, and u is the first counterclockwise neighbor of t, then a jointly minimal pair of actual majorant paths can be chosen so that the terminal endpoint s of the majorant of zx lies on the arc from u to the terminal endpoint s' of the majorant of tu. In side-count form this is precisely s = cyclicAdvance u M for some M≤β.

The acute-angle/nonavoiding-majorants implication is proved in MajorantArcNesting.lean. What remains is ErLV's undisplayed strict order of the two inner majorant endpoints: under the draft's side-count convention it is first.rightMoves + second.leftMoves < 3.

Equations

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