A balanced maximum sofa of large area can be turned through the full right angle
OpenGerver.rotation_angle_rightA balanced maximum sofa of area at least 2.2 whose rotation angle lies between arccos(1/2.2) and π/2 has a rotated copy that admits a movement of rotation angle π/2. This is the reduction that confines the endgame to sofas moving through the full right angle: since the sofa area is known to be at least 2.2195... by Gerver's construction, any balanced maximum sofa of large area can be rigidly rotated so that its supporting movement turns the full π/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.2): a balanced maximum sofa of area at least 2.2 and
rotation angle in [sec⁻¹(2.2), π/2] has a rotated copy that admits a movement
of rotation angle π/2. -/
theorem rotation_angle_right (S : Set (ℝ × ℝ)) {ω : ℝ}
(hbal : IsBalancedMaximumSofa S ω) (hmov : HasMovementAngle S ω)
(ha : 2.2 ≤ area S)
(hω : Real.arccos (1 / 2.2) ≤ ω ∧ ω ≤ Real.pi / 2) :
∃ δ, HasMovementAngle ((fun p => rot δ p) '' S) (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 planar set S and every real number ω, if S is a balanced maximum sofa of angle ω that admits a movement of rotation angle ω, the area of S is at least 2.2, and ω lies in the closed interval between arccos(1/2.2) and π/2, then there exists a real number δ such that the image of S under rotation by the angle δ admits a movement of rotation angle π/2.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.