Some Gerver sofa dominates every injectivity-constrained rotation path
OpenGerver.q_upper_boundSome Gerver sofa dominates in area every moving sofa whose supporting rotation path of angle π/2 satisfies the injectivity condition. This is the concavity argument at the heart of the proof: the area upper bound Q of the source is a concave functional on a convex domain of triples of convex bodies, it coincides with the sofa area at the Gerver sofa, and the Gerver sofa is its global maximizer — so every sofa meeting the injectivity condition is bounded above by a Gerver sofa in area.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 3 (Sections 1.8.2-1.8.3; Theorem 8.3.8, Theorem 8.5.7 and
Theorem 8.4.6): some Gerver sofa dominates in area every moving sofa whose
supporting rotation path of angle π/2 satisfies the injectivity condition.
This is the concavity argument: the area upper bound Q is a concave
functional on the convex domain of convex-body triples, it matches the sofa
area at the Gerver sofa, and the Gerver sofa is its global maximizer. -/
theorem q_upper_bound :
∃ G, IsGerverSofa G ∧ ∀ (X : ℝ → ℝ × ℝ), SatisfiesInjectivity X →
IsSupportingPathOf X (Real.pi / 2) → IsMovingSofa (sofaOfPath X (Real.pi / 2)) →
area (sofaOfPath X (Real.pi / 2)) ≤ area G := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: there exists a planar set G satisfying the Gerver sofa structure such that for every curve X of planar points, if X satisfies the injectivity condition, X is a supporting rotation path of angle π/2, and the monotone sofa determined by X at angle π/2 is a moving sofa, then the area of that monotone sofa is at most the area of G.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.