Every moving sofa sits in a monotone moving sofa
DisprovedGerver.monotone_containerFor every moving sofa S there is a moving sofa T that is monotone — an intersection of strips and hallways arising from a rotation path of some angle ω ∈ (0, π/2] — that contains S and has area at least the area of S. This is the reduction of the moving sofa problem to monotone sofas: the intersection I(S) of the supporting hallways of S is itself a moving sofa containing S, and area is monotone under inclusion.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 1a (Theorem 2.3.2 and Theorem 2.4.4): every moving sofa is contained
in a monotone moving sofa of at least its own area. The intersection I(S) of
the supporting hallways of S is a moving sofa that contains S, so a
maximum-area moving sofa can be assumed monotone. -/
theorem monotone_container (S : Set (ℝ × ℝ)) (hS : IsMovingSofa S) :
∃ T, IsMonotoneSofa T ∧ IsMovingSofa T ∧ S ⊆ T ∧ area S ≤ area T := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every set S of pairs of real numbers that is a moving sofa (nonempty, compact, connected, and able to move around the corner of the hallway by a continuous path of orientation-preserving rigid motions), there exists a set T such that four things hold: T is a monotone sofa, meaning T equals the intersection of the two strips and a family of hallways determined by some rotation path with some angle ω with 0 < ω ≤ π/2; T is itself a moving sofa; S is a subset of T; and the area of S is at most the area of T. No hypothesis on S beyond its being a moving sofa is assumed.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.