Global convex k = 3 assembly

This file connects the raw convex/top-three hypotheses to the ErLV maximal-gap diagram. The unconditional terminal-color closure supplies the jointly selected majorants and their outer-endpoint localization. The first stage below packages that data and instantiates the five-row enumeration.

inductive LeanPool.Erdos132ConvexK3.K3CoverSequence.StartsLeft {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} : K3CoverSequence P i j leftMoves rightMoves → Prop

The first strict cover move acts at the left endpoint.

• intro {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (h : IsLeftCover P i j) (tail : K3CoverSequence P (cyclicRetreat i 1) j leftMoves rightMoves) : ⋯.StartsLeft

inductive LeanPool.Erdos132ConvexK3.K3CoverSequence.StartsRight {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} : K3CoverSequence P i j leftMoves rightMoves → Prop

The first strict cover move acts at the right endpoint.

• intro {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (h : IsRightCover P i j) (tail : K3CoverSequence P i (cyclicAdvance j 1) leftMoves rightMoves) : ⋯.StartsRight

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.startsLeft_or_startsRight_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) : path.StartsLeft ∨ path.StartsRight

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.startsLeft_of_left_positive_right_zero {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (path : K3CoverSequence P i j leftMoves rightMoves) (hleft : 0 < leftMoves) (hright : rightMoves = 0) : path.StartsLeft

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.startsRight_of_left_zero_right_positive {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (path : K3CoverSequence P i j leftMoves rightMoves) (hleft : leftMoves = 0) (hright : 0 < rightMoves) : path.StartsRight

theorem LeanPool.Erdos132ConvexK3.strict_top_three_rank_transition {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {i j p q : Fin n} (hStart : TopThreeAdjacent P d₁ d₂ d₃ i j) (hEnd : TopThreeAdjacent P d₁ d₂ d₃ p q) (hRaise : sqDist (P i) (P j) < sqDist (P p) (P q)) : sqDist (P i) (P j) = d₃ ∧ sqDist (P p) (P q) = d₂ ∨ sqDist (P i) (P j) = d₃ ∧ sqDist (P p) (P q) = d₁ ∨ sqDist (P i) (P j) = d₂ ∧ sqDist (P p) (P q) = d₁

A single strict rank increase between top-three edges has exactly one of the three transitions d₃→d₂, d₃→d₁, or d₂→d₁.

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

The geometric maximal-gap frame obtained in the high-minimum-degree branch, including the jointly minimal majorants and the now-proved outer endpoint localization.

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

  Vertex whose first-neighbor gap is maximal.

• 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 majorants anchored at the selected vertex.

• M : ℕ

  Outer localization offset along the second majorant.

• M_le_secondRight : self.M ≤ self.pair.second.rightMoves
• outerLocalized : cyclicRetreat (firstClockwiseNeighbor P d₁ d₂ d₃ self.x) self.pair.first.leftMoves = cyclicAdvance (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance self.x 3)) self.M

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

The global frame contains exactly the data required by the established degree-seven use-site lemmas.

Equations

• F.toUseSite = LeanPool.Erdos132ConvexK3.erlvAtVertexUseSiteOfHighDegree ⋯ ⋯ ⋯ F.x ⋯ F.pair

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

Forget the geometric labels while retaining the exact arithmetic data used by the five-row enumeration.

Equations

• F.setup = LeanPool.Erdos132ConvexK3.erlvK3MaximalGapSetupOfMajorants F.pair.first F.pair.second ⋯ F.M ⋯

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

First exceptional row of the five-row count table.

Equations

• F.Row1 = (F.pair.first.rightMoves = 0 ∧ F.pair.first.leftMoves = 1 ∧ F.setup.L = 3 ∧ F.M = 2)

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

Second exceptional row of the five-row count table.

Equations

• F.Row2 = (F.pair.first.rightMoves = 1 ∧ F.pair.first.leftMoves = 1 ∧ F.setup.L = 3 ∧ F.M = 2)

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

Third exceptional row of the five-row count table.

Equations

• F.Row3 = (F.pair.first.rightMoves = 0 ∧ F.pair.first.leftMoves = 2 ∧ F.setup.L = 2 ∧ F.M = 2)

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

Fourth exceptional row of the five-row count table.

Equations

• F.Row4 = (F.pair.first.rightMoves = 0 ∧ F.pair.first.leftMoves = 2 ∧ F.setup.L = 3 ∧ F.M = 1)

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

Fifth exceptional row of the five-row count table.

Equations

• F.Row5 = (F.pair.first.rightMoves = 0 ∧ F.pair.first.leftMoves = 2 ∧ F.setup.L = 3 ∧ F.M = 2)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.exceptional_row_iff_rows {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : IsExceptionalMajorantRow (↑F.setup.first.leftMoves) (↑F.setup.first.rightMoves) F.setup.L ↑F.setup.M ↔ F.Row1 ∨ F.Row2 ∨ F.Row3 ∨ F.Row4 ∨ F.Row5

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

Squared distance of the first majorant's starting edge.

Equations

• F.firstStartSqDist = LeanPool.Erdos132ConvexK3.sqDist (P (LeanPool.Erdos132ConvexK3.firstClockwiseNeighbor P d₁ d₂ d₃ F.x)) (P F.x)

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

Squared distance of the first majorant's terminal edge.

Equations

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

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

Squared distance of the second majorant's starting edge.

Equations

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

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

Squared distance of the second majorant's terminal edge.

Equations

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

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

The first majorant changes rank from d₃ to d₂.

Equations

• F.FirstRank32 = (F.firstStartSqDist = d₃ ∧ F.firstTerminalSqDist = d₂)

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

The first majorant changes rank from d₃ to d₁.

Equations

• F.FirstRank31 = (F.firstStartSqDist = d₃ ∧ F.firstTerminalSqDist = d₁)

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

The first majorant changes rank from d₂ to d₁.

Equations

• F.FirstRank21 = (F.firstStartSqDist = d₂ ∧ F.firstTerminalSqDist = d₁)

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

The second majorant changes rank from d₃ to d₂.

Equations

• F.SecondRank32 = (F.secondStartSqDist = d₃ ∧ F.secondTerminalSqDist = d₂)

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

The second majorant changes rank from d₃ to d₁.

Equations

• F.SecondRank31 = (F.secondStartSqDist = d₃ ∧ F.secondTerminalSqDist = d₁)

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

The second majorant changes rank from d₂ to d₁.

Equations

• F.SecondRank21 = (F.secondStartSqDist = d₂ ∧ F.secondTerminalSqDist = d₁)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.first_rank_transition_of_positive {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hpositive : 0 < F.pair.first.leftMoves + F.pair.first.rightMoves) : F.FirstRank32 ∨ F.FirstRank31 ∨ F.FirstRank21

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.second_rank_transition_of_positive {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hpositive : 0 < F.pair.second.leftMoves + F.pair.second.rightMoves) : F.SecondRank32 ∨ F.SecondRank31 ∨ F.SecondRank21

def LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.RealizesCoverWord {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : ExceptionalCoverWord → Prop

Geometric semantics of the thirteen cover words for one localized maximal-gap frame. The letters record the actual endpoint order (A/B for the first path and C/D for the second); the one-step words also retain the exact strict rank transition.

Equations

• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row1_B32 = (F.Row1 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight ∧ F.FirstRank32)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row1_B31 = (F.Row1 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight ∧ F.FirstRank31)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row1_B21 = (F.Row1 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight ∧ F.FirstRank21)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row2_AB = (F.Row2 ∧ ⋯.StartsRight ∧ ⋯.StartsRight)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row2_BA = (F.Row2 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row3_BB_DD = (F.Row3 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_D32 = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 0 ∧ F.pair.second.rightMoves = 1 ∧ ⋯.StartsRight ∧ F.SecondRank32)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_D31 = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 0 ∧ F.pair.second.rightMoves = 1 ∧ ⋯.StartsRight ∧ F.SecondRank31)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_D21 = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 0 ∧ F.pair.second.rightMoves = 1 ∧ ⋯.StartsRight ∧ F.SecondRank21)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_CD = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 1 ∧ F.pair.second.rightMoves = 1 ∧ ⋯.StartsLeft)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_DC = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 1 ∧ F.pair.second.rightMoves = 1 ∧ ⋯.StartsRight)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row4_DD = (F.Row4 ∧ ⋯.StartsLeft ∧ F.pair.second.leftMoves = 0 ∧ F.pair.second.rightMoves = 2 ∧ ⋯.StartsRight)
• F.RealizesCoverWord LeanPool.Erdos132ConvexK3.ExceptionalCoverWord.row5_BB_DD = (F.Row5 ∧ ⋯.StartsLeft ∧ ⋯.StartsRight)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.exceptional_row_realizes_cover_word {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hRow : IsExceptionalMajorantRow (↑F.setup.first.leftMoves) (↑F.setup.first.rightMoves) F.setup.L ↑F.setup.M) : ∃ (w : ExceptionalCoverWord), F.RealizesCoverWord w

Every actual exceptional row expands to one of exactly the thirteen cover words in the draft table.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.short_arc_or_exceptional_row {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : F.setup.yzSides ≤ 5 ∨ IsExceptionalMajorantRow (↑F.setup.first.leftMoves) (↑F.setup.first.rightMoves) F.setup.L ↑F.setup.M

The five-row arithmetic applies to every global frame: either the short-arc inequality already holds or one of the five exceptional rows is realized by the actual majorant counts.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.localized_offset_span_eq_yzSides {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : ↑(n - ↑(firstClockwiseNeighborOffset P d₁ d₂ d₃ F.x)) - ↑(firstNeighborGap P d₁ d₂ d₃ F.x) = F.setup.yzSides

The localized terminal endpoint turns the abstract signed quantity D.yzSides into the actual counterclockwise offset span from the first counterclockwise neighbor of x to its first clockwise neighbor.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.degree_le_six_of_short_arc {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hShort : F.setup.yzSides ≤ 5) : vertexDegree P d₁ d₂ d₃ F.x ≤ 6

The direct branch of the ErLV assembly. If the localized span between the first counterclockwise and first clockwise neighbors is at most five sides, the complete neighbor set of x has at most six vertices.

theorem LeanPool.Erdos132ConvexK3.exists_erlv_global_five_row_frame {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) : Nonempty (ErLVGlobalFiveRowFrame P d₁ d₂ d₃)

Raw convex/top-three data in the high-degree contradiction branch produces the complete localized maximal-gap frame.

theorem LeanPool.Erdos132ConvexK3.exists_erlv_global_short_arc_or_exceptional_row {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) : ∃ (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃), F.setup.yzSides ≤ 5 ∨ IsExceptionalMajorantRow (↑F.setup.first.leftMoves) (↑F.setup.first.rightMoves) F.setup.L ↑F.setup.M

Combined raw-data form of the maximal-gap choice, the two actual majorants, their localization, and the five-row enumeration.

theorem LeanPool.Erdos132ConvexK3.exists_erlv_global_exceptional_row_of_no_degree_six {n : ℕ} [NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hNoLow : ¬∃ (v : Fin n), vertexDegree P d₁ d₂ d₃ v ≤ 6) : ∃ (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃), IsExceptionalMajorantRow (↑F.setup.first.leftMoves) (↑F.setup.first.rightMoves) F.setup.L ↑F.setup.M

Once the direct short-arc branch is discharged, failure of the desired degree bound produces an actual localized frame in one of the five rows.

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

Canonical raw geometric meaning of a cover word: it is realized by an actual localized maximal-gap frame with the row, endpoint order, and rank data recorded by RealizesCoverWord.

Equations

• LeanPool.Erdos132ConvexK3.GeometricallyRealizesCoverWord P d₁ d₂ d₃ w = ∃ (F : LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame P d₁ d₂ d₃), F.RealizesCoverWord w

theorem LeanPool.Erdos132ConvexK3.has_thirteen_word_reduction_of_convex_top_three {n : ℕ} [NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) : HasThirteenWordReduction (vertexDegree P d₁ d₂ d₃) (GeometricallyRealizesCoverWord P d₁ d₂ d₃)

Raw convex/top-three data now supplies the complete direct-or-thirteen- word reduction. No route closure is assumed in this theorem.

def LeanPool.Erdos132ConvexK3.GlobalThirteenWordClosureComplete : Prop

Exact remaining global component after the maximal-gap, five-row, and thirteen-word reductions: prove each canonical geometric word closes by its routed local kernel.

Equations

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

theorem LeanPool.Erdos132ConvexK3.convex_top_three_draft_reduction_complete_of_global_word_closure (hClosure : GlobalThirteenWordClosureComplete) : ConvexTopThreeDraftReductionComplete

Once the route-specific geometric closure interface is constructed, the new raw reduction is the final HasConvexK3DraftReduction adapter.

theorem LeanPool.Erdos132ConvexK3.convex_top_three_degree_six_of_global_word_closure (hClosure : GlobalThirteenWordClosureComplete) : ConvexTopThreeDegreeSixStatement

The same exact closure boundary implies the intended unconditional degree-six statement through the existing thirteen-word assembly.