/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilInscribed square problem
The inscribed square problem or Toeplitz conjecture asks whether every Jordan curve (i.e. simple close curve in ℝ²) admits an inscribed square, i.e. a square whose vertices all lie on the curve. There are several open and solved variants of this conjecture.
References:
A Survey on the Square Peg Problem by Benjamin Matschke
open Topology ContDiff Manifoldopen scoped EuclideanGeometrynamespace InscribedSquare
Four points a b c d in the plane form a rectangle with a opposite to c iff the line
segments from a to c and from b to d have both the same length and the same midpoint, acting
as the diagonals of the rectangle. We also require the rectangle to be nondegenerate and have a
given aspect ratio ratio : ℝ.
structure IsRectangle (a b c d : ℝ²) (ratio : ℝ) : Prop where
diagonal_midpoints_eq : a + c = b + d
diagonal_lengths_eq : dist a c = dist b d
a_ne_b : a ≠ b
b_ne_c : b ≠ c
has_ratio : (dist a b) / (dist b c) = ratioInscribed square problem Does every Jordan curve admit an inscribed square?
@[category research open, AMS 51]
theorem inscribed_square_problem :
answer(sorry) ↔ ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ),
∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 := ⊢ True ↔ ∀ (γ : Circle → ℝ²), IsEmbedding γ → ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1
All goals completed! 🐙Inscribed rectangle problem Does every Jordan curve admit inscribed rectangles of any given aspect ratio?
@[category research open, AMS 51]
theorem inscribed_rectangle_problem :
answer(sorry) ↔ ∀ (γ : Circle → ℝ²) (hγ : IsEmbedding γ) (r : ℝ) (hr : r > 0),
∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := ⊢ True ↔ ∀ (γ : Circle → ℝ²), IsEmbedding γ → ∀ r > 0, ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r
All goals completed! 🐙It is known that every Jordan curve admits at least one inscribed rectangle.
@[category research solved, AMS 51]
theorem exists_inscribed_rectangle (γ : Circle → ℝ²) (hγ : IsEmbedding γ) :
∃ t₁ t₂ t₃ t₄ r, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := γ:Circle → ℝ²hγ:IsEmbedding γ⊢ ∃ t₁ t₂ t₃ t₄ r, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r
All goals completed! 🐙It is known that every smooth Jordan curve admits inscribed rectangles of all aspect ratios.
@[category research solved, AMS 51]
theorem exists_inscribed_rectangle_of_smooth (γ : Circle → ℝ²)
(hγ : IsEmbedding γ) (hγ' : ContMDiff (𝓡 1) (𝓡 2) ∞ γ) (r : ℝ) (hr : r > 0) :
∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r := γ:Circle → ℝ²hγ:IsEmbedding γhγ':ContMDiff (𝓡 1) (𝓡 2) ∞ γr:ℝhr:r > 0⊢ ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r
All goals completed! 🐙It is also known that every $C^2$ Jordan curve admits an inscribed square.
@[category research solved, AMS 51]
theorem exists_inscribed_square_of_C2 (γ : Circle → ℝ²)
(hγ : IsEmbedding γ) (hγ' : ContMDiff (𝓡 1) (𝓡 2) 2 γ) :
∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1 := γ:Circle → ℝ²hγ:IsEmbedding γhγ':ContMDiff (𝓡 1) (𝓡 2) 2 γ⊢ ∃ t₁ t₂ t₃ t₄, IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1
All goals completed! 🐙end InscribedSquare