ErLV maximal-gap arithmetic for the convex three-distance argument

This file isolates the integer bookkeeping in draft Sections 3--4. A K3Majorant records cover moves, equivalently polygon sides consumed at its two ends. In particular, the first majorant's fields are the draft's a,b; they are not counts of interior points. This is the side-count convention for which the rank budget is a + b ≤ 2.

Signed integers are used for arc differences. Thus the case L < 0, where u precedes y in unwrapped order, is represented rather than discarded.

structure LeanPool.Erdos132ConvexK3.K3Majorant : Type

Cover moves at the two ends of a k = 3 majorant.

For the majorant of zx, leftMoves = a counts moves at the x-end and rightMoves = b counts moves at the z-end. For the majorant of tu, the same fields are the draft's α,β. Every move consumes one polygon side and strictly raises one of the three distance ranks, hence at most two moves.

• leftMoves : ℕ

  Cover moves made at the first endpoint.

• rightMoves : ℕ

  Cover moves made at the second endpoint.

• coverBudget : self.leftMoves + self.rightMoves ≤ 2

structure LeanPool.Erdos132ConvexK3.ErLVK3MaximalGapSetup : Type

Arithmetic data retained from the two ErLV majorants after choosing a vertex with maximal first-neighbor gap.

• first : K3Majorant

  Majorant issuing from the maximal-gap vertex.

• second : K3Majorant

  Facing majorant issuing three cyclic steps later.

• gapX : ℕ

  First-neighbor gap at the selected maximal-gap vertex.

• gapT : ℕ

  First-neighbor gap at the facing vertex.

• gapT_le_gapX : self.gapT ≤ self.gapX
• M : ℕ

  M = |us|_sides; the second majorant consumes at least these moves at its u-end.

• M_le_secondRight : self.M ≤ self.second.rightMoves

def LeanPool.Erdos132ConvexK3.ErLVK3MaximalGapSetup.delta (D : ErLVK3MaximalGapSetup) : ℕ

The maximal-gap slack δ = gₓ - gₜ.

Equations

• D.delta = D.gapX - D.gapT

def LeanPool.Erdos132ConvexK3.ErLVK3MaximalGapSetup.L (D : ErLVK3MaximalGapSetup) : ℤ

The signed side difference L = |yu|_sides = 3 - δ.

Equations

• D.L = 3 - ↑D.delta

def LeanPool.Erdos132ConvexK3.ErLVK3MaximalGapSetup.yzSides (D : ErLVK3MaximalGapSetup) : ℤ

The signed side difference |yz| = L + M + b.

Equations

• D.yzSides = D.L + ↑D.M + ↑D.first.rightMoves

theorem LeanPool.Erdos132ConvexK3.maximal_gap_L_eq_three_sub_delta (D : ErLVK3MaximalGapSetup) : D.L = 3 - ↑D.delta

Maximality gives the exact corrected formula L = 3 - δ, not merely ErLV's printed loose upper bound.

theorem LeanPool.Erdos132ConvexK3.maximal_gap_L_le_three (D : ErLVK3MaximalGapSetup) : D.L ≤ 3

The corrected maximal-gap formula implies the sharp signed bound L ≤ 3.

theorem LeanPool.Erdos132ConvexK3.maximal_gap_signed_yu (D : ErLVK3MaximalGapSetup) {x t y u : ℤ} (ht : t = x + 3) (hy : y = x + ↑D.gapX) (hu : u = t + ↑D.gapT) : u - y = D.L

With unwrapped indices t=x+3, y=x+gₓ, and u=t+gₜ, maximality turns the signed arc difference u-y into 3-δ.

theorem LeanPool.Erdos132ConvexK3.signed_arc_arithmetic {y u s z L M b : ℤ} (hyu : u - y = L) (hus : s - u = M) (hsz : z - s = b) : z - y = L + M + b

Signed arc arithmetic remains valid when L < 0: if u-y=L, s-u=M, and z-s=b, then z-y=L+M+b.

theorem LeanPool.Erdos132ConvexK3.majorant_M_le_two (D : ErLVK3MaximalGapSetup) : D.M ≤ 2

The second majorant gives the draft bound M ≤ 2.

theorem LeanPool.Erdos132ConvexK3.maximal_gap_signed_yz (D : ErLVK3MaximalGapSetup) {x t y u s z : ℤ} (ht : t = x + 3) (hy : y = x + ↑D.gapX) (hu : u = t + ↑D.gapT) (hus : s - u = ↑D.M) (hsz : z - s = ↑D.first.rightMoves) : z - y = D.yzSides

The complete signed arc identity for the maximal-gap setup.

def LeanPool.Erdos132ConvexK3.IsExceptionalMajorantRow (a b L M : ℤ) : Prop

The five and only five integer rows for which the short-arc inequality L + M + b ≤ 5 fails under the k = 3 majorant budgets.

Equations

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

theorem LeanPool.Erdos132ConvexK3.five_row_enumeration {a b L M δ : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hM0 : 0 ≤ M) (hδ : 0 ≤ δ) (hcover : a + b ≤ 2) (hM2 : M ≤ 2) (hL : L = 3 - δ) : 5 < L + M + b ↔ IsExceptionalMajorantRow a b L M

Transparent Presburger certification of draft table (3.5)/(Section 4): the short-arc bound fails exactly on the five displayed (a,b,L,M) rows.

theorem LeanPool.Erdos132ConvexK3.maximal_gap_five_row_enumeration (D : ErLVK3MaximalGapSetup) : 5 < D.yzSides ↔ IsExceptionalMajorantRow (↑D.first.leftMoves) (↑D.first.rightMoves) D.L ↑D.M

The structure-level form of five_row_enumeration, with a,b,L,M read directly from the two majorants and maximal-gap data.

theorem LeanPool.Erdos132ConvexK3.negative_L_short_arc (D : ErLVK3MaximalGapSetup) (hL : D.L < 0) : D.yzSides ≤ 5

A negative signed L can never be exceptional; it forces the desired short-arc bound directly.