Geometric closure of the thirteen global cover words

This file transports the actual maximal-gap frames produced by GlobalAssembly into the four raw local-geometry records proved in WordClosures. All cyclic arcs are explicit finsets of offsets. The two reflected row-4 routes use the orientation-reversing isometry reflectAcrossXAxis; squared distances and degrees are transported back to the original labelling.

def LeanPool.Erdos132ConvexK3.reflectAcrossXAxis (p : Point ℝ) : Point ℝ

Reflection in the horizontal axis. This preserves squared distances and reverses signed orientation.

Equations

• LeanPool.Erdos132ConvexK3.reflectAcrossXAxis p = (p.1, -p.2)

@[simp]

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_sqDist (p q : Point ℝ) : sqDist (reflectAcrossXAxis p) (reflectAcrossXAxis q) = sqDist p q

@[simp]

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_turn (p q r : Point ℝ) : turn (reflectAcrossXAxis p) (reflectAcrossXAxis q) (reflectAcrossXAxis r) = -turn p q r

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_injective : Function.Injective reflectAcrossXAxis

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_strictConvexQuad_reverse {a b c d : Point ℝ} (h : StrictConvexQuad a b c d) : StrictConvexQuad (reflectAcrossXAxis a) (reflectAcrossXAxis d) (reflectAcrossXAxis c) (reflectAcrossXAxis b)

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_halfPlane_reverse (a b p : Point ℝ) : InLeftOpenHalfPlane (reflectAcrossXAxis a) (reflectAcrossXAxis b) (reflectAcrossXAxis p) ↔ InLeftOpenHalfPlane b a p

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_vertexDegree {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (v : Fin n) : vertexDegree (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃ v = vertexDegree P d₁ d₂ d₃ v

theorem LeanPool.Erdos132ConvexK3.reflectAcrossXAxis_top_three_classes {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (h : HasTopThreeDistanceClasses P d₁ d₂ d₃) : HasTopThreeDistanceClasses (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃

theorem LeanPool.Erdos132ConvexK3.penultimate_turn_lt_shared_tip {e t w s : Point ℝ} {d₁ d₂ : ℝ} (het : e ≠ t) (hd₂d₁ : d₂ < d₁) (hes : sqDist e s = d₁) (hts : sqDist t s = d₁) (hew : sqDist e w = d₁) (htw : sqDist t w = d₂) (hw : 0 < turn e t w) (hs : 0 < turn e t s) : turn e t w < turn e t s

On one side of an oriented center line, the point on the first-center circle which is strictly closer to the second center has strictly smaller signed height than the common-radius tip.

theorem LeanPool.Erdos132ConvexK3.red_blue_forcing_sqDist {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) {a b c d : Fin n} (hac : a ≠ c) (hbd : b ≠ d) (hquad : StrictConvexQuad (P a) (P b) (P c) (P d)) (hab : sqDist (P a) (P b) = d₁) (hcd : sqDist (P c) (P d) = d₂) : sqDist (P a) (P c) = d₁ ∧ sqDist (P b) (P d) = d₁

Squared-distance form of red-blue forcing, with the two diagonal class splits discharged from the global top-three hypothesis.

def LeanPool.Erdos132ConvexK3.cyclicOffset {n : ℕ} (base j : Fin n) : ℕ

Counterclockwise offset of a label from a chosen base.

Equations

• LeanPool.Erdos132ConvexK3.cyclicOffset base j = ↑(j - base)

@[simp]

theorem LeanPool.Erdos132ConvexK3.cyclicAdvance_cyclicOffset {n : ℕ} [NeZero n] (base j : Fin n) : cyclicAdvance base (cyclicOffset base j) = j

@[simp]

theorem LeanPool.Erdos132ConvexK3.cyclicOffset_self {n : ℕ} [NeZero n] (base : Fin n) : cyclicOffset base base = 0

theorem LeanPool.Erdos132ConvexK3.cyclicOffset_cyclicAdvance {n : ℕ} [NeZero n] (base : Fin n) {k : ℕ} (hk : k < n) : cyclicOffset base (cyclicAdvance base k) = k

theorem LeanPool.Erdos132ConvexK3.eq_cyclicAdvance_of_cyclicOffset_eq {n : ℕ} [NeZero n] {base j : Fin n} {k : ℕ} (h : cyclicOffset base j = k) : j = cyclicAdvance base k

noncomputable def LeanPool.Erdos132ConvexK3.cyclicOpenInterval {n : ℕ} (base : Fin n) (lo hi : ℕ) : Finset (Fin n)

Labels whose offsets lie strictly between two unwrapped positions.

Equations

• LeanPool.Erdos132ConvexK3.cyclicOpenInterval base lo hi = {j : Fin n | lo < LeanPool.Erdos132ConvexK3.cyclicOffset base j ∧ LeanPool.Erdos132ConvexK3.cyclicOffset base j < hi}

noncomputable def LeanPool.Erdos132ConvexK3.cyclicWrapInterval {n : ℕ} (base : Fin n) (hi lo : ℕ) : Finset (Fin n)

Labels in the open interval that wraps after hi and before lo.

Equations

• LeanPool.Erdos132ConvexK3.cyclicWrapInterval base hi lo = {j : Fin n | hi < LeanPool.Erdos132ConvexK3.cyclicOffset base j ∨ LeanPool.Erdos132ConvexK3.cyclicOffset base j < lo}

@[simp]

theorem LeanPool.Erdos132ConvexK3.mem_cyclicOpenInterval {n : ℕ} {base j : Fin n} {lo hi : ℕ} : j ∈ cyclicOpenInterval base lo hi ↔ lo < cyclicOffset base j ∧ cyclicOffset base j < hi

@[simp]

theorem LeanPool.Erdos132ConvexK3.mem_cyclicWrapInterval {n : ℕ} {base j : Fin n} {hi lo : ℕ} : j ∈ cyclicWrapInterval base hi lo ↔ hi < cyclicOffset base j ∨ cyclicOffset base j < lo

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

Four increasing unwrapped offsets in a single turn form a strict quadrilateral, even when the last offsets use representatives past n.

theorem LeanPool.Erdos132ConvexK3.cyclic_inLeft_of_unwrapped_order {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {a b k : ℕ} (hab : a < b) (hbk : b < k) (hwindow : k < a + n) : InLeftOpenHalfPlane (P (cyclicAdvance base a)) (P (cyclicAdvance base b)) (P (cyclicAdvance base k))

A point after an oriented chord in one unwrapped turn lies in its left open half-plane.

theorem LeanPool.Erdos132ConvexK3.cyclic_inLeft_reverse_of_between {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {a k b : ℕ} (hak : a < k) (hkb : k < b) (hbn : b < n) : InLeftOpenHalfPlane (P (cyclicAdvance base b)) (P (cyclicAdvance base a)) (P (cyclicAdvance base k))

The reversed chord sees the points on its short intervening arc in its left open half-plane.

theorem LeanPool.Erdos132ConvexK3.fullTwoRungGeometry_of_cyclic_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (base : Fin n) {e v t w s r : ℕ} (he_v : e < v) (hv_t : v < t) (ht_w : t < w) (hw_s : w < s) (hs_r : s < r) (hr_n : r < n) (hes : sqDist (P (cyclicAdvance base e)) (P (cyclicAdvance base s)) = d₁) (hts : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base s)) = d₁) (hew : sqDist (P (cyclicAdvance base e)) (P (cyclicAdvance base w)) = d₁) (htw : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base w)) = d₂) (her : sqDist (P (cyclicAdvance base e)) (P (cyclicAdvance base r)) = d₂) (htr : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base r)) = d₁) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

A six-label cyclic pattern with the displayed two-rung distances is the raw shared-tip realization consumed by the full-two-rung kernel.

theorem LeanPool.Erdos132ConvexK3.onePenultimateGeometry_of_cyclic_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (base : Fin n) {e v t p s : ℕ} (he_v : e < v) (hv_t : v < t) (ht_p : t < p) (hp_s : p < s) (hs_n : s < n) (hes : sqDist (P (cyclicAdvance base e)) (P (cyclicAdvance base s)) = d₁) (hts : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base s)) = d₁) (htp : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base p)) = d₂) : Nonempty (OnePenultimateWordGeometry P d₁ d₂ d₃)

The corresponding five-label cyclic pattern realizes the raw one-penultimate anti-saturation record.

theorem LeanPool.Erdos132ConvexK3.reflectedOnePenultimateGeometry_of_cyclic_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (base : Fin n) {t v e s p : ℕ} (ht_v : t < v) (hv_e : v < e) (he_s : e < s) (hs_p : s < p) (hp_n : p < n) (hes : sqDist (P (cyclicAdvance base e)) (P (cyclicAdvance base s)) = d₁) (hts : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base s)) = d₁) (htp : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base p)) = d₂) : Nonempty (OnePenultimateWordGeometry (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃)

Reflection reverses the row-4 cyclic orientation and turns the displayed five-label pattern into the raw one-penultimate orientation.

theorem LeanPool.Erdos132ConvexK3.reflectedRow1B32Geometry_of_cyclic_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (base : Fin n) {t v x s w : ℕ} (ht_v : t < v) (hv_x : v < x) (hx_s : x < s) (hsw : w = s + 1) (hw_n : w < n) (hxw : sqDist (P (cyclicAdvance base x)) (P (cyclicAdvance base w)) ≤ d₂) (hxs : sqDist (P (cyclicAdvance base x)) (P (cyclicAdvance base s)) = d₂) (htw : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base w)) = d₂) (hts : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base s)) = d₁) : Nonempty (Row1B32WordRealization (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃)

Reflected terminal-cage adapter for the row-4 D32 orientation.

theorem LeanPool.Erdos132ConvexK3.fourEdgeEndpointGeometry_of_cyclic_offsets {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hConvex : CyclicStrictConvex P) (base : Fin n) {x v t w s : ℕ} (hx_v : x < v) (hv_t : v < t) (ht_w : t < w) (hsucc : s = w + 1) (hs_n : s < n) (hxw : sqDist (P (cyclicAdvance base x)) (P (cyclicAdvance base w)) = d₁) (hts : sqDist (P (cyclicAdvance base t)) (P (cyclicAdvance base s)) = d₁) : ∃ (E : FourEdgeEndpointGeometry P d₁ d₂ d₃ (cyclicAdvance base x) (cyclicAdvance base t) (cyclicAdvance base w) (cyclicAdvance base s)), E.vertex = cyclicAdvance base v

One endpoint of the row-4 four-edge cage, generated from its cyclic offset pattern.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.two_cover_rank_endpoints {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} {i j : Fin n} {leftMoves rightMoves : ℕ} (path : K3CoverSequence P i j leftMoves rightMoves) (hClasses : HasTopThreeDistanceClasses P d₁ d₂ d₃) (hStart : TopThreeAdjacent P d₁ d₂ d₃ i j) (hEnd : TopThreeAdjacent P d₁ d₂ d₃ (cyclicRetreat i leftMoves) (cyclicAdvance j rightMoves)) (hMoves : leftMoves + rightMoves = 2) : sqDist (P i) (P j) = d₃ ∧ sqDist (P (cyclicRetreat i leftMoves)) (P (cyclicAdvance j rightMoves)) = d₁

Any actual two-cover witness exhausts the three strict distance ranks, independently of the order in which its endpoints move.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.right_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 1 1) (hOrder : path.StartsRight) : sqDist (P i) (P j) = d₃ ∧ sqDist (P i) (P (cyclicAdvance j 1)) = d₂ ∧ sqDist (P (cyclicRetreat i 1)) (P (cyclicAdvance j 1)) = d₁

A one-right/one-left path which starts on the right has the expected d₃,d₂,d₁ ladder.

theorem LeanPool.Erdos132ConvexK3.K3CoverSequence.left_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 1 1) (hOrder : path.StartsLeft) : sqDist (P i) (P j) = d₃ ∧ sqDist (P (cyclicRetreat i 1)) (P j) = d₂ ∧ sqDist (P (cyclicRetreat i 1)) (P (cyclicAdvance j 1)) = d₁

The opposite one-left/one-right order has the same rank ladder, with the middle edge obtained by retreating the left endpoint.

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

First-neighbor gap at the second anchor x+3.

Equations

• F.secondGap = LeanPool.Erdos132ConvexK3.firstNeighborGap P d₁ d₂ d₃ (LeanPool.Erdos132ConvexK3.cyclicAdvance F.x 3)

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

Offset of the second anchor's first counterclockwise neighbor from x.

Equations

• F.uOffset = 3 + F.secondGap

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

Offset of the first clockwise neighbor of x, measured counterclockwise.

Equations

• F.zOffset = n - ↑(LeanPool.Erdos132ConvexK3.firstClockwiseNeighborOffset P d₁ d₂ d₃ F.x)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.card_ge_eight {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : 8 ≤ n

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.secondGap_pos {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : 0 < F.secondGap

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.uOffset_add_M_lt_card {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : F.uOffset + F.M < n

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.zOffset_lt_card {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : F.zOffset < n

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.zOffset_eq_uOffset_add {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : F.zOffset = F.uOffset + F.M + F.pair.first.leftMoves

Outer localization is equality of unwrapped offsets, not merely equality of labels.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.firstClockwiseNeighbor_eq_offset {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : firstClockwiseNeighbor P d₁ d₂ d₃ F.x = cyclicAdvance F.x F.zOffset

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.firstCounterclockwiseNeighbor_eq_uOffset {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) : firstCounterclockwiseNeighbor P d₁ d₂ d₃ (cyclicAdvance F.x 3) = cyclicAdvance F.x F.uOffset

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row1_B32_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row1_B32) : Nonempty (Row1B32WordRealization P d₁ d₂ d₃)

The canonical row-1 terminal word supplies exactly the raw terminal-cage record used by row1_B32_realization_degree_le_six.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row1_B21_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row1_B21) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

Row 1 with first transition d₂→d₁ is the direct full-two-rung realization.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row1_B31_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row1_B31) : Nonempty (OnePenultimateWordGeometry P d₁ d₂ d₃)

Row 1 with first transition d₃→d₁ is the direct one-penultimate realization.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row2_BA_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row2_BA) : Nonempty (OnePenultimateWordGeometry P d₁ d₂ d₃)

The row-2 left-first word is the direct one-penultimate geometry based at the first lower endpoint.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row2_AB_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row2_AB) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

The row-2 right-first word supplies the second full-two-rung realization.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.double_double_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hFirstRight : F.pair.first.rightMoves = 0) (hFirstLeft : F.pair.first.leftMoves = 2) (hM : F.M = 2) (hSecondLeft : F.pair.second.leftMoves = 0) (hSecondRight : F.pair.second.rightMoves = 2) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

The common BB/DD geometry in rows 3 and 5 is a direct full-two-rung record.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row3_BB_DD_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row3_BB_DD) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row5_BB_DD_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row5_BB_DD) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_full_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hFirstRight : F.pair.first.rightMoves = 0) (hFirstLeft : F.pair.first.leftMoves = 2) (hM : F.M = 1) (tOffset : ℕ) (htLower : 1 < tOffset) (htUpper : tOffset ≤ 3) (hTU : sqDist (P (cyclicAdvance F.x tOffset)) (P (cyclicAdvance F.x F.uOffset)) = d₂) (hTS : sqDist (P (cyclicAdvance F.x tOffset)) (P (cyclicAdvance F.x (F.uOffset + 1))) = d₁) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

Common direct row-4 full-two-rung adapter. The second diameter center is either x+3 (D21) or x+2 (CD).

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_D21_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_D21) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_CD_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_CD) : Nonempty (FullTwoRungGeometry P d₁ d₂ d₃)

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_first_ladder_data {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hFirstRight : F.pair.first.rightMoves = 0) (hFirstLeft : F.pair.first.leftMoves = 2) (hM : F.M = 1) : F.uOffset + 3 < n ∧ sqDist (P F.x) (P (cyclicAdvance F.x (F.uOffset + 1))) = d₁ ∧ sqDist (P F.x) (P (cyclicAdvance F.x (F.uOffset + 2))) = d₂

The first double-left ladder shared by every row-4 word.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_D31_reflected_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_D31) : Nonempty (OnePenultimateWordGeometry (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃)

The row-4 D31 route becomes one-penultimate geometry after reflecting the polygon across the horizontal axis.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_DC_reflected_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_DC) : Nonempty (OnePenultimateWordGeometry (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃)

The row-4 DC route has the same reflected raw geometry, with x+2 as its first center.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_D32_reflected_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_D32) : Nonempty (Row1B32WordRealization (fun (i : Fin n) => reflectAcrossXAxis (P i)) d₁ d₂ d₃)

The row-4 D32 terminal cage is the reflected terminal realization.

theorem LeanPool.Erdos132ConvexK3.ErLVGlobalFiveRowFrame.row4_DD_raw_realization {n : ℕ} [NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (F : ErLVGlobalFiveRowFrame P d₁ d₂ d₃) (hWord : F.RealizesCoverWord ExceptionalCoverWord.row4_DD) : Nonempty (Row4DDWordRealization P d₁ d₂ d₃)

The row-4 DD word supplies the complete two-endpoint four-edge cage.

theorem LeanPool.Erdos132ConvexK3.global_thirteen_word_closure_complete : GlobalThirteenWordClosureComplete

The thirteen canonical maximal-gap words all transport to their four raw geometric closure predicates.

theorem LeanPool.Erdos132ConvexK3.convex_top_three_draft_reduction_complete : ConvexTopThreeDraftReductionComplete

Raw convex top-three data now constructs the complete thirteen-word reduction package without an additional hypothesis.

theorem LeanPool.Erdos132ConvexK3.convex_top_three_degree_six : ConvexTopThreeDegreeSixStatement

Every finite strictly convex three-distance configuration has a vertex incident to at most six edges from its three largest distance classes.