Moving sofa problem

DefinitionCorridor#✓fully proved

The corridor is the L-shaped set of points \(z \in \mathbb{C}\) with \(\operatorname{Re} z \le 1\) and \(0 \le \operatorname{Im} z \le 1\) (the horizontal arm, extending to the left) together with the points \(z\) with \(0 \le \operatorname{Re} z \le 1\) and \(\operatorname{Im} z \ge 0\) (the vertical arm, extending upward): two perpendicular semi-infinite arms of width one.

def corridor : Set ℂ :=
  {z | z.re ≤ 1 ∧ 0 ≤ z.im ∧ z.im ≤ 1} ∪
    {z | 0 ≤ z.re ∧ z.re ≤ 1 ∧ 0 ≤ z.im}

Used by 2

Used byPassing the corridor · The unit square passes the corridor

DefinitionEntrance of the corridor#✓fully proved

The entrance region of the unit right-angle corridor is the closed half-strip \(\{z \in \mathbb{C} : \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z \le 1\}\), the part of its horizontal arm to the left of the corner square.

def entrance : Set ℂ := {z | z.re ≤ 0 ∧ 0 ≤ z.im ∧ z.im ≤ 1}

Used by 2

Used byPassing the corridor · The unit square passes the corridor

DefinitionExit of the corridor#✓fully proved

The exit region of the unit right-angle corridor is the closed half-strip \(\{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ \operatorname{Im} z \ge 1\}\), the part of its vertical arm above the corner square.

def exit : Set ℂ := {z | 0 ≤ z.re ∧ z.re ≤ 1 ∧ 1 ≤ z.im}

Used by 2

Used byPassing the corridor · The unit square passes the corridor

StructurePlanar rigid motion#✓fully proved

A motion consists of a continuous map \(t \mapsto u_t\) from \([0, 1]\) to the unit circle \(\{u \in \mathbb{C} : |u| = 1\}\) (the rotation) and a continuous map \(t \mapsto c_t\) from \([0, 1]\) to \(\mathbb{C}\) (the translation).

structure Motion where
  /-- The orientation-preserving unit complex rotation at each time. -/
  rotation : C(unitInterval, Circle)
  /-- The planar translation at each time. -/
  translation : C(unitInterval, ℂ)

Used by 12

Used byPassing the corridor · Passing the mirrored corridor · Passing the Z corridor at a given separation · Motions preserve distance · Position under a rigid motion · The unit square passes the corridor · The unit square passes the mirrored corridor · Z-corridor passage of the unit square · The square's translation through the corner · The square's translation through the mirrored corner · The square's translation through the Z corridor at separation one · The square's translation through the Z corridor

DefinitionPosition under a rigid motion#✓fully proved

Let \(m\) be a motion with rotation \(u(t)\) in the unit circle and translation \(c(t) \in \mathbb{C}\) at each time \(t \in [0, 1]\). The position at time \(t\) of a point \(z \in \mathbb{C}\) is \(u(t)\,z + c(t)\).

def Motion.position (m : Motion) (t : unitInterval) (z : ℂ) : ℂ :=
  (m.rotation t : ℂ) * z + m.translation t

Uses 1 · Used by 7

Statement usesPlanar rigid motion

Used byPassing the corridor · Passing the mirrored corridor · Passing the Z corridor at a given separation · Motions preserve distance · The unit square passes the corridor · The unit square passes the mirrored corridor · Z-corridor passage of the unit square

DefinitionPassing the corridor#✓fully proved

A set \(K \subseteq \mathbb{C}\) can pass the corridor if there are continuous maps \(u\) from \([0, 1]\) to the unit circle \(\{w \in \mathbb{C} : |w| = 1\}\) and \(c\) from \([0, 1]\) to \(\mathbb{C}\) such that, writing \(K_t = \{u(t) z + c(t) : z \in K\}\) for the position of \(K\) at time \(t\), \(K_0\) lies in the entrance arm, \(K_1\) lies in the exit arm, and \(K_t\) lies in the corridor for every \(t \in [0, 1]\).

def CanPass (K : Set ℂ) : Prop :=
  ∃ m : Motion,
    m.position 0 '' K ⊆ entrance ∧
    m.position 1 '' K ⊆ exit ∧
    ∀ t : unitInterval, m.position t '' K ⊆ corridor

Uses 5 · Used by 3

Statement usesPlanar rigid motion · Position under a rigid motion · Corridor · Entrance of the corridor · Exit of the corridor

Used bySofa shapes · The unit square passes the corridor · The unit square is a sofa

DefinitionSofa shapes#✓fully proved

A set \(K \subseteq \mathbb{C}\) is a sofa when it is Lebesgue measurable, nonempty and connected, and can be moved through the unit right-angle corridor: there is a motion (a rotation by a unit complex number and a translation, both varying continuously with time \(t \in [0, 1]\)) that places \(K\) inside the corridor's entrance region at time \(0\), inside its exit region at time \(1\), and inside the corridor at every time \(t\).

def IsSofa (K : Set ℂ) : Prop :=
  NullMeasurableSet K volume ∧ IsConnected K ∧ CanPass K

Uses 1 · Used by 6

Statement usesPassing the corridor

Used byThe ambidextrous optimal area is at most the optimal area · Ambidextrous sofa shapes · The optimal sofa area is at least one · Optimal sofa area · The unit square is an ambidextrous sofa · The unit square is a sofa

DefinitionOptimal sofa area#✓fully proved

Let the corridor be \(L = \{z \in \mathbb{C} : \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\} \cup \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z\}\), with entrance \(E = \{z \in \mathbb{C} : \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z \le 1\}\) and exit \(X = \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 1 \le \operatorname{Im} z\}\). A sofa is a nonempty connected Lebesgue-measurable set \(K \subseteq \mathbb{C}\) for which there are continuous maps \(u : [0, 1] \to \{w \in \mathbb{C} : |w| = 1\}\) and \(c : [0, 1] \to \mathbb{C}\) such that, writing \(K_t = \{u(t)\,z + c(t) : z \in K\}\), we have \(K_0 \subseteq E\), \(K_1 \subseteq X\) and \(K_t \subseteq L\) for every \(t \in [0, 1]\). The optimal sofa area is the supremum, taken in \([0, \infty]\), of the Lebesgue measures of all sofas.

Because the supremum is taken in \([0, \infty]\), neither its finiteness nor its attainment is assumed.

noncomputable def optimalArea : ℝ≥0∞ := ⨆ (K : Set ℂ) (_ : IsSofa K), volume K

Uses 1 · Used by 6

Statement usesSofa shapes

Used byThe ambidextrous optimal area is at most the optimal area · Gerver's lower bound for the moving sofa constant · Hammersley's lower bound for the moving sofa constant · Hammersley's upper bound for the moving sofa constant · Kallus–Romik upper bound for the moving sofa constant · The optimal sofa area is at least one

DefinitionUnit square#✓fully proved

The unit square is the set of complex numbers \(z\) with \(0 \le \operatorname{Re} z \le 1\) and \(0 \le \operatorname{Im} z \le 1\), that is, the square \([0,1] \times [0,1]\) in the complex plane.

def unitSquare : Set ℂ :=
  Complex.measurableEquivRealProd ⁻¹' (Icc (0 : ℝ) 1 ×ˢ Icc (0 : ℝ) 1)

Used by 12

Used byThe ambidextrous sofa constant is at least one · The optimal sofa area is at least one · The unit square has area one · The unit square passes the corridor · The unit square passes the mirrored corridor · Z-corridor passage of the unit square for large separations · Z-corridor passage of the unit square · Z-corridor passage of the unit square at separation one · The unit square is connected · The unit square is an ambidextrous sofa · The unit square is a sofa · The unit square is Borel measurable

DefinitionThe square's translation through the corner#✓fully proved

The motion with no rotation that sends a point \(z\) at time \(t \in [0,1]\) to \(z + \tau(t)\), where \(\tau(t) = 2t - 1\) for \(t \le 1/2\) and \(\tau(t) = (2t - 1)i\) for \(t \ge 1/2\): it moves a shape one unit to the right during the first half of the time interval and then one unit upward.

noncomputable def squareMotion : Motion where
  rotation := ContinuousMap.const unitInterval 1
  translation :=
    ⟨fun t ↦ ((min (2 * (t : ℝ) - 1) 0 : ℝ) : ℂ) +
      ((max (2 * (t : ℝ) - 1) 0 : ℝ) : ℂ) * Complex.I, by fun_prop⟩

Uses 1 · Used by 1

Statement usesPlanar rigid motion

Used byThe unit square passes the corridor

TheoremMotions preserve distance#✓fully proved

Let \(m\) be a motion, \(t \in [0, 1]\) a time, and write \(m_t(z)\) for the position of a point \(z \in \mathbb{C}\) under \(m\) at time \(t\). Then \(|m_t(z) - m_t(w)| = |z - w|\) for all \(z, w \in \mathbb{C}\).

theorem motion_preserves_distance (m : Motion) (t : unitInterval) (z w : ℂ) :
    dist (m.position t z) (m.position t w) = dist z w

Uses 2

Statement usesPlanar rigid motion · Position under a rigid motion

TheoremThe unit square is Borel measurable#✓fully proved

The unit square \([0,1] \times [0,1]\) is a measurable set for the Borel \(\sigma\)-algebra of the complex plane.

theorem square_measurable : MeasurableSet unitSquare

Uses 1 · Used by 1

Statement usesUnit square

Used byThe unit square is a sofa

TheoremThe unit square is connected#✓fully proved

The unit square \(\{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\}\) is a nonempty connected subset of \(\mathbb{C}\).

theorem square_connected : IsConnected unitSquare

Uses 1 · Used by 1

Statement usesUnit square

Used byThe unit square is a sofa

TheoremThe unit square has area one#✓fully proved

The unit square \(\{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\}\) has Lebesgue measure \(1\).

theorem square_area : volume unitSquare = 1

Uses 1 · Used by 2

Statement usesUnit square

Used byThe ambidextrous sofa constant is at least one · The optimal sofa area is at least one

TheoremThe unit square passes the corridor#✓fully proved

Let the corridor be \(L = \{z \in \mathbb{C} : \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\} \cup \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z\}\), with entrance \(E = \{z \in \mathbb{C} : \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z \le 1\}\) and exit \(X = \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 1 \le \operatorname{Im} z\}\). For the unit square \(Q = \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\}\) there are continuous maps \(u : [0, 1] \to \{w \in \mathbb{C} : |w| = 1\}\) and \(c : [0, 1] \to \mathbb{C}\) such that, writing \(Q_t = \{u(t)\,z + c(t) : z \in Q\}\), we have \(Q_0 \subseteq E\), \(Q_1 \subseteq X\) and \(Q_t \subseteq L\) for every \(t \in [0, 1]\).

A pure translation, first to the right and then upward, suffices.

theorem square_canPass : CanPass unitSquare

Uses 8 · Used by 1

Statement usesPassing the corridor · Unit square

Proof usesPlanar rigid motion · Position under a rigid motion · Corridor · Entrance of the corridor · Exit of the corridor · The square's translation through the corner

Used byThe unit square is a sofa

TheoremThe unit square is a sofa#✓fully proved

The unit square \([0,1] \times [0,1]\) in the complex plane is a sofa: it is null-measurable for Lebesgue measure, connected, and there are continuous maps \(u \colon [0,1] \to \{w \in \mathbb{C} : |w| = 1\}\) and \(v \colon [0,1] \to \mathbb{C}\) such that the motion \(z \mapsto u(t) z + v(t)\) carries the square into the entrance \(\{z : \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z \le 1\}\) at \(t = 0\), into the exit \(\{z : 0 \le \operatorname{Re} z \le 1,\ 1 \le \operatorname{Im} z\}\) at \(t = 1\), and into the unit right-angle corridor \(\{z : \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\} \cup \{z : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z\}\) at every time \(t \in [0,1]\).

theorem square_isSofa : IsSofa unitSquare

Uses 6 · Used by 2

Statement usesSofa shapes · Unit square

Proof usesPassing the corridor · The unit square passes the corridor · The unit square is connected · The unit square is Borel measurable

Used byThe optimal sofa area is at least one · The unit square is an ambidextrous sofa

TheoremThe optimal sofa area is at least one#✓fully proved

The optimal sofa area, that is, the supremum in \([0, \infty]\) of the Lebesgue areas of all sofas, is at least \(1\).

The unit square, a sofa of area \(1\), witnesses the bound.

theorem one_le_optimalArea : 1 ≤ optimalArea

Uses 5

Statement usesOptimal sofa area

Proof usesSofa shapes · The unit square has area one · The unit square is a sofa · Unit square

DefinitionMirrored corridor#✓fully proved

The mirrored corridor is the set of points \(z \in \mathbb{C}\) with \(\operatorname{Re} z \ge -1\) and \(0 \le \operatorname{Im} z \le 1\) (the horizontal arm, extending to the right) together with the points \(z\) with \(-1 \le \operatorname{Re} z \le 0\) and \(\operatorname{Im} z \ge 0\) (the vertical arm, extending upward). It is the reflection of the corridor in the imaginary axis, so passing it requires the opposite turn.

def corridorOther : Set ℂ :=
  {z | -1 ≤ z.re ∧ 0 ≤ z.im ∧ z.im ≤ 1} ∪
    {z | -1 ≤ z.re ∧ z.re ≤ 0 ∧ 0 ≤ z.im}

Used by 2

Used byPassing the mirrored corridor · The unit square passes the mirrored corridor

DefinitionEntrance arm of the mirrored corridor#✓fully proved

The entrance arm of the mirrored corridor is the set of points \(z \in \mathbb{C}\) with \(\operatorname{Re} z \ge 0\) and \(0 \le \operatorname{Im} z \le 1\): the part of its horizontal arm beyond the corner square \(-1 \le \operatorname{Re} z \le 0\), \(0 \le \operatorname{Im} z \le 1\).

def entranceOther : Set ℂ := {z | 0 ≤ z.re ∧ 0 ≤ z.im ∧ z.im ≤ 1}

Used by 2

Used byPassing the mirrored corridor · The unit square passes the mirrored corridor

DefinitionExit of the mirrored corridor#✓fully proved

The exit region of the mirrored unit corridor is the closed half-strip \(\{z \in \mathbb{C} : -1 \le \operatorname{Re} z \le 0,\ \operatorname{Im} z \ge 1\}\), the part of its vertical arm above its corner square.

def exitOther : Set ℂ := {z | -1 ≤ z.re ∧ z.re ≤ 0 ∧ 1 ≤ z.im}

Used by 2

Used byPassing the mirrored corridor · The unit square passes the mirrored corridor

DefinitionPassing the mirrored corridor#✓fully proved

A set \(K \subseteq \mathbb{C}\) can pass the mirrored corridor if there are continuous maps \(u\) from \([0, 1]\) to the unit circle \(\{w \in \mathbb{C} : |w| = 1\}\) and \(c\) from \([0, 1]\) to \(\mathbb{C}\) such that, writing \(K_t = \{u(t) z + c(t) : z \in K\}\) for the position of \(K\) at time \(t\), \(K_0\) lies in the entrance arm of the mirrored corridor, \(K_1\) lies in the exit arm of the mirrored corridor, and \(K_t\) lies in the mirrored corridor for every \(t \in [0, 1]\).

def CanPassOther (K : Set ℂ) : Prop :=
  ∃ m : Motion,
    m.position 0 '' K ⊆ entranceOther ∧
    m.position 1 '' K ⊆ exitOther ∧
    ∀ t : unitInterval, m.position t '' K ⊆ corridorOther

Uses 5 · Used by 1

Statement usesPlanar rigid motion · Position under a rigid motion · Mirrored corridor · Entrance arm of the mirrored corridor · Exit of the mirrored corridor

Used byThe unit square passes the mirrored corridor

DefinitionZ-shaped corridor#✓fully proved

For a real number \(d\), the Z-shaped corridor with corner separation \(d\) is the set of points \(z \in \mathbb{C}\) lying in at least one of three pieces: the lower horizontal arm, where \(\operatorname{Re} z \le 1\) and \(0 \le \operatorname{Im} z \le 1\); the middle channel, where \(0 \le \operatorname{Re} z \le 1\) and \(0 \le \operatorname{Im} z \le 2 + d\); and the upper horizontal arm, where \(\operatorname{Re} z \ge 0\) and \(1 + d \le \operatorname{Im} z \le 2 + d\).

The middle channel is bounded: it does not contain the upward ray above the upper arm. For \(d = 1\) the two corner squares are separated by one full corridor width. Passing the corridor requires one turn in each direction inside a single passage.

def corridorZ (d : ℝ) : Set ℂ :=
  {z | z.re ≤ 1 ∧ 0 ≤ z.im ∧ z.im ≤ 1} ∪
    {z | 0 ≤ z.re ∧ z.re ≤ 1 ∧ 0 ≤ z.im ∧ z.im ≤ 2 + d} ∪
    {z | 0 ≤ z.re ∧ 1 + d ≤ z.im ∧ z.im ≤ 2 + d}

Used by 2

Used byPassing the Z corridor at a given separation · Z-corridor passage of the unit square

DefinitionEntrance arm of the Z corridor#✓fully proved

The entrance region of the Z corridor is the closed half-strip \(\{z \in \mathbb{C} : \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z \le 1\}\), the part of its horizontal entrance arm to the left of the middle channel.

def entranceZ : Set ℂ := {z | z.re ≤ 0 ∧ 0 ≤ z.im ∧ z.im ≤ 1}

Used by 2

Used byPassing the Z corridor at a given separation · Z-corridor passage of the unit square

DefinitionExit arm of the Z corridor#✓fully proved

For a real number \(d\) (the corner separation), the exit region of the Z corridor with separation \(d\) is the closed half-strip \(\{z \in \mathbb{C} : \operatorname{Re} z \ge 1,\ 1 + d \le \operatorname{Im} z \le 2 + d\}\), the part of its horizontal exit arm to the right of the middle channel.

def exitZ (d : ℝ) : Set ℂ := {z | 1 ≤ z.re ∧ 1 + d ≤ z.im ∧ z.im ≤ 2 + d}

Used by 2

Used byPassing the Z corridor at a given separation · Z-corridor passage of the unit square

DefinitionPassing the Z corridor at a given separation#✓fully proved

For a real number \(d\), a set \(K \subseteq \mathbb{C}\) can pass the Z corridor with corner separation \(d\) if there are continuous maps \(u\) from \([0, 1]\) to the unit circle \(\{w \in \mathbb{C} : |w| = 1\}\) and \(c\) from \([0, 1]\) to \(\mathbb{C}\) such that, writing \(K_t = \{u(t) z + c(t) : z \in K\}\) for the position of \(K\) at time \(t\), \(K_0\) lies in the entrance arm of the Z corridor, \(K_1\) lies in the exit arm of the Z corridor with corner separation \(d\), and \(K_t\) lies in the Z corridor with corner separation \(d\) for every \(t \in [0, 1]\).

Such a passage is a single motion that turns once in each direction.

def CanPassZAt (K : Set ℂ) (d : ℝ) : Prop :=
  ∃ m : Motion,
    m.position 0 '' K ⊆ entranceZ ∧
    m.position 1 '' K ⊆ exitZ d ∧
    ∀ t : unitInterval, m.position t '' K ⊆ corridorZ d

Uses 5 · Used by 4

Statement usesPlanar rigid motion · Position under a rigid motion · Z-shaped corridor · Entrance arm of the Z corridor · Exit arm of the Z corridor

Used byPassing the Z corridor for all large separations · Z-corridor passage of the unit square for large separations · Z-corridor passage of the unit square · Z-corridor passage of the unit square at separation one

DefinitionPassing the Z corridor for all large separations#✓fully proved

A set \(K \subseteq \mathbb{C}\) can pass the Z corridor if there is a real number \(D\) such that, for every real \(d \ge D\), \(K\) can pass the Z corridor with corner separation \(d\); that is, \(K\) passes whenever the corners are sufficiently separated.

Unlike the mirrored corridor, this is not implied by an ordinary passage: time reversal plus a rigid motion transports an ordinary passage to the mirrored corridor, but a Z passage couples both turns in one motion.

def CanPassZ (K : Set ℂ) : Prop :=
  ∃ D : ℝ, ∀ d : ℝ, D ≤ d → CanPassZAt K d

Uses 1 · Used by 4

Statement usesPassing the Z corridor at a given separation

Used byThe ambidextrous optimal area is at most the optimal area · Ambidextrous sofa shapes · Z-corridor passage of the unit square for large separations · The unit square is an ambidextrous sofa

DefinitionThe square's translation through the Z corridor#✓fully proved

For a real number \(d\), the motion with no rotation that sends a point \(z\) at time \(t \in [0,1]\) to \(z + \tau(t)\), where \(\tau(t) = 3t - 1\) for \(t \le 1/3\), \(\tau(t) = (1 + d)(3t - 1)i\) for \(1/3 \le t \le 2/3\), and \(\tau(t) = (3t - 2) + (1 + d)i\) for \(t \ge 2/3\): it translates a shape by \(1\), then by \((1 + d)i\), then by \(1\), each segment taking a third of the time interval.

noncomputable def squareMotionZAt (d : ℝ) : Motion where
  rotation := ContinuousMap.const unitInterval 1
  translation :=
    ⟨fun t ↦ ((-1 + min (3 * (t : ℝ)) 1 + max (3 * (t : ℝ) - 2) 0 : ℝ) : ℂ) +
      (((1 + d) * min (max (3 * (t : ℝ) - 1) 0) 1 : ℝ) : ℂ) * Complex.I,
      by fun_prop⟩

Uses 1 · Used by 2

Statement usesPlanar rigid motion

Used byZ-corridor passage of the unit square · The square's translation through the Z corridor at separation one

TheoremZ-corridor passage of the unit square#✓fully proved

For every real \(d \ge 0\), the unit square passes the Z corridor with corner separation \(d\).

theorem square_canPassZAt (d : ℝ) (hd : 0 ≤ d) : CanPassZAt unitSquare d

Uses 8 · Used by 2

Statement usesPassing the Z corridor at a given separation · Unit square

Proof usesPlanar rigid motion · Position under a rigid motion · Z-shaped corridor · Entrance arm of the Z corridor · Exit arm of the Z corridor · The square's translation through the Z corridor

Used byZ-corridor passage of the unit square for large separations · Z-corridor passage of the unit square at separation one

DefinitionThe square's translation through the Z corridor at separation one#✓fully proved

The square's translation through the Z corridor at separation \(d = 1\): the motion with no rotation that sends a point \(z\) at time \(t \in [0,1]\) to \(z + \tau(t)\), where \(\tau(t) = 3t - 1\) for \(t \le 1/3\), \(\tau(t) = 2(3t - 1)i\) for \(1/3 \le t \le 2/3\), and \(\tau(t) = (3t - 2) + 2i\) for \(t \ge 2/3\).

noncomputable def squareMotionZ : Motion := squareMotionZAt 1

Uses 2

Statement usesPlanar rigid motion · The square's translation through the Z corridor

TheoremZ-corridor passage of the unit square at separation one#✓fully proved

The unit square passes the Z corridor with corner separation \(1\).

theorem square_canPassZAt_one : CanPassZAt unitSquare 1

Uses 3

Statement usesPassing the Z corridor at a given separation · Unit square

Proof usesZ-corridor passage of the unit square

TheoremZ-corridor passage of the unit square for large separations#✓fully proved

There is a real \(D\) such that for every \(d \ge D\) the unit square passes the Z corridor with corner separation \(d\).

theorem square_canPassZ : CanPassZ unitSquare

Uses 4 · Used by 1

Statement usesPassing the Z corridor for all large separations · Unit square

Proof usesPassing the Z corridor at a given separation · Z-corridor passage of the unit square

Used byThe unit square is an ambidextrous sofa

DefinitionAmbidextrous sofa shapes#✓fully proved

A set \(K \subseteq \mathbb{C}\) is an ambidextrous sofa when it is a sofa and there is a real number \(D\) such that, for every corner separation \(d \ge D\), a single motion places \(K\) inside the entrance arm of the Z corridor with separation \(d\) at time \(0\), inside its exit arm at time \(1\), and inside that corridor at every time; such a passage turns once in each direction.

(Two independent passages, one through each mirrored L corridor, would not suffice: an ordinary passage transports to the mirrored corridor by time reversal plus a rigid motion, so that formulation would collapse to the ordinary sofa condition.)

def IsAmbidextrousSofa (K : Set ℂ) : Prop :=
  IsSofa K ∧ CanPassZ K

Uses 2 · Used by 4

Statement usesPassing the Z corridor for all large separations · Sofa shapes

Used byOptimal area of ambidextrous sofas · The ambidextrous optimal area is at most the optimal area · The ambidextrous sofa constant is at least one · The unit square is an ambidextrous sofa

DefinitionOptimal area of ambidextrous sofas#✓fully proved

The ambidextrous optimal area is the supremum, taken in \([0, \infty]\), of the Lebesgue areas of all ambidextrous sofas \(K \subseteq \mathbb{C}\).

noncomputable def ambidextrousOptimalArea : ℝ≥0∞ :=
  ⨆ (K : Set ℂ) (_ : IsAmbidextrousSofa K), volume K

Uses 1 · Used by 6

Statement usesAmbidextrous sofa shapes

Used byThe ambidextrous optimal area is at most the optimal area · Baek upper bound for the ambidextrous sofa · Gibbs lower bound for the ambidextrous sofa · Hammersley upper bound for the ambidextrous sofa · The ambidextrous sofa constant is at least one · Romik lower bound for the ambidextrous sofa

TheoremThe ambidextrous optimal area is at most the optimal area#✓fully proved

The supremum, in \([0, \infty]\), of the Lebesgue areas of all ambidextrous sofas is at most the supremum of the Lebesgue areas of all sofas. This holds because every ambidextrous sofa is a sofa.

theorem ambidextrousOptimalArea_le_optimalArea :
    ambidextrousOptimalArea ≤ optimalArea

Uses 5

Statement usesOptimal area of ambidextrous sofas · Optimal sofa area

Proof usesPassing the Z corridor for all large separations · Ambidextrous sofa shapes · Sofa shapes

DefinitionThe square's translation through the mirrored corner#✓fully proved

The motion with no rotation that sends a point \(z\) at time \(t \in [0,1]\) to \(z + \tau(t)\), where \(\tau(t) = -2t\) for \(t \le 1/2\) and \(\tau(t) = -1 + (2t - 1)i\) for \(t \ge 1/2\): it moves a shape one unit to the left during the first half of the time interval and then one unit upward.

noncomputable def squareMotionOther : Motion where
  rotation := ContinuousMap.const unitInterval 1
  translation :=
    ⟨fun t ↦ ((-1 - min (2 * (t : ℝ) - 1) 0 : ℝ) : ℂ) +
      ((max (2 * (t : ℝ) - 1) 0 : ℝ) : ℂ) * Complex.I, by fun_prop⟩

Uses 1 · Used by 1

Statement usesPlanar rigid motion

Used byThe unit square passes the mirrored corridor

TheoremThe unit square passes the mirrored corridor#✓fully proved

Let the mirrored corridor be \(L' = \{z \in \mathbb{C} : -1 \le \operatorname{Re} z,\ 0 \le \operatorname{Im} z \le 1\} \cup \{z \in \mathbb{C} : -1 \le \operatorname{Re} z \le 0,\ 0 \le \operatorname{Im} z\}\), with entrance \(E' = \{z \in \mathbb{C} : 0 \le \operatorname{Re} z,\ 0 \le \operatorname{Im} z \le 1\}\) and exit \(X' = \{z \in \mathbb{C} : -1 \le \operatorname{Re} z \le 0,\ 1 \le \operatorname{Im} z\}\). For the unit square \(Q = \{z \in \mathbb{C} : 0 \le \operatorname{Re} z \le 1,\ 0 \le \operatorname{Im} z \le 1\}\) there are continuous maps \(u : [0, 1] \to \{w \in \mathbb{C} : |w| = 1\}\) and \(c : [0, 1] \to \mathbb{C}\) such that, writing \(Q_t = \{u(t)\,z + c(t) : z \in Q\}\), we have \(Q_0 \subseteq E'\), \(Q_1 \subseteq X'\) and \(Q_t \subseteq L'\) for every \(t \in [0, 1]\).

theorem square_canPassOther : CanPassOther unitSquare

Uses 8

Statement usesPassing the mirrored corridor · Unit square

Proof usesPlanar rigid motion · Position under a rigid motion · Mirrored corridor · Entrance arm of the mirrored corridor · Exit of the mirrored corridor · The square's translation through the mirrored corner

TheoremThe unit square is an ambidextrous sofa#✓fully proved

The unit square \([0,1] \times [0,1]\) in the complex plane is an ambidextrous sofa.

theorem square_isAmbidextrousSofa : IsAmbidextrousSofa unitSquare

Uses 6 · Used by 1

Statement usesAmbidextrous sofa shapes · Unit square

Proof usesPassing the Z corridor for all large separations · Sofa shapes · Z-corridor passage of the unit square for large separations · The unit square is a sofa

Used byThe ambidextrous sofa constant is at least one

TheoremThe ambidextrous sofa constant is at least one#✓fully proved

The supremum of the Lebesgue areas of all ambidextrous sofas, taken in \([0, \infty]\), is at least \(1\).

The unit square \([0, 1] \times [0, 1]\) is an ambidextrous sofa of area \(1\).

theorem one_le_ambidextrousOptimalArea : 1 ≤ ambidextrousOptimalArea

Uses 5

Statement usesOptimal area of ambidextrous sofas

Proof usesAmbidextrous sofa shapes · The unit square has area one · The unit square is an ambidextrous sofa · Unit square

TheoremHammersley upper bound for the ambidextrous sofa#●ready to prove

The supremum of the areas of ambidextrous sofas, taken in \([0, \infty]\), is at most \(2\sqrt{2}\).

theorem_wanted hammersley_upper :
    MovingSofa.ambidextrousOptimalArea ≤ ENNReal.ofReal (2 * Real.sqrt 2)

Sources

• catalogue upper row, Hammersley (1968), adapted from C41a.

Uses 1

Statement usesOptimal area of ambidextrous sofas

TheoremBaek upper bound for the ambidextrous sofa#●ready to prove

The supremum of the areas of ambidextrous sofas, taken in \([0, \infty]\), is at most \(22195/10000 = 2.2195\).

theorem_wanted baek_upper :
    MovingSofa.ambidextrousOptimalArea ≤
      ENNReal.ofReal ((22195 : ℝ) / 10000)

Sources

• catalogue upper row, Baek (2024) naive bound from C41a, exact decimal endpoint 22195 / 10000.

Uses 1

Statement usesOptimal area of ambidextrous sofas

TheoremGibbs lower bound for the ambidextrous sofa#●ready to prove

The supremum of the areas of ambidextrous sofas, taken in \([0, \infty]\), is at least \(164495/100000 = 1.64495\).

theorem_wanted gibbs_lower :
    ENNReal.ofReal ((164495 : ℝ) / 100000) ≤
      MovingSofa.ambidextrousOptimalArea

Sources

• catalogue lower row, Gibbs (2014) numerical construction, exact decimal endpoint 164495 / 100000.

Uses 1

Statement usesOptimal area of ambidextrous sofas

TheoremRomik lower bound for the ambidextrous sofa#●ready to prove

The supremum of the areas of ambidextrous sofas, taken in \([0, \infty]\), is at least \(164495521/100000000 = 1.64495521\).

theorem_wanted romik_lower :
    ENNReal.ofReal ((164495521 : ℝ) / 100000000) ≤
      MovingSofa.ambidextrousOptimalArea

Sources

• catalogue lower row, Romik (2016), exact decimal endpoint 164495521 / 100000000.

Uses 1

Statement usesOptimal area of ambidextrous sofas

TheoremHammersley's upper bound for the moving sofa constant#●ready to prove

The moving sofa constant, the supremum of the areas of connected Lebesgue-measurable planar shapes that a continuous rigid motion can carry through the right-angled corridor of width \(1\), is at most \(2\sqrt{2}\).

public theorem_wanted hammersley_upper :
    MovingSofa.optimalArea ≤ ENNReal.ofReal (2 * Real.sqrt 2)

Sources

• catalogue line 13, attributed to Hammersley (1968). Primary not retained.

Uses 1

Statement usesOptimal sofa area

TheoremKallus–Romik upper bound for the moving sofa constant#●ready to prove

The moving sofa constant, the supremum of the areas of connected Lebesgue-measurable planar shapes that a continuous rigid motion can carry through the right-angled corridor of width \(1\), is at most \(2.37\).

public theorem_wanted kallus_romik_upper :
    MovingSofa.optimalArea ≤ ENNReal.ofReal ((237 : ℝ) / 100)

Sources

• catalogue line 14, Kallus-Romik (2018). Numerical certificate not retained.

Uses 1

Statement usesOptimal sofa area

TheoremHammersley's lower bound for the moving sofa constant#●ready to prove

The moving sofa constant, the supremum of the areas of connected Lebesgue-measurable planar shapes that a continuous rigid motion can carry through the right-angled corridor of width \(1\), is at least \(\pi/2 + 2/\pi\).

public theorem_wanted hammersley_lower :
    ENNReal.ofReal (Real.pi / 2 + 2 / Real.pi) ≤ MovingSofa.optimalArea

Sources

• catalogue line 21, Hammersley (1968). Construction not retained.

Uses 1

Statement usesOptimal sofa area

TheoremGerver's lower bound for the moving sofa constant#●ready to prove

The moving sofa constant, the supremum of the areas of connected Lebesgue-measurable planar shapes that a continuous rigid motion can carry through the right-angled corridor of width \(1\), is at least \(2.2195\).

public theorem_wanted gerver_printed_lower :
    ENNReal.ofReal ((4439 : ℝ) / 2000) ≤ MovingSofa.optimalArea

Sources

• catalogue line 22, printed Gerver lower target, not an exact area formula.

Uses 1

Statement usesOptimal sofa area

38 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.