China South-Eastern 2024 Problem 2
Let $P$ be a convex polygon in the plane. If the endpoints of a line segment $AB$ lie on the boundary of $P$, and the region between the two lines passing through $A$ and $B$ perpendicular to $AB$ (including the boundary) contains $P$, then the segment $AB$ is called a $J$-chord. Find the largest positive integer $k$ such that any convex polygon $P$ in the plane has $k$ $J$-chords.
import Mathlib.Analysis.InnerProductSpace.PiL2
abbrev Plane := EuclideanSpace ℝ (Fin 2)
def IsConvexPolygon (P : Set Plane) : Prop :=
∃ s : Finset Plane, P = convexHull ℝ s ∧ (interior P).Nonempty
def IsJChord (P : Set Plane) (A B : Plane) : Prop := A ∈ frontier P ∧ B ∈ frontier P ∧ A ≠ B ∧
∀ X ∈ P, 0 ≤ inner ℝ (X - A) (B - A) ∧ 0 ≤ inner ℝ (X - B) (A - B)
def HasAtLeastKJChords (P : Set Plane) (k : ℕ) : Prop := ∃ s : Finset (Plane × Plane),
s.card = k ∧ (∀ p ∈ s, IsJChord P p.1 p.2) ∧ (∀ p ∈ s, (p.2, p.1) ∉ s)
def answer : ℕ := sorry
theorem solution : IsGreatest {k : ℕ | k > 0 ∧ (∀ P : Set Plane,
IsConvexPolygon P → HasAtLeastKJChords P k)} answer := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
None yet.