equichordal_point_unique.toml

id = "equichordal_point_unique"
title = "Equichordal point theorem (convex curves have a unique equichordal point)"
test = false
module = "LeanEval.Geometry.Equichordal"
holes = ["equichordal_point_unique"]
submitter = "Kim Morrison"
notes = "A compact convex planar domain with nonempty interior cannot have two distinct equichordal points: there is no pair of interior points P ≠ Q such that, for each, every direction yields a boundary chord of one fixed total length. The curve is packaged as the frontier of K; for convex K a line through an interior point meets the boundary on the two opposite rays. Mathlib has StarConvex and the Euclidean plane EuclideanSpace ℝ (Fin 2) but no equichordal-point theory. The original uniqueness was proved by Rychlik; Knill lists it as §205."
source = "M. R. Rychlik, A complete solution to the equichordal point problem of Fujiwara, Blaschke, Rothe and Weizenböck, Invent. Math. 129 (1997). Listed as §205 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §205."
informal_solution = "Suppose P and Q were two distinct equichordal points with common chord constant L. Following Rychlik, complexify and analyze the equichordal map (the involution sending one chord endpoint through P to the opposite endpoint through Q); its dynamics define a real-analytic area-preserving map of the annulus whose invariant curves and heteroclinic connections are obstructed. Rychlik shows the resulting functional/dynamical system has no closed convex curve solution for L > 0 unless P = Q, contradicting P ≠ Q. No such argument is available in Mathlib, which lacks the equichordal map, its complex-analytic continuation, and the KAM/heteroclinic machinery used."