Moving Sofa Problem #

References:

Wikipedia
[Ge92] Gerver, J. L., On moving a sofa around a corner. Geometriae Dedicata 42.3 (1992): 267-283.
[Ro18] Romik, D. Differential equations and exact solutions in the moving sofa problem. Experimental mathematics 27.3 (2018): 316-330.
[Ba24] Baek, J. Optimality of Gerver's Sofa. arXiv preprint arXiv:2411.19826 (2024).

source

def MovingSofa.horizontalHallway :

Set (EuclideanSpace ℝ (Fin 2))

The horizontal side of the hallway is $(-\infty, 1] \times [0, 1]$.

Equations

MovingSofa.horizontalHallway = {x : EuclideanSpace ℝ (Fin 2) | ∃ (x_1 : ℝ) (y : ℝ) (_ : x_1 ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1), !₂[x_1, y] = x}

Instances For

source

def MovingSofa.verticalHallway :

Set (EuclideanSpace ℝ (Fin 2))

The vertical side of the hallway is $[0, 1] \times (-\infty, 1]$.

Equations

MovingSofa.verticalHallway = {x : EuclideanSpace ℝ (Fin 2) | ∃ (x_1 : ℝ) (y : ℝ) (_ : 0 ≤ x_1 ∧ x_1 ≤ 1 ∧ y ≤ 1), !₂[x_1, y] = x}

Instances For

source

def MovingSofa.hallway :

Set (EuclideanSpace ℝ (Fin 2))

The hallway is the union of its horizontal and vertical sides.

Equations

MovingSofa.hallway = MovingSofa.horizontalHallway ∪ MovingSofa.verticalHallway

Instances For

source

def MovingSofa.«termE(2)» :

Lean.ParserDescr

Equations

MovingSofa.«termE(2)» = Lean.ParserDescr.node `MovingSofa.«termE(2)» 1024 (Lean.ParserDescr.symbol "E(2)")

Instances For

source

instance MovingSofa.instTopologicalSpaceAffineIsometryEquivRealEuclideanSpaceFinOfNatNat_formalConjectures :

TopologicalSpace (EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ ] EuclideanSpace ℝ (Fin 2))

Equations

One or more equations did not get rendered due to their size.

source

structure MovingSofa.IsMovingSofa (s : Set (EuclideanSpace ℝ (Fin 2))) (m : ↑unitInterval → EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ ] EuclideanSpace ℝ (Fin 2)) :

Prop

A connected closed set $s$ is a moving sofa according to a rigid motion $m:I\to\mathrm{SE}(2)$, if the sofa is initially in the horizontal side of the hallway and ends up in the vertical side. Here, since $\mathrm{SE}(2)$ is not in Mathlib yet, we use $\mathrm{E}(2)$ and rely on continuity and $m(0) = \mathrm{id}$ to ensure $m$ is in $\mathrm{SE}(2)$.

isConnected : IsConnected s
isClosed : IsClosed s
continuous : Continuous m
zero : m 0 = AffineIsometryEquiv.refl ℝ (EuclideanSpace ℝ (Fin 2))
initial : s ⊆ horizontalHallway
subset_hallway (t : ↑unitInterval) : ⇑(m t) '' s ⊆ hallway
final : ⇑(m 1) '' s ⊆ verticalHallway

Instances For

source

def MovingSofa.unitSquare :

Set (EuclideanSpace ℝ (Fin 2))

The unit square.

Equations

MovingSofa.unitSquare = parallelepiped ⇑(EuclideanSpace.basisFun (Fin 2) ℝ)

Instances For

source

theorem MovingSofa.isMovingSofa_unitSquare :

∃ (m : ↑unitInterval → EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ ] EuclideanSpace ℝ (Fin 2)), IsMovingSofa unitSquare m

The unit square $[0,1]^2$ is a valid moving sofa (with the identity motion). It sits in the corner where both hallways overlap, so the stationary motion works. This is a sanity check that the IsMovingSofa definition is not vacuous.

source

def MovingSofa.rotateTranslate (α : Real.Angle) (p : EuclideanSpace ℝ (Fin 2)) :

EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ ] EuclideanSpace ℝ (Fin 2)

The rigid motion that translates by $p$ and then rotates counterclockwise by $\alpha$. Note that [Ge92] used this definition while [Ro18] used rotation first and then translation.

Equations

MovingSofa.rotateTranslate α p = (EuclideanGeometry.o.rotation α).toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst ℝ p)

Instances For

source

def MovingSofa.sofaOfRotateTranslatePath (p : ℝ → EuclideanSpace ℝ (Fin 2)) :

Set (EuclideanSpace ℝ (Fin 2))

The sofa according to a rotation path $p : [0, \pi/2] \to \mathbb{R}^2$ as in [Ge92] is the intersection over $\alpha \in [0, \pi/2]$ of hallways each translated by $p(\alpha)$ and then rotated by $\alpha$, with the special cases that the hallway at $0$ is the horizontal side and the hallway at $\pi/2$ is the vertical side.

Equations