ErLV majorant arc nesting

This file formalizes the geometric core of Erdos--Lovasz--Vesztergombi's Proposition 2.6 argument. A terminal cover edge makes the two exterior boundary angles acute. If two such majorants were avoiding, cyclic convexity propagates those local inequalities to all four angles of their quadrilateral, contradicting strict_convex_quad_not_all_acute.

theorem LeanPool.Erdos132ConvexK3.dot_comm (u v : Point ℝ) : dot u v = dot v u

theorem LeanPool.Erdos132ConvexK3.dot_pos_of_sqDist_le {a b p : Point ℝ} (hap : a ≠ p) (hshort : sqDist p b ≤ sqDist a b) : 0 < dot (b - a) (p - a)

A failed endpoint cover gives a strict acute-angle dot product, provided the polygon side used by that cover is nondegenerate.

theorem LeanPool.Erdos132ConvexK3.dot_self_pos_of_cross_pos_left {u v : Point ℝ} (hcross : 0 < cross u v) : 0 < dot u u

theorem LeanPool.Erdos132ConvexK3.dot_self_pos_of_cross_pos_right {u v : Point ℝ} (hcross : 0 < cross u v) : 0 < dot v v

theorem LeanPool.Erdos132ConvexK3.dot_pos_of_cross_between_left {u w v : Point ℝ} (huw : 0 < cross u w) (hwv : 0 < cross w v) (huv : 0 < cross u v) (hacute : 0 < dot u v) : 0 < dot u w

A ray strictly between two rays in an open half-plane is their positive linear combination. This determinant identity transfers an acute endpoint inequality to the intermediate ray.

theorem LeanPool.Erdos132ConvexK3.dot_pos_of_cross_between_right {u w v : Point ℝ} (huw : 0 < cross u w) (hwv : 0 < cross w v) (huv : 0 < cross u v) (hacute : 0 < dot u v) : 0 < dot v w

theorem LeanPool.Erdos132ConvexK3.cross_trans_of_common_half_plane {e u v w : Point ℝ} (heu : 0 < cross e u) (hev : 0 < cross e v) (hew : 0 < cross e w) (huv : 0 < cross u v) (hvw : 0 < cross v w) : 0 < cross u w

theorem LeanPool.Erdos132ConvexK3.positive_cross_chain (V : ℕ → Point ℝ) (N : ℕ) (hbase : ∀ (r : ℕ), 1 < r → r ≤ N → 0 < cross (V 1) (V r)) (hstep : ∀ (r : ℕ), 1 ≤ r → r < N → 0 < cross (V r) (V (r + 1))) {j k : ℕ} (hj : 1 ≤ j) (hjk : j < k) (hkN : k ≤ N) : 0 < cross (V j) (V k)

Positive consecutive turns are transitive while the whole chain stays in one open half-plane.

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_turn_zero_of_lt {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) {j k : Fin n} (hj : 0 < j) (hjk : j < k) : 0 < turn (P 0) (P j) (P k)

The boundary-half-plane definition of cyclic strict convexity implies positive orientation for every three labels in increasing order from zero.

def LeanPool.Erdos132ConvexK3.cyclicRotate {K : Type u_1} {n : ℕ} [_nonzero : NeZero n] (P : Fin n → Point K) (base : Fin n) : Fin n → Point K

Relabel a cyclic configuration so that base becomes index zero.

Equations

• LeanPool.Erdos132ConvexK3.cyclicRotate P base i = P (base + i)

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_rotate {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) : CyclicStrictConvex (cyclicRotate P base)

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_turn_from_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {j k : Fin n} (hj : 0 < j) (hjk : j < k) : 0 < turn (P base) (P (base + j)) (P (base + k))

Positive orientation for any three vertices described by increasing cyclic offsets from an arbitrary base vertex.

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_turn_advance {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {j k : ℕ} (hj : 0 < j) (hjk : j < k) (hkn : k < n) : 0 < turn (P base) (P (cyclicAdvance base j)) (P (cyclicAdvance base k))

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_turn_unwrapped {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {a b c : ℕ} (hab : a < b) (hbc : b < c) (hwindow : c < a + n) : 0 < turn (P (cyclicAdvance base a)) (P (cyclicAdvance base b)) (P (cyclicAdvance base c))

Positive orientation for three increasing positions in one unwrapped window of the cyclic order. The last two positions may exceed n; their Fin representatives wrap automatically.

theorem LeanPool.Erdos132ConvexK3.cyclicAdvance_period {n : ℕ} [NeZero n] (i : Fin n) (k : ℕ) : cyclicAdvance i (k + n) = cyclicAdvance i k

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_advance_one {n : ℕ} [NeZero n] (i : Fin n) {k : ℕ} (hk : 0 < k) (hkn : k < n) : cyclicRetreat (cyclicAdvance i k) 1 = cyclicAdvance i (k - 1)

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_advance {n : ℕ} [NeZero n] (i : Fin n) {k m : ℕ} (hmk : m ≤ k) (hkn : k < n) : cyclicRetreat (cyclicAdvance i k) m = cyclicAdvance i (k - m)

theorem LeanPool.Erdos132ConvexK3.cyclicRetreat_eq_advance_complement {n : ℕ} [NeZero n] (i : Fin n) {k : ℕ} (hk : 0 < k) (hkn : k < n) : cyclicRetreat i k = cyclicAdvance i (n - k)

theorem LeanPool.Erdos132ConvexK3.cyclicAdvance_one_eq_next {n : ℕ} [NeZero n] (i : Fin n) : cyclicAdvance i 1 = cyclicNext i

theorem LeanPool.Erdos132ConvexK3.cyclicNext_retreat_one {n : ℕ} [NeZero n] (i : Fin n) : cyclicNext (cyclicRetreat i 1) = i

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

theorem LeanPool.Erdos132ConvexK3.cyclic_strict_convex_boundary_points_ne {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (hn : 3 ≤ n) (i : Fin n) : P i ≠ P (cyclicNext i)

theorem LeanPool.Erdos132ConvexK3.majorant_left_local_acute {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (hConvex : CyclicStrictConvex P) (hn : 3 ≤ n) (hMajorant : IsMajorant P i j) : 0 < dot (P j - P i) (P (cyclicRetreat i 1) - P i)

theorem LeanPool.Erdos132ConvexK3.majorant_right_local_acute {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {i j : Fin n} (hConvex : CyclicStrictConvex P) (hn : 3 ≤ n) (hMajorant : IsMajorant P i j) : 0 < dot (P i - P j) (P (cyclicAdvance j 1) - P j)

theorem LeanPool.Erdos132ConvexK3.vertexDegree_le_pred {n : ℕ} [_nonzero : NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (v : Fin n) : vertexDegree P d₁ d₂ d₃ v ≤ n - 1

theorem LeanPool.Erdos132ConvexK3.eight_le_card_of_degree_seven {n : ℕ} [_nonzero : NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 7 ≤ vertexDegree P d₁ d₂ d₃ v) : 8 ≤ n

theorem LeanPool.Erdos132ConvexK3.fin_ofNat_val {n : ℕ} [NeZero n] (k : Fin n) : Fin.ofNat n ↑k = k

theorem LeanPool.Erdos132ConvexK3.ccwNeighborOffsets_card_eq_vertexDegree {n : ℕ} [NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (v : Fin n) : (ccwNeighborOffsets P d₁ d₂ d₃ v).card = vertexDegree P d₁ d₂ d₃ v

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

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

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

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

theorem LeanPool.Erdos132ConvexK3.first_neighbor_gap_cw_budget {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {v : Fin n} (hdegree : 7 ≤ vertexDegree P d₁ d₂ d₃ v) : firstNeighborGap P d₁ d₂ d₃ v + ↑(firstClockwiseNeighborOffset P d₁ d₂ d₃ v) + 6 ≤ n

With degree at least seven, the two first-neighbor gaps leave at least six polygon sides between their endpoints.

theorem LeanPool.Erdos132ConvexK3.erlv_terminal_majorants_not_avoiding_of_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {v vp sp s : ℕ} (hvv : v < vp) (hvsp : vp < sp) (hsps : sp < s) (hsn : s < n) (hFirst : IsMajorant P (cyclicAdvance base s) (cyclicAdvance base v)) (hSecond : IsMajorant P (cyclicAdvance base vp) (cyclicAdvance base sp)) : False

Offset form of ErLV Proposition 2.6's geometric step. If the endpoints of two terminal edges occur as v < v' < s' < s in one unwrapped cyclic window, the edges are avoiding, which is impossible.

theorem LeanPool.Erdos132ConvexK3.erlv_majorant_arc_nesting_of_inner_separation {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) (first : K3MajorantWitness P d₁ d₂ d₃ (firstClockwiseNeighbor P d₁ d₂ d₃ x) x) (second : K3MajorantWitness P d₁ d₂ d₃ (cyclicAdvance x 3) (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3))) (hInner : first.rightMoves + second.leftMoves < 3) : ∃ M ≤ second.rightMoves, cyclicRetreat (firstClockwiseNeighbor P d₁ d₂ d₃ x) first.leftMoves = cyclicAdvance (firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance x 3)) M

The ErLV arc-nesting conclusion once the paper's undisplayed inner-end separation v < v' is made explicit. All remaining order facts, including u < s, follow from maximality and the degree-seven gap budget.

theorem LeanPool.Erdos132ConvexK3.k3_inner_endpoint_budget_partition {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {i j k ell : Fin n} (first : K3MajorantWitness P d₁ d₂ d₃ i j) (second : K3MajorantWitness P d₁ d₂ d₃ k ell) : first.rightMoves + second.leftMoves < 3 ∨ first.rightMoves = 1 ∧ second.leftMoves = 2 ∨ first.rightMoves = 2 ∧ second.leftMoves = 1 ∨ first.rightMoves = 2 ∧ second.leftMoves = 2

The two independent k = 3 cover budgets leave exactly three cases in which the inner endpoints are not strictly ordered as in ErLV Figure 4. This is an arithmetic partition only: it does not assert that any exceptional case is geometrically realizable.

def LeanPool.Erdos132ConvexK3.ErLVInnerEndpointSeparationComplete : Prop

Exact extra statement needed to justify ErLV's printed sentence "Obviously, v' lies on the arc vt" under the draft's side-count convention. It asks for a jointly minimal pair of actual cover paths whose facing endpoints consume strictly fewer than the three sides between x and t.

Equations

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

theorem LeanPool.Erdos132ConvexK3.erlv_majorant_arc_nesting_complete_of_inner_endpoint_separation (hInner : ErLVInnerEndpointSeparationComplete) : ErLVMajorantArcNestingComplete

All of ErLV Proposition 2.6's geometry now closes the requested nesting headline once the source's undisplayed strict order of the inner endpoints is supplied.

theorem LeanPool.Erdos132ConvexK3.erlv_terminal_majorants_not_avoiding {a b c d pa nb pc nd : Point ℝ} (hquad : StrictConvexQuad a b c d) (haCone : 0 < turn a b d ∧ 0 < turn a d pa ∧ 0 < turn a b pa) (hbCone : 0 < turn b nb c ∧ 0 < turn b c a ∧ 0 < turn b nb a) (hcCone : 0 < turn c d b ∧ 0 < turn c b pc ∧ 0 < turn c d pc) (hdCone : 0 < turn d nd a ∧ 0 < turn d a c ∧ 0 < turn d nd c) (haLocal : 0 < dot (b - a) (pa - a)) (hbLocal : 0 < dot (a - b) (nb - b)) (hcLocal : 0 < dot (d - c) (pc - c)) (hdLocal : 0 < dot (c - d) (nd - d)) : False

The exact geometric core of ErLV Proposition 2.6: two terminal edges cannot be avoiding. The four h*Cone hypotheses spell out the cyclic ray order between each majorant endpoint and the adjacent boundary vertex on the exterior side.