Big sofas turn most of the right angle
OpenGerver.rotation_angle_rangeEvery moving sofa of area at least 2.2 admits a movement whose rotation angle — the total clockwise turn of the movement — lies between sec⁻¹(2.2) and π/2. This is Gerver's bound: a sofa too large to fit in the intersection of two strips at a shallow angle must rotate through nearly the full right angle. Combined with Gerver's sofa of area 2.2195..., it restricts the rotation angle of a maximum-area sofa to [sec⁻¹(2.2), π/2].
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 1c (Theorem 1.5.1, Gerver): a moving sofa of area at least 2.2 admits
a movement whose rotation angle lies between sec⁻¹(2.2) and π/2. -/
theorem rotation_angle_range (S : Set (ℝ × ℝ)) (hS : IsMovingSofa S)
(ha : 2.2 ≤ area S) :
∃ ω, HasMovementAngle S ω ∧ Real.arccos (1 / 2.2) ≤ ω ∧ ω ≤ Real.pi / 2 := 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 planar points that is a moving sofa, if the area of S is at least the real number 2.2, then there exist a real number ω and a movement of S — a continuous path of orientation-preserving rigid motions starting at a translation that puts S into the horizontal side of the hallway, staying inside the hallway, and ending inside the vertical side — whose total clockwise rotation equals ω, with the arccosine of 1/2.2 at most ω and ω at most π/2.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.