The shared-diameter lens

This file formalizes the unique-farthest lemma used in draft Section 6. The normalization is

e = (0,0), t = (2c,0), s = (c,H), d₁² = c² + H².

The P5-1 correction is explicit in the theorem statement: the lower point P = (X,Y) must satisfy |Ps|² ≤ d₁². Convexity supplies Y < 0, but it does not by itself supply 0 < X < 2c; the diameter bound does.

def LeanPool.Erdos132ConvexK3.InSharedDiameterLens (c H : ℝ) (v : Point ℝ) : Prop

The intersection of the two closed radius-d₁ disks centered at (0,0) and (2c,0), where d₁² = c² + H².

Equations

• LeanPool.Erdos132ConvexK3.InSharedDiameterLens c H v = (LeanPool.Erdos132ConvexK3.sqDist (0, 0) v ≤ c ^ 2 + H ^ 2 ∧ LeanPool.Erdos132ConvexK3.sqDist (2 * c, 0) v ≤ c ^ 2 + H ^ 2)

theorem LeanPool.Erdos132ConvexK3.diameter_partner_abscissa {c H X Y : ℝ} (hc : 0 < c) (hH : 0 < H) (hY : Y < 0) (hdiameter : sqDist (X, Y) (c, H) ≤ c ^ 2 + H ^ 2) : 0 < X ∧ X < 2 * c

P5-1, explicit. If a lower point's distance to the shared diameter tip is at most the diameter, then its abscissa lies strictly between the two centers. The diameter hypothesis is load-bearing.

theorem LeanPool.Erdos132ConvexK3.shared_diameter_lens_ordinate_le {c H x y : ℝ} (hH : 0 ≤ H) (hv : InSharedDiameterLens c H (x, y)) : y ≤ H

Every point of the shared-diameter lens has ordinate at most that of the upper tip (c,H).

theorem LeanPool.Erdos132ConvexK3.diameter_lens_unique_farthest {c H X Y : ℝ} (hc : 0 < c) (hH : 0 < H) (hY : Y < 0) (hPdiameter : sqDist (X, Y) (c, H) ≤ c ^ 2 + H ^ 2) {v : Point ℝ} (hv : InSharedDiameterLens c H v) (hne : v ≠ (c, H)) : sqDist (X, Y) v < sqDist (X, Y) (c, H)

Diameter-lens unique farthest point. Let P=(X,Y) be below the center line and no farther than the diameter from the upper tip s. Then every other point of the shared-diameter lens is strictly closer to P than s is.

This is the exact squared-distance form of draft (5.2), used in Section 6. The hPdiameter hypothesis is the formal repair of P5-1.