FormalConjectures.Wikipedia.MovingSofa

/-
Copyright 2026 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 FormalConjecturesUtil

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).


noncomputable section


namespace MovingSofa


open Topology

open scoped Real unitInterval EuclideanGeometry

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

def horizontalHallway : Set ℝ² := {!2[x, y] | (x) (y) (_ : x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1)}

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

def verticalHallway : Set ℝ² := {!2[x, y] | (x) (y) (_ : 0 ≤ x ∧ x ≤ 1 ∧ y ≤ 1)}

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

def hallway : Set ℝ² := horizontalHallway ∪ verticalHallway


scoped notation "E(2)" => ℝ² ≃ᵃⁱ[ℝ] ℝ²


instance : TopologicalSpace E(2) :=
  .induced (·.toAffineIsometry.toContinuousAffineMap) inferInstance

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)$.

structure IsMovingSofa (s : Set ℝ²) (m : I → E(2)) : Prop where
  isConnected : IsConnected s
  isClosed : IsClosed s
  continuous : Continuous m
  zero : m 0 = .refl ℝ ℝ²
  initial : s ⊆ horizontalHallway
  subset_hallway : ∀ t, m t '' s ⊆ hallway
  final : m 1 '' s ⊆ verticalHallway

The unit square.

def unitSquare : Set ℝ² := parallelepiped (EuclideanSpace.basisFun (Fin 2) ℝ)

Coordinates of points in the unit square lie in [0,1].

@[category API, AMS 49]
private lemma mem_Icc_of_mem_unitSquare {p : ℝ²} (hp : p ∈ unitSquare) (i : Fin 2) :
    p i ∈ Set.Icc (0:ℝ) 1 := byp:ℝ²hp:p ∈ unitSquarei:Fin 2⊢ p.ofLp i ∈ Set.Icc 0 1
  have h := parallelepiped_basis_eq (EuclideanSpace.basisFun (Fin 2) ℝ).toBasisp:ℝ²hp:p ∈ unitSquarei:Fin 2h:parallelepiped ⇑(EuclideanSpace.basisFun (Fin 2) ℝ).toBasis =
  {x | ∀ (i : Fin 2), ((EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.repr x) i ∈ Set.Icc 0 1} := 
  parallelepiped_basis_eq (EuclideanSpace.basisFun (Fin 2) ℝ).toBasis⊢ p.ofLp i ∈ Set.Icc 0 1
  rw [unitSquare, show parallelepiped ⇑(EuclideanSpace.basisFun (Fin 2) ℝ) =
    parallelepiped (EuclideanSpace.basisFun (Fin 2) ℝ).toBasis by
      rw [OrthonormalBasis.coe_toBasis], h] at hpp:ℝ²hp:p ∈ {x | ∀ (i : Fin 2), ((EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.repr x) i ∈ Set.Icc 0 1}i:Fin 2h:parallelepiped ⇑(EuclideanSpace.basisFun (Fin 2) ℝ).toBasis =
  {x | ∀ (i : Fin 2), ((EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.repr x) i ∈ Set.Icc 0 1}⊢ p.ofLp i ∈ Set.Icc 0 1
  simpa using hp iAll goals completed! 🐙

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.

@[category test, AMS 49]
theorem isMovingSofa_unitSquare : ∃ m, IsMovingSofa unitSquare m := by⊢ ∃ m, IsMovingSofa unitSquare m
  refine ⟨fun _ => .refl ℝ ℝ², ?_, ?_, continuous_const, rfl, ?_, ?_, ?_⟩refine_1⊢ IsConnected unitSquarerefine_2⊢ IsClosed unitSquarerefine_3⊢ unitSquare ⊆ horizontalHallwayrefine_4⊢ ∀ (t : ↑I), ⇑(AffineIsometryEquiv.refl ℝ ℝ²) '' unitSquare ⊆ hallwayrefine_5⊢ ⇑(AffineIsometryEquiv.refl ℝ ℝ²) '' unitSquare ⊆ verticalHallway
  ·refine_1⊢ IsConnected unitSquare unfold unitSquare parallelepipedrefine_1⊢ IsConnected ((fun t => ∑ i, t i • (EuclideanSpace.basisFun (Fin 2) ℝ) i) '' Set.Icc 0 1)
    refine ⟨⟨0, 0, by⊢ 0 ∈ Set.Icc 0 1 simpAll goals completed! 🐙, by⊢ (fun t => ∑ i, t i • (EuclideanSpace.basisFun (Fin 2) ℝ) i) 0 = 0 simpAll goals completed! 🐙⟩, (convex_Icc _ _).isPreconnected.image _ ?_⟩
    exact (continuous_finset_sum _ fun i _ =>
      (continuous_apply i).smul continuous_const).continuousOnAll goals completed! 🐙
  ·refine_2⊢ IsClosed unitSquare unfold unitSquare parallelepipedrefine_2⊢ IsClosed ((fun t => ∑ i, t i • (EuclideanSpace.basisFun (Fin 2) ℝ) i) '' Set.Icc 0 1)
    exact (isCompact_Icc.image
      (continuous_finset_sum _ fun i _ =>
        (continuous_apply i).smul continuous_const)).isClosedAll goals completed! 🐙
  ·refine_3⊢ unitSquare ⊆ horizontalHallway intro p hprefine_3p:ℝ²hp:p ∈ unitSquare⊢ p ∈ horizontalHallway
    have h0 := mem_Icc_of_mem_unitSquare hp 0refine_3p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0⊢ p ∈ horizontalHallway
    have h1 := mem_Icc_of_mem_unitSquare hp 1refine_3p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ p ∈ horizontalHallway
    exact ⟨p 0, p 1, ⟨h0.2.trans (byp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ 1 ≤ 1 norm_numAll goals completed! 🐙), h1.1, h1.2⟩,
      byp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1] = p ext ihp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1i:Fin 2⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp i = p.ofLp i; fin_cases ih.«0»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h.«0»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) rflAll goals completed! 🐙⟩
  ·refine_4⊢ ∀ (t : ↑I), ⇑(AffineIsometryEquiv.refl ℝ ℝ²) '' unitSquare ⊆ hallway rintro t q ⟨p, hp, rfl⟩refine_4t:↑Ip:ℝ²hp:p ∈ unitSquare⊢ (AffineIsometryEquiv.refl ℝ ℝ²) p ∈ hallway
    rw [show (AffineIsometryEquiv.refl ℝ ℝ²) p = p from rfl]refine_4t:↑Ip:ℝ²hp:p ∈ unitSquare⊢ p ∈ hallway
    refine .inl ?_refine_4t:↑Ip:ℝ²hp:p ∈ unitSquare⊢ p ∈ horizontalHallway
    have h0 := mem_Icc_of_mem_unitSquare hp 0refine_4t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0⊢ p ∈ horizontalHallway
    have h1 := mem_Icc_of_mem_unitSquare hp 1refine_4t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ p ∈ horizontalHallway
    exact ⟨p 0, p 1, ⟨h0.2.trans (byt:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ 1 ≤ 1 norm_numAll goals completed! 🐙), h1.1, h1.2⟩,
      byt:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1] = p ext iht:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1i:Fin 2⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp i = p.ofLp i; fin_cases ih.«0»t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h.«0»t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»t:↑Ip:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) rflAll goals completed! 🐙⟩
  ·refine_5⊢ ⇑(AffineIsometryEquiv.refl ℝ ℝ²) '' unitSquare ⊆ verticalHallway rintro q ⟨p, hp, rfl⟩refine_5p:ℝ²hp:p ∈ unitSquare⊢ (AffineIsometryEquiv.refl ℝ ℝ²) p ∈ verticalHallway
    rw [show (AffineIsometryEquiv.refl ℝ ℝ²) p = p from rfl]refine_5p:ℝ²hp:p ∈ unitSquare⊢ p ∈ verticalHallway
    have h0 := mem_Icc_of_mem_unitSquare hp 0refine_5p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0⊢ p ∈ verticalHallway
    have h1 := mem_Icc_of_mem_unitSquare hp 1refine_5p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ p ∈ verticalHallway
    exact ⟨p 0, p 1, ⟨h0.1, h0.2, h1.2.trans (byp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ 1 ≤ 1 norm_numAll goals completed! 🐙)⟩,
      byp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1] = p ext ihp:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1i:Fin 2⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp i = p.ofLp i; fin_cases ih.«0»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) <;>h.«0»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨0, ⋯⟩) = p.ofLp ((fun i => i) ⟨0, ⋯⟩)h.«1»p:ℝ²hp:p ∈ unitSquareh0:p.ofLp 0 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 0h1:p.ofLp 1 ∈ Set.Icc 0 1 := mem_Icc_of_mem_unitSquare hp 1⊢ !₂[p.ofLp 0, p.ofLp 1].ofLp ((fun i => i) ⟨1, ⋯⟩) = p.ofLp ((fun i => i) ⟨1, ⋯⟩) rflAll goals completed! 🐙⟩

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.

def rotateTranslate (α : Real.Angle) (p : ℝ²) : E(2) :=
  (EuclideanGeometry.o.rotation α).toAffineIsometryEquiv
    |>.trans (AffineIsometryEquiv.vaddConst ℝ p)

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.

def sofaOfRotateTranslatePath (p : ℝ → ℝ²) : Set ℝ² :=
  rotateTranslate 0 (p 0) '' horizontalHallway ∩
  rotateTranslate ↑(π / 2) (p (π / 2)) '' verticalHallway ∩
  ⋂ α ∈ Set.Icc 0 (π / 2), rotateTranslate α (p α) '' hallway


namespace GerversSofa

Eq. 1-4 of [Ro18], which specifies the constants $A$, $B$, $\varphi$, and $\theta$ of [Ge92].

def ABφθSpec (A B φ θ : ℝ) : Prop :=
  0 ≤ φ ∧ φ ≤ θ ∧ θ ≤ π / 4 ∧ 0 ≤ A ∧ 0 ≤ B ∧
  A * (θ.cos - φ.cos) - 2 * B * φ.sin
    + (θ - φ - 1) * θ.cos - θ.sin + φ.cos + φ.sin = 0 ∧
  A * (3 * θ.sin + φ.sin) - 2 * B * φ.cos
    + 3 * (θ - φ - 1) * θ.sin + 3 * θ.cos - φ.sin + φ.cos = 0 ∧
  A * φ.cos - (φ.sin + 1 / 2 - φ.cos / 2 + B * φ.sin) = 0 ∧
  (A + π / 2 - φ - θ) - (B - (θ - φ) * (1 + A) / 2 - (θ - φ)^2 / 4) = 0

There exist unique constants $A$, $B$, $\varphi$, and $\theta$ satisfying the spec.

@[category textbook, AMS 49]
theorem declaration uses 'sorry'ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ,
    ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2 :=
  sorry


def A : ℝ := ABφθSpec.existsUnique.choose.1

def B : ℝ := ABφθSpec.existsUnique.choose.2.1def φ : ℝ := ABφθSpec.existsUnique.choose.2.2.1def θ : ℝ := ABφθSpec.existsUnique.choose.2.2.2


def r (α : ℝ) : ℝ :=
  if α ≤ φ then
    1 / 2
  else if α ≤ θ then
    (1 + A + α - φ) / 2
  else if α ≤ π / 2 - θ then
    A + α - φ
  else if α ≤ π / 2 - φ then
    B - (π / 2 - α - φ) * (1 + A) / 2 - (π / 2 - α - φ) ^ 2 / 4
  else
    0


def y (α : ℝ) : ℝ :=
  ∫ t in α..π / 2 - φ, r t * t.sin


def x (α : ℝ) : ℝ :=
  1 - ∫ t in α..π / 2 - φ, r t * t.cos


def p (α : ℝ) : ℝ² :=
  !2[if α ≤ φ
      then α.cos - 1
      else x (π / 2 - α) * α.cos + y (π / 2 - α) * α.sin - 1,
    if α ≤ π / 2 - φ
      then y α * α.cos - (4 * x 0 - 2 - x α) * α.sin - 1
      else -(4 * x 0 - 3) * α.sin - 1]


end GerversSofa

Gerver's sofa is the sofa according to the rotation path GerversSofa.p.

def gerversSofa : Set ℝ² :=
  sofaOfRotateTranslatePath GerversSofa.p


open MeasureTheory

open scoped ENNReal

The sofa constant is the maximal area of a moving sofa.

def sofaConstant : ℝ≥0∞ := ⨆ (s : Set ℝ²) (_ : ∃ m, IsMovingSofa s m), volume s

The sofa constant is at least 1, as witnessed by the unit square.

@[category test, AMS 49]
theorem one_le_sofaConstant : 1 ≤ sofaConstant := by⊢ 1 ≤ sofaConstant
  calc
    _ = volume unitSquare := (OrthonormalBasis.volume_parallelepiped _).symm
    _ ≤ sofaConstant := le_iSup₂ (α := ℝ≥0∞) unitSquare isMovingSofa_unitSquare

What is the sofa constant?

@[category research solved, AMS 49]
theorem declaration uses 'sorry'sofaConstant_eq : sofaConstant = answer(sorry) := by⊢ sofaConstant = sorry
  sorryAll goals completed! 🐙

Gerver's sofa attains the sofa constant, conjectured by [Ge92] and claimed by [Ba24].

@[category research solved, AMS 49]
theorem declaration uses 'sorry'sofaConstant_eq_volume_gerversSofa : sofaConstant = volume gerversSofa := by⊢ sofaConstant = volume gerversSofa
  sorryAll goals completed! 🐙

Gerver's sofa is the unique sofa that attains the sofa constant.

@[category research open, AMS 49]
theorem declaration uses 'sorry'sofaConstant_eq_volume_iff_eq_gerversSofa :
    ∀ s : Set ℝ², sofaConstant = volume s ↔ s = gerversSofa := by⊢ ∀ (s : Set ℝ²), sofaConstant = volume s ↔ s = gerversSofa
  sorryAll goals completed! 🐙


end MovingSofa