The sofa area functional: cap minus niche
ProvedGerver.area_functionalWhenever the niche of a rotation path lies inside its cap, the area of the monotone sofa of the path is exactly the area of the cap minus the area of the niche. This is the sofa area functional A_ω(K) = |K| - |N(K)| of the source, the maximization of which over caps K is the moving sofa problem restated.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 1a (Section 1.2.2): the area of a monotone sofa is the area of its
cap minus the area of its niche — the sofa area functional
A_ω(K) = |K| - |N(K)|, whenever the niche lies inside the cap. -/
theorem area_functional (x : ℝ → ℝ × ℝ) (ω : ℝ)
(hsub : nicheOf x ω ⊆ capOf x ω) :
area (sofaOfPath x ω) = area (capOf x ω) - area (nicheOf 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 ω, if the niche of x (the part of the fan swept by the open inner quarter-planes over t ∈ [0, ω]) is a subset of the cap of x (the part of the parallelogram cut out by the closed outer quarter-planes over the same angles), then the area of the monotone sofa determined by x — the intersection of the strips and hallways — equals the real number obtained by subtracting the area of the niche from the area of the cap.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.