Mathematical billiards

DefinitionElliptic billiard invariant \(k_{602}\)#✓fully proved

Write \(|XY|\) for the distance between points \(X\) and \(Y\) of the Euclidean plane. For every natural number \(N\), all points \(O, f_1, f_2\) of the plane and all reals \(a, a_c\) with \(O = \frac{1}{2}(f_1 + f_2)\), \(|f_1 f_2| < a\), \(|f_1 f_2| < a_c\) and \(a_c < a\), there is a real number \(C\) with the following property. Let \(P_0, P_1, P_2, \dots\) be points of the plane such that \(|P_i f_1| + |P_i f_2| = a\) and \(P_{i+N} = P_i\) for every \(i\), and such that for every \(i < N\) the points \(P_i\) and \(P_{i+1}\) are distinct and the line \(P_i P_{i+1}\) contains exactly one point \(X\) with \(|X f_1| + |X f_2| = a_c\). For \(i < N\) let \(Q_{1,i}\) and \(Q_{2,i}\) be points of the line \(P_i P_{i+1}\) closest to \(f_1\) and to \(f_2\) respectively. Then

\[\prod_{i\lt N} |f_1 Q_{1,i}| \cdot \prod_{i\lt N} |f_2 Q_{2,i}| = C.\]

In words: the vertices lie on the ellipse with foci \(f_1, f_2\) and major axis \(a\), every side is tangent to the confocal caustic with major axis \(a_c\), and \(Q_{j,i}\) is the foot of the perpendicular from \(f_j\) to the \(i\)-th side.

MathlibExt.Geometry.EllipticBilliard602Wanted.conjecture · 23 lines
def conjecture : Prop :=
  ∀ (N : ℕ) (O f₁ f₂ : EuclideanSpace ℝ (Fin 2)) (a ac : ℝ),
    O = ((1 / 2 : ℝ) • (f₁ + f₂)) →
    dist f₁ f₂ < a →
    dist f₁ f₂ < ac →
    ac < a →
    ∃ C : ℝ,
      ∀ (P : ℕ → EuclideanSpace ℝ (Fin 2)) (Q₁ Q₂ : Fin N → EuclideanSpace ℝ (Fin 2)),
        (∀ i, dist (P i) f₁ + dist (P i) f₂ = a) →
        (∀ i, P (i + N) = P i) →
        (∀ i : Fin N, P i.val ≠ P (i.val + 1)) →
        (∀ i : Fin N, ∃! X : EuclideanSpace ℝ (Fin 2),
          (∃ t : ℝ, X = P i.val + t • (P (i.val + 1) - P i.val)) ∧
            dist X f₁ + dist X f₂ = ac) →
        (∀ i : Fin N, (∃ t : ℝ, Q₁ i = P i.val + t • (P (i.val + 1) - P i.val)) ∧
          ∀ X : EuclideanSpace ℝ (Fin 2),
            (∃ t : ℝ, X = P i.val + t • (P (i.val + 1) - P i.val)) →
              dist f₁ (Q₁ i) ≤ dist f₁ X) →
        (∀ i : Fin N, (∃ t : ℝ, Q₂ i = P i.val + t • (P (i.val + 1) - P i.val)) ∧
          ∀ X : EuclideanSpace ℝ (Fin 2),
            (∃ t : ℝ, X = P i.val + t • (P (i.val + 1) - P i.val)) →
              dist f₂ (Q₂ i) ≤ dist f₂ X) →
        (∏ i : Fin N, dist f₁ (Q₁ i)) * (∏ i : Fin N, dist f₂ (Q₂ i)) = C
Sources
  • [AMR-050-0031] Reznik, Garcia and Koiller, Eighty New Invariants of N-Periodics in the Elliptic Billiard (2021), Table row \(k_{602}\), arXiv:2004.12497.
Used by 1

TheoremBialy–Tabachnikov: \(k_{602}\) is invariant#●ready to prove

The elliptic billiard invariant \(k_{602}\) conjecture holds. Write \(|XY|\) for the distance between points \(X\) and \(Y\). For every natural number \(N\), all points \(O, f_1, f_2\) of the Euclidean plane and all reals \(a, a_c\) with \(O = \frac{1}{2}(f_1 + f_2)\), \(|f_1 f_2| < a\), \(|f_1 f_2| < a_c\) and \(a_c < a\), there is a real number \(C\) with the following property. Let \(P_0, P_1, P_2, \dots\) be points of the plane such that \(|P_i f_1| + |P_i f_2| = a\) and \(P_{i+N} = P_i\) for every \(i\), and such that for every \(i < N\) the points \(P_i\) and \(P_{i+1}\) are distinct and the line \(P_i P_{i+1}\) contains exactly one point \(X\) with \(|X f_1| + |X f_2| = a_c\). For \(i < N\) let \(Q_{1,i}\) and \(Q_{2,i}\) be any points of the line \(P_i P_{i+1}\) closest to \(f_1\) and to \(f_2\) respectively. Then \(\prod_{i\lt N} |f_1 Q_{1,i}| \cdot \prod_{i\lt N} |f_2 Q_{2,i}| = C\).

Bialy and Tabachnikov (Lemma 4.2) show that for each side tangent to the confocal caustic with semi-minor axis \(b\) the two focal distances multiply to \(b^2\), so the common value is \(b^{2N}\).

public theorem_wanted conjecture_holds : conjecture
Sources
  • M. Bialy, S. Tabachnikov, Dan Reznik's identities and more, European Journal of Mathematics (2020), arXiv:2001.08469, https://arxiv.org/abs/2001.08469.
Uses 1

TheoremLattice step of the billiard unfolding in a rectangle#●ready to prove

For a natural number \(j\), let \(\varepsilon_j = 1\) if \(j\) is odd and \(\varepsilon_j = 0\) if \(j\) is even. Let \(a, b > 0\) be real numbers with \(a n = b m\) for some positive integers \(m, n\). Then there are a real number \(t > 0\) and natural numbers \(k > 0\), \(l > 0\) and \(N\) such that \(t = k a = l b\), \(N + 2 = k + l\), \(k\) and \(l\) are coprime, and the point \((\varepsilon_k a, \varepsilon_l b)\) is one of \((a, 0)\), \((0, b)\), \((a, b)\).

In the billiard argument for the \(a \times b\) rectangle, the unfolded diagonal from the corner \((0, 0)\) first meets a corner of the tiling at \((t, t)\) (coprimality is the first-hit condition), \(N\) counts the reflections, and folding back yields the corner \((\varepsilon_k a, \varepsilon_l b)\). This lemma covers only that lattice step; it does not formalize the reflected trajectory and does not prove Problem 147.

theorem_wanted billiardUnfoldingDiagonalLemma :
    ∀ a b : ℝ, 0 < a → 0 < b →
      (∃ m n : ℕ, 0 < m ∧ 0 < n ∧ a * (n : ℝ) = b * (m : ℝ)) →
      ∃ t : ℝ, ∃ k l N : ℕ, 0 < t ∧ 0 < k ∧ 0 < l ∧ t = (k : ℝ) * a ∧
        t = (l : ℝ) * b ∧ N + 2 = k + l ∧ Nat.Coprime k l ∧
        (if k % 2 = 1 then a else 0, if l % 2 = 1 then b else 0) ∈
          ({(a, 0), (0, b), (a, b)} : Set (ℝ × ℝ))
Sources
  • H. Auerbach and S. Mazur, Problem 147 of the Scottish Book; the typescript labels the entry Theorem (Problem Mazur). Elementary unfolding argument for polygonal billiards, see e.g. S. Tabachnikov, Geometry and Billiards.
1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.