A moving monotone sofa is its cap minus its niche
ProvedGerver.sofa_cap_nicheLet x be a supporting rotation path of angle ω ∈ (0, π/2] whose monotone sofa sofaOfPath x ω is a moving sofa. Then the monotone sofa equals its cap minus its niche — the cap being the part of the parallelogram P_ω cut out by the outer quarter-planes, the niche the part of the fan swept by the inner quarter-planes — and the niche lies inside the cap. Together with the area-functional milestone this identifies the moving sofa with its cap, the sofa problem becoming the maximization of |K| - |N(K)| over caps K.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 1a (Theorem 2.4.2 and Theorem 2.5.9): a moving monotone sofa with a
supporting rotation path is its cap minus its niche, and the niche lies
inside the cap. -/
theorem sofa_cap_niche (x : ℝ → ℝ × ℝ) {ω : ℝ} (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2)
(hsup : IsSupportingPathOf x ω) (hm : IsMovingSofa (sofaOfPath x ω)) :
sofaOfPath x ω = capOf x ω \ nicheOf x ω ∧ nicheOf x ω ⊆ capOf x ω := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every curve x of planar points and every real number ω with 0 < ω and ω ≤ π/2, if x is a supporting rotation path of angle ω (x is continuous, and for every t between 0 and ω both outer walls of the hallway with inner corner x(t) touch the intersection sofaOfPath x ω) and that intersection is a moving sofa, then two conclusions hold. First, the intersection of the strips and hallways determined by x equals the set difference of the cap of x (the part of the parallelogram cut out by the closed outer quarter-planes) and the niche of x (the part of the fan swept by the open inner quarter-planes). Second, the niche of x is a subset of the cap of x.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.