Balanced maximum sofas exist for each rotation angle
OpenGerver.balanced_maximum_existsFor every rotation angle ω ∈ (0, π/2] there exists a moving sofa S that is a balanced maximum sofa of angle ω — the Hausdorff limit of maximum polygon sofas whose uniform angle sets Θ_{ω,n_i} run over a strictly increasing sequence of powers of two — such that S admits a movement of rotation angle ω and the area of S equals the maximum area m_ω of a moving sofa admitting such a movement. This is the limit construction that turns Gerver's balancing argument into an actual maximizer: maximum polygon sofas are balanced, and their limit is a genuine moving sofa attaining the supremum.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 1b (Theorem 3.5.2 and Theorem 3.5.6): for every rotation angle
ω ∈ (0, π/2] there is a balanced maximum sofa of rotation angle ω, and it
attains the maximum area among all moving sofas admitting a movement of
rotation angle ω. -/
theorem balanced_maximum_exists (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) :
∃ S, IsBalancedMaximumSofa S ω ∧ HasMovementAngle S ω ∧ area S = angleMax ω := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every real number ω with 0 < ω and ω ≤ π/2, there exists a set S of planar points such that three things hold. S is a balanced maximum sofa of angle ω: a moving sofa for which there is a sequence of natural numbers n, each at least two and a strictly increasing sequence of powers of two, and a sequence of sets F, where each F i is a maximum-area polygon sofa with uniform angle set Θ_{ω,n i} (an intersection of the two strips with hallways of angles iω/n i, translated by corner maps, maximal in area among all such translations), such that F converges to S in the Hausdorff sense — for every positive ε the sets F i and S eventually lie in each other's ε-neighborhoods. S admits a movement of rotation angle ω. And the area of S equals angleMax ω, the supremum of the areas of moving sofas admitting a movement of rotation angle ω.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.