Geometric inputs for the convex three-distance argument

This file proves the strict edge--diagonal inequality, its diameter and red--blue consequences, chord half-plane separation, and same-half-plane uniqueness for two-circle intersections.

noncomputable def LeanPool.Erdos132ConvexK3.euclideanDist (a b : Point ℝ) : ℝ

Ordinary Euclidean distance between real Cartesian points.

Equations

• LeanPool.Erdos132ConvexK3.euclideanDist a b = dist (LeanPool.Erdos132ConvexK3.toComplex✝ a) (LeanPool.Erdos132ConvexK3.toComplex✝ b)

theorem LeanPool.Erdos132ConvexK3.euclideanDist_sq (a b : Point ℝ) : euclideanDist a b ^ 2 = sqDist a b

The ordinary distance squares to the polynomial Cartesian squared distance used by the top-three graph.

theorem LeanPool.Erdos132ConvexK3.edge_diagonal_inequality {a b c d : Point ℝ} (h : StrictConvexQuad a b c d) : euclideanDist a b + euclideanDist c d < euclideanDist a c + euclideanDist b d

Edge--diagonal inequality. Opposite side sums in a strictly convex cyclic quadrilateral are strictly smaller than the diagonal sum.

theorem LeanPool.Erdos132ConvexK3.strict_convex_quad_not_all_acute {a b c d : Point ℝ} (hquad : StrictConvexQuad a b c d) (ha : 0 < dot (b - a) (d - a)) (hb : 0 < dot (a - b) (c - b)) (hc : 0 < dot (b - c) (d - c)) (hd : 0 < dot (c - d) (a - d)) : False

Four strictly acute interior angles are impossible in a strict convex quadrilateral. This is the algebraic form of the final sentence in ErLV's majorant argument.

theorem LeanPool.Erdos132ConvexK3.avoiding_diameters_impossible {a b c d : Point ℝ} {diameter : ℝ} (hquad : StrictConvexQuad a b c d) (hab : euclideanDist a b = diameter) (hcd : euclideanDist c d = diameter) (hac : euclideanDist a c ≤ diameter) (hbd : euclideanDist b d ≤ diameter) : False

Avoiding-diameter impossibility. Two opposite sides of a strictly convex cyclic quadrilateral cannot both realize its diameter.

theorem LeanPool.Erdos132ConvexK3.red_blue_forcing {a b c d : Point ℝ} {d₁ d₂ : ℝ} (hquad : StrictConvexQuad a b c d) (hd : d₂ < d₁) (hab : euclideanDist a b = d₁) (hcd : euclideanDist c d = d₂) (hac : euclideanDist a c ≤ d₂ ∨ euclideanDist a c = d₁) (hbd : euclideanDist b d ≤ d₂ ∨ euclideanDist b d = d₁) : euclideanDist a c = d₁ ∧ euclideanDist b d = d₁

Red--blue forcing. Avoiding sides in the largest and second-largest classes force both diagonals into the largest class.

theorem LeanPool.Erdos132ConvexK3.turn_cyclic {K : Type u_1} [CommRing K] (a b c : Point K) : turn a b c = turn b c a

theorem LeanPool.Erdos132ConvexK3.turn_swap {K : Type u_1} [CommRing K] (a b c : Point K) : turn a c b = -turn a b c

theorem LeanPool.Erdos132ConvexK3.chord_half_plane_separation {K : Type u_1} [CommRing K] [LinearOrder K] {a b c d : Point K} (h : StrictConvexQuad a b c d) : InLeftOpenHalfPlane a c d ∧ InLeftOpenHalfPlane c a b

Chord half-plane separation. In cyclic order a,b,c,d, the two boundary arcs represented by b and d lie in opposite open half-planes of chord ac.

theorem LeanPool.Erdos132ConvexK3.same_half_plane_two_circle_unique {a b p q : Point ℝ} (hab : a ≠ b) (hap : sqDist a p = sqDist a q) (hbp : sqDist b p = sqDist b q) (hp : InLeftOpenHalfPlane a b p) (hq : InLeftOpenHalfPlane a b q) : p = q

Same-half-plane two-circle uniqueness. Two points with the same distances to distinct centers coincide if both are in the same open half-plane bounded by the line of centers.

theorem LeanPool.Erdos132ConvexK3.diameter_lens_abscissa {c X Y : ℝ} (hc : 0 < c) (hleft : sqDist (0, 0) (X, Y) ≤ (2 * c) ^ 2) (hright : sqDist (2 * c, 0) (X, Y) ≤ (2 * c) ^ 2) (hneLeft : (X, Y) ≠ (0, 0)) (hneRight : (X, Y) ≠ (2 * c, 0)) : 0 < X ∧ X < 2 * c

A point distinct from both endpoints and contained in both closed disks whose common diameter is the endpoint segment has abscissa strictly between the endpoint abscissae. The disk bounds are the explicit diameter property needed for the strict box 0 < X < 2c.

theorem LeanPool.Erdos132ConvexK3.two_rung_sum_identity {c d H Δ X Y : ℝ} (hconstraint : 2 * c * d + d ^ 2 = Δ * (H + (H - Δ))) : sqDist (X, Y) (c + d, H - Δ) + sqDist (X, Y) (c - d, H - Δ) - 2 * sqDist (X, Y) (c, H) = -4 * c * d + 4 * Δ * Y

The exact algebra behind draft equation (5.5). The displayed constraint 2cd + d² = Δ(H + (H - Δ)) is essential; without it the identity is false.

theorem LeanPool.Erdos132ConvexK3.two_rung_sum_identity_with_classes {c d H Δ X Y A B : ℝ} (hconstraint : 2 * c * d + d ^ 2 = Δ * (H + (H - Δ))) (hclasses : B - A = -4 * c * d) : sqDist (X, Y) (c + d, H - Δ) + sqDist (X, Y) (c - d, H - Δ) - 2 * sqDist (X, Y) (c, H) = B - A + 4 * Δ * Y

Draft equation (5.5), with B - A = -4cd made explicit.