The rotation path of a maximum-area sofa satisfies the injectivity condition
OpenGerver.injectivityThe rotation path of a balanced maximum sofa of rotation angle π/2 that attains the maximum sofa area satisfies the injectivity condition: it is continuously differentiable, and on the open interval (0, π/2) its derivative points strictly against the inner wall direction u_t and strictly along the outer wall direction v_t. Geometrically, the contact path of a maximizer never loops back on itself — it sweeps monotonically through the turn. The formal statement abridges the source's injectivity condition by dropping its auxiliary clause on the boundary curve σ_K, keeping the continuous differentiability and the two strict derivative inequalities, which are what the endgame's dominating argument consumes.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Step 2 (Theorem 1.7.1 / Theorem 6.1.1): the rotation path of a balanced
maximum sofa of rotation angle π/2 attaining the maximum area satisfies the
injectivity condition — it is continuously differentiable, and its derivative
points strictly against u_t and along v_t on (0, π/2), so the rotation path
makes no self-loop. -/
theorem injectivity (S : Set (ℝ × ℝ)) (X : ℝ → ℝ × ℝ)
(hbal : IsBalancedMaximumSofa S (Real.pi / 2)) (hmax : area S = sofaMax)
(hsup : IsSupportingPathOf X (Real.pi / 2)) (hmono : S = sofaOfPath X (Real.pi / 2)) :
SatisfiesInjectivity 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 planar set S and every curve X of planar points, if S is a balanced maximum sofa of angle π/2, the area of S equals the maximum sofa area, X is a supporting rotation path of angle π/2, and S equals the monotone sofa determined by X, then X satisfies the injectivity condition — X is continuously differentiable, and at every interior parameter t of (0, π/2) the derivative of X has strictly negative inner product with the vector u t and strictly positive inner product with the vector v t.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.