Inscribed 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:

• Wikipedia
• A Survey on the Square Peg Problem by Benjamin Matschke
• arxiv/2005.09193

structure IsRectangle (a b c d : EuclideanSpace ℝ (Fin 2)) (ratio : ℝ) : Prop

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 : ℝ.

• 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 = ratio

theorem inscribed_square_problem : (∀ (γ : Circle → EuclideanSpace ℝ (Fin 2)), Topology.IsEmbedding γ → ∃ (t₁ : Circle) (t₂ : Circle) (t₃ : Circle) (t₄ : Circle), IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1) ↔ sorry

Inscribed square problem Does every Jordan curve admit an inscribed square?

theorem inscribed_rectangle_problem : (∀ (γ : Circle → EuclideanSpace ℝ (Fin 2)), Topology.IsEmbedding γ → ∀ r > 0, ∃ (t₁ : Circle) (t₂ : Circle) (t₃ : Circle) (t₄ : Circle), IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r) ↔ sorry

Inscribed rectangle problem Does every Jordan curve admit inscribed rectangles of any given aspect ratio?

theorem exists_inscribed_rectangle (γ : Circle → EuclideanSpace ℝ (Fin 2)) (hγ : Topology.IsEmbedding γ) : ∃ (t₁ : Circle) (t₂ : Circle) (t₃ : Circle) (t₄ : Circle) (r : ℝ), IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r

It is known that every Jordan curve admits at least one inscribed rectangle.

theorem exists_inscribed_rectangle_of_smooth (γ : Circle → EuclideanSpace ℝ (Fin 2)) (hγ : Topology.IsEmbedding γ) (hγ' : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) (↑⊤) γ) (r : ℝ) (hr : r > 0) : ∃ (t₁ : Circle) (t₂ : Circle) (t₃ : Circle) (t₄ : Circle), IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) r

It is known that every smooth Jordan curve admits inscribed rectangles of all aspect ratios.

theorem exists_inscribed_square_of_C2 (γ : Circle → EuclideanSpace ℝ (Fin 2)) (hγ : Topology.IsEmbedding γ) (hγ' : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 2))) 2 γ) : ∃ (t₁ : Circle) (t₂ : Circle) (t₃ : Circle) (t₄ : Circle), IsRectangle (γ t₁) (γ t₂) (γ t₃) (γ t₄) 1

It is also known that every C² Jordan curve admits an inscribed square.