Moving sofa: related mathematical developments

• Gerver.Applications.Development004.
• Bounds.Applications.Development003.
• Sofa.Applications.Development001.
• Motion.Applications.Development001.
• Sofa.Applications.Development002.
• Sofa.Applications.Development003.
• Motion.Applications.Development002.
• Main.

Moving sofa: related mathematical developments

• Gerver.Niche.Orientation.
• Gerver.ContactGeometry.
• Gerver.TailGeometry.
• Gerver.MeasureTranslation.
• Gerver.PhaseMeasures.
• Gerver.PhaseIntegration.
• Gerver.QMatch.
• Gerver.QVariation.

Orientation of the certified Gerver niche boundary

The niche of the certified Gerver outer cap is the strict region under the niche roof, and the roof is the graph of a continuous height function f over the horizontal extent [gerverNicheLeft, gerverNicheRight] of the roof (exists_gerverRoofHeight). The closure of the niche is therefore the closed subgraph of f, its interior the open subgraph, and the counterclockwise loop positiveGraphLoop around that region traces their common frontier.

gerverNicheBoundary is the explicit four-piece traversal of that frontier: the second contact curve reversed, the ambient path forwards, the fourth contact curve reversed, and the base segment. It runs backwards along the roof through a decreasing piecewise affine parameter change (gerverBoundaryParam), so it is the positive-graph loop reparametrized by an increasing map (gerverNicheBoundary_orientedJordan). The main result gerver_niche_orientation collects the consequences: the traversal is a continuous path of bounded variation, a counterclockwise Jordan parametrization of the frontier of the closed niche, its signed curve area is the area of the niche, and no roof point lies in the niche.

The same description of the niche as the strict region under the roof settles the opposite inclusion for the fourth boundary piece: every interior point of the base segment does lie in the niche (gerver_bottom_segment_mem_gerverLiteralNiche).

The roof as the graph of a continuous height function

The literal niche is the strict region under the roof

noncomputable def MovingSofa.gerverNicheBoundary (s : ↑(Set.Icc 0 4)) : Point

The closed boundary parametrization of the Gerver niche.

Equations

• One or more equations did not get rendered due to their size.

The four-piece traversal of the niche boundary

theorem MovingSofa.gerverNicheBoundary_of_le_one {s : ℝ} (hs : s ∈ Set.Icc 0 4) (h : s ≤ 1) : gerverNicheBoundary ⟨s, hs⟩ = paperGerverContacts (Real.pi / 2 - (Real.pi / 2 - gerverStageTimes 3) * s) 1

On its first piece the niche traversal runs backwards along the second contact curve B, from B (π / 2) at s = 0 to B t₃ at s = 1.

theorem MovingSofa.gerverNicheBoundary_mid {s : ℝ} (hs : s ∈ Set.Icc 0 4) (h1 : 1 ≤ s) (h2 : s ≤ 2) : gerverNicheBoundary ⟨s, hs⟩ = paperGerverPath (gerverStageTimes 1 + (gerverStageTimes 4 - gerverStageTimes 1) * (s - 1))

On its second piece the niche traversal runs forwards along the direct Gerver path, from x t₁ at s = 1 to x t₄ at s = 2.

theorem MovingSofa.gerverNicheBoundary_third {s : ℝ} (hs : s ∈ Set.Icc 0 4) (h1 : 2 ≤ s) (h2 : s ≤ 3) : gerverNicheBoundary ⟨s, hs⟩ = paperGerverContacts (gerverStageTimes 2 * (3 - s)) 3

On its third piece the niche traversal runs backwards along the fourth contact curve D, from D t₂ at s = 2 to D 0 at s = 3.

theorem MovingSofa.gerverNicheBoundary_base {s : ℝ} (hs : s ∈ Set.Icc 0 4) (h : 3 ≤ s) : gerverNicheBoundary ⟨s, hs⟩ = (4 - s) • paperGerverContacts 0 3 + (s - 3) • paperGerverContacts (Real.pi / 2) 1

On its last piece the niche traversal runs along the base segment of the niche, from D 0 at s = 3 to B (π / 2) at s = 4.

The traversal is the roof, run backwards

theorem MovingSofa.gerver_niche_orientation : ∃ (K : RightAngleCapSpace), ↑↑K = gerverOuterCap ∧ ∃ (Γ : ContinuousBVPaths 0 4), ↑Γ = gerverNicheBoundary ∧ IsOrientedJordanParametrization gerver_niche_orientation._proof_1 (frontier (closure (capNiche K))) true ↑Γ ∧ closure (capNiche K) = jordanInterior (Set.range ↑Γ) ∪ Set.range ↑Γ ∧ ClassicalResults.area (closure (capNiche K)) = ClassicalResults.area (capNiche K) ∧ curveAreaFunctional Γ = ClassicalResults.area (capNiche K) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 3) (gerverStageTimes 5), paperGerverContacts t 1 ∉ capNiche K) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 1) (gerverStageTimes 4), paperGerverPath t ∉ capNiche K) ∧ ∀ t ∈ Set.Icc (gerverStageTimes 0) (gerverStageTimes 2), paperGerverContacts t 3 ∉ capNiche K

The interior of the base segment

theorem MovingSofa.gerver_niche_bottom_ends_ne : paperGerverContacts 0 3 ≠ paperGerverContacts (Real.pi / 2) 1

The two ends of the base segment of the niche boundary are distinct: they are the images of the parameters 3 and 0 of the boundary traversal, which is injective on [0, 4).

theorem MovingSofa.gerver_bottom_segment_mem_gerverLiteralNiche {a : ℝ} (ha : a ∈ Set.Ioo 0 1) : (1 - a) • paperGerverContacts 0 3 + a • paperGerverContacts (Real.pi / 2) 1 ∈ gerverLiteralNiche

Every interior point of the base segment of the niche boundary, which runs from D(0) to B(π/2), lies in the literal Gerver niche. Both ends sit on the wall, so the segment is horizontal and its interior points have strictly intermediate horizontal coordinate; the intermediate value theorem then puts a roof point directly above such a point, where the roof has strictly positive height, and the description of the niche as the strict region under the roof concludes.

The contact geometry of the paper Gerver sofa

Gerver's sofa is a monotone sofa, and its right-angle cap has all the contact geometry the upper-bound argument reads off a monotone sofa: selected cap vertices and inner corner given by the paper's curves A, C and x, a counterclockwise Jordan traversal of the niche boundary, the interior of the base segment inside the niche and the three roof pieces outside it, the two inner contact curves on the two inner walls of the supporting hallway, and the signs of their stage speeds along the frame directions.

Every clause is about one and the same cap. The cap is taken from paperGerverCap_injectivity — which also supplies the density hypothesis that makes the selected contacts well defined — and the caps produced by cap-support identification, niche identification and niche orientation are identified with it through their common carrier gerverOuterCap. The clauses themselves are then assembled from the identification theorems together with gerver_bottom_segment_mem_gerverLiteralNiche, the frame descriptions mem_rotatingHallwayParts_bRay_iff and mem_rotatingHallwayParts_dRay_iff of the two inner walls, the closed-interval velocity signs paperGerverVelocityComponents_fst_nonpos and paperGerverVelocityComponents_snd_nonneg, and the stage speeds hasDerivWithinAt_paperGerverContacts_one_neg_smul and hasDerivWithinAt_paperGerverContacts_three_pos_smul.

theorem MovingSofa.paperGerver_contact_geometry : IsMonotoneSofa paperGerverSofa ∧ ∃ (K : RightAngleCapSpace), ↑↑K = capOfSofa paperGerverSofa (Real.pi / 2) ∧ ∃ (hK : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s), (∀ (t : ↑(Set.Icc 0 (Real.pi / 2))), (nondegenerateCapData K hK).1.1 t = paperGerverContacts (↑t) 0 ∧ (nondegenerateCapData K hK).1.2 t = paperGerverContacts (↑t) 2 ∧ capInnerCorner K ↑t = paperGerverPath ↑t) ∧ (∃ (Γ : ContinuousBVPaths 0 4), ↑Γ = gerverNicheBoundary ∧ IsOrientedJordanParametrization gerver_niche_orientation._proof_1 (frontier (closure (capNiche K))) true ↑Γ ∧ closure (capNiche K) = jordanInterior (Set.range ↑Γ) ∪ Set.range ↑Γ ∧ ClassicalResults.area (closure (capNiche K)) = ClassicalResults.area (capNiche K)) ∧ (∀ a ∈ Set.Ioo 0 1, (1 - a) • paperGerverContacts 0 3 + a • paperGerverContacts (Real.pi / 2) 1 ∈ capNiche K) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 3) (gerverStageTimes 5), paperGerverContacts t 1 ∉ capNiche K ∧ paperGerverContacts t 1 ∈ (rotatingHallwayParts ↑↑K ↑t).bRay) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 1) (gerverStageTimes 4), paperGerverPath t ∉ capNiche K) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 0) (gerverStageTimes 2), paperGerverContacts t 3 ∉ capNiche K ∧ paperGerverContacts t 3 ∈ (rotatingHallwayParts ↑↑K ↑t).dRay) ∧ (∀ (i : Fin 5), i = 3 ∨ i = 4 → ∀ t ∈ gerverStageIntervals i, ∃ c < 0, HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 1) (c • tangentVector ↑t) (gerverStageIntervals i) t) ∧ ∀ (i : Fin 5), i = 0 ∨ i = 1 → ∀ t ∈ gerverStageIntervals i, ∃ (c : ℝ), 0 < c ∧ HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 3) (c • normalVector ↑t) (gerverStageIntervals i) t

The left and right tails of the Gerver cap

gerver_tailGeometry identifies the two tails cut out of the Gerver cap by the inner hallway walls. Each tail is cut out by a one-parameter family of supporting half-planes whose contact points are the two inner Gerver contact curves B and D, so the envelope-tangency lemmas of MovingSofa/Convex/EnvelopeFace.lean identify every intervening face of a tail with a single point of the corresponding contact curve, and the stagewise monotonicity of the contact curves against a fixed frame direction (MovingSofa/Gerver/StageRegularity.lean) supplies both the containment of the contact curves in the tails and the injectivity of the two parametrizations. The support sums are the cut identity h_L (s + π) = -m s.

def MovingSofa.ParametrizesDirectedArc (f : ℝ → Point) (a b : ℝ) (Γ : DirectedArcData) : Prop

A continuous injective parametrization traces the directed arc with the specified endpoints.

Equations

• MovingSofa.ParametrizesDirectedArc f a b Γ = (a < b ∧ ContinuousOn f (Set.Icc a b) ∧ Set.InjOn f (Set.Icc a b) ∧ f '' Set.Icc a b = Γ.carrier ∧ f a = Γ.startPoint ∧ f b = Γ.endPoint)

theorem MovingSofa.gerver_tailGeometry (K : SpecialCapSpace) (B D : ConvexBody Point) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) (hB : ↑B = (canonicalTailSets K).1) (hD : ↑D = (canonicalTailSets K).2) : (∀ t ∈ Set.Ioo (gerverStageTimes 0) (gerverStageTimes 2), edgeVertices D ↑(3 * Real.pi / 2 + t) = (paperGerverContacts t 3, paperGerverContacts t 3)) ∧ (∀ t ∈ Set.Ioo (gerverStageTimes 3) (gerverStageTimes 5), edgeVertices B ↑(Real.pi + t) = (paperGerverContacts t 1, paperGerverContacts t 1)) ∧ (distinguishedCapSides ↑K).2.corner = paperGerverContacts (gerverStageTimes 2) 3 ∧ (rightLeftTailArcs B D).2.endPoint = paperGerverContacts (gerverStageTimes 2) 3 ∧ edgeVertices D ↑(3 * Real.pi / 2 + gerverStageTimes 2) = (paperGerverContacts (gerverStageTimes 2) 3, paperGerverContacts (gerverStageTimes 2) 3) ∧ ParametrizesDirectedArc (fun (t : ℝ) => paperGerverContacts t 3) (gerverStageTimes 0) (gerverStageTimes 2) (rightLeftTailArcs B D).2 ∧ (distinguishedCapSides ↑K).1.corner = paperGerverContacts (gerverStageTimes 3) 1 ∧ (rightLeftTailArcs B D).1.startPoint = paperGerverContacts (gerverStageTimes 3) 1 ∧ edgeVertices B ↑(Real.pi + gerverStageTimes 3) = (paperGerverContacts (gerverStageTimes 3) 1, paperGerverContacts (gerverStageTimes 3) 1) ∧ ParametrizesDirectedArc (fun (t : ℝ) => paperGerverContacts t 1) (gerverStageTimes 3) (gerverStageTimes 5) (rightLeftTailArcs B D).1 ∧ (∀ t ∈ Set.Icc (gerverStageTimes 0) (gerverStageTimes 2), supportValue ↑↑↑K ↑(Real.pi / 2 + t) + supportValue ↑D ↑(3 * Real.pi / 2 + t) = 1) ∧ ∀ t ∈ Set.Icc (gerverStageTimes 3) (gerverStageTimes 5), supportValue ↑↑↑K ↑t + supportValue ↑B ↑(Real.pi + t) = 1

The four contact densities of Gerver's cap

The rotating frame reads the four contact curves of Gerver's sofa as angular densities of two surface measures: the two outer contacts A, C against the cap K = C(G) itself, and the two inner contacts B, D against the two tail bodies through the opposite surface measure.

The two outer clauses are exactly the certified cap densities gerver_surface_densities, rewritten with the tautological identity ⟨r • v_t, v_t⟩ = r and translated by the quarter turn that separates the A arc from the C arc. The two inner clauses use that B = A - u and D = C - v are the outer contacts translated by a frame vector, so each closed stage carries a globally differentiable branch curve for them (exists_branch_paperGerverContacts_one, exists_branch_paperGerverContacts_three); the tail geometry identifies those curves with the positive vertices of the two tail bodies at the opposite normal, and oppositeSurfaceData_angleImage_eq_withDensity turns each stage into a Lebesgue density. The stages are glued with measure_angleImage_eq_of_union, which puts every interior switch inside a window that is closed on the right, so the only atom to compute is the one at the included left endpoint t₃ of the B arc.

noncomputable def MovingSofa.angularDensityMeasure (f : ℝ → ℝ) (S : Set ℝ) : MeasureTheory.Measure Real.Angle

Push a real density measure on an angle window to angles modulo a full turn.

Equations

• MovingSofa.angularDensityMeasure f S = MeasureTheory.Measure.map (fun (t : ℝ) => ↑t) ((MeasureTheory.volume.restrict S).withDensity fun (t : ℝ) => ENNReal.ofReal (f t))

def MovingSofa.HasAngularDensity (μ : MeasureTheory.Measure Real.Angle) (f : ℝ → ℝ) (S : Set ℝ) : Prop

The measure has the specified integrable nonnegative density on the angular image of a window.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.HasAngularDensity.angleImage_eq_setLIntegral {μ : MeasureTheory.Measure Real.Angle} {f : ℝ → ℝ} {S : Set ℝ} (h : HasAngularDensity μ f S) {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (hS : S ⊆ Set.Ioc a b) {T : Set ℝ} (hT : MeasurableSet T) (hTS : T ⊆ S) : μ ((fun (t : ℝ) => ↑t) '' T) = ∫⁻ (t : ℝ) in T, ENNReal.ofReal (f t)

An angular density identity on a window of at most one turn computes the measure of the angular image of every measurable subset of the window.

theorem MovingSofa.gerver_measureTranslation (K : SpecialCapSpace) (B D : ConvexBody Point) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) (hB : ↑B = (canonicalTailSets K).1) (hD : ↑D = (canonicalTailSets K).2) : HasAngularDensity (surfaceAreaMeasure ↑↑K) (fun (t : ℝ) => inner ℝ (deriv (fun (s : ℝ) => paperGerverContacts s 0) t) (tangentVector ↑t)) (Set.Ico 0 (Real.pi / 2)) ∧ HasAngularDensity (oppositeSurfaceData B).1 (fun (t : ℝ) => inner ℝ (-deriv (fun (s : ℝ) => paperGerverContacts s 1) t) (tangentVector ↑t)) (Set.Ico (gerverStageTimes 3) (gerverStageTimes 5)) ∧ HasAngularDensity (surfaceAreaMeasure ↑↑K) (fun (t : ℝ) => inner ℝ (-deriv (fun (s : ℝ) => paperGerverContacts s 2) (t - Real.pi / 2)) (normalVector ↑(t - Real.pi / 2))) (Set.Ioc (Real.pi / 2) Real.pi) ∧ HasAngularDensity (oppositeSurfaceData D).1 (fun (t : ℝ) => inner ℝ (deriv (fun (s : ℝ) => paperGerverContacts s 3) (t - Real.pi / 2)) (normalVector ↑(t - Real.pi / 2))) (Set.Ioc (Real.pi / 2 + gerverStageTimes 0) (Real.pi / 2 + gerverStageTimes 2))

The eight phase identities of Gerver's cap

The ten Gerver phase intervals cut the angular window [0, π] at the five stage times and at their reflections. On each of them the surface-area measure of the cap K = C(G) of Gerver's sofa is one of: zero, the inner-corner measure ι_K, the opposite surface measure of one of the two tail bodies, or a sum of the last two (gerver_phaseMeasures).

Every clause is proved set-wise. The translated-measure proposition gerver_measureTranslation presents the surface measure of the cap and the two opposite tail measures as angular densities on the two half-windows, so each of them gives the angular image of a measurable subset of a phase interval the Lebesgue integral of the corresponding contact derivative (HasAngularDensity.angleImage_eq_setLIntegral), and the corner measure does the same with its own density (capCornerAngleMeasure_angleImage_eq_setLIntegral). The five stagewise contact equations gerver_stageODEs identify those densities on the interior of each stage, which is almost all of it, and Real.Angle.measure_restrict_image_congr_of_ae_eq turns an almost-everywhere identity of densities into an equality of the restricted measures. No atom computation at the included stage endpoints is needed: a single parameter is Lebesgue-null and the four measures are only ever evaluated through their densities.

def MovingSofa.gerverPhaseAngles (j : Fin 10) : Set Real.Angle

The angular image of one of the ten phase intervals.

Equations

• MovingSofa.gerverPhaseAngles j = (fun (t : ℝ) => ↑t) '' MovingSofa.gerverPhaseIntervals j

def MovingSofa.GerverPhaseMeasureIdentities (K : SpecialCapSpace) (B D : ConvexBody Point) : Prop

The phase-by-phase surface-measure identities relating the cap, corner and two tail bodies.

Equations

• One or more equations did not get rendered due to their size.

The corner density of the cap of Gerver's sofa

On each of the two open quarter turns the inner corner of the cap is the direct Gerver path (derivWithin_capInnerCorner_eq_deriv_paperGerverPath), so the two branches of capCornerDensity are the two velocity components β and -α of that path.

theorem MovingSofa.capCornerDensity_eq_velocity_tangential (K : SpecialCapSpace) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) {s : ℝ} (hs : s ∈ Set.Ioo 0 (Real.pi / 2)) : capCornerDensity K s = (paperGerverVelocityComponents s).2

On the first open quarter turn the corner density of the cap of Gerver's sofa is the tangential velocity component of the direct Gerver path.

theorem MovingSofa.capCornerDensity_eq_neg_velocity_normal (K : SpecialCapSpace) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) {s : ℝ} (hs : s ∈ Set.Ioo (Real.pi / 2) Real.pi) : capCornerDensity K s = -(paperGerverVelocityComponents (s - Real.pi / 2)).1

On the second open quarter turn the corner density of the cap of Gerver's sofa is minus the normal velocity component of the direct Gerver path, at the parameter shifted by a quarter turn.

theorem MovingSofa.gerver_phaseMeasures (K : SpecialCapSpace) (B D : ConvexBody Point) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) (hB : ↑B = (canonicalTailSets K).1) (hD : ↑D = (canonicalTailSets K).2) : GerverPhaseMeasureIdentities K B D

Integrating the variation of 𝒬 over the Gerver phases

The ten phase windows gerverPhaseAngles j partition the angular window [0, π] except for the single angle π/2, and six of them cover the domain of the inner-corner measure except for two angles. Since the cap surface measure integrates a continuous integrand and the corner measure has no atoms, qVariationIntegral_eq_phaseSum rewrites the four integrals of the variation formula as the eight contributions of the source table (gerverPhaseContribution), grouped so that gerver_phaseMeasures applies to each of them.

gerverPhaseContribution_nonpos then signs each contribution. Six of the eight vanish or cancel outright against the corner measure; on the two active right windows and the two active left windows the phase identities turn the remaining cap measure into the tail measure, and the resulting integrand is the difference between the competitor's support sum and the base support sum, which is ≤ 1 - 1 = 0 by the cap-tail constraints.

The angular phase windows are measurable

theorem MovingSofa.measurableSet_gerverPhaseAngles (j : Fin 10) : MeasurableSet (gerverPhaseAngles j)

Each of the ten angular phase windows of Gerver's cap is a Borel set.

The phase windows partition the upper half-circle

theorem MovingSofa.gerverPhaseAngles_three_union_four : gerverPhaseAngles 3 ∪ gerverPhaseAngles 4 = (fun (t : ℝ) => ↑t) '' Set.Ico (Real.pi / 2 - GerversSofa.θ) (Real.pi / 2)

The two active right-tail phases make up the angular window [π/2 - θ, π/2).

theorem MovingSofa.gerverPhaseAngles_five_union_six : gerverPhaseAngles 5 ∪ gerverPhaseAngles 6 = (fun (t : ℝ) => ↑t) '' Set.Ioc (Real.pi / 2) (Real.pi / 2 + GerversSofa.θ)

The two active left-tail phases make up the angular window (π/2, π/2 + θ].

Splitting the four variation integrals over the phase windows

The eight phase contributions of the variation integral

noncomputable def MovingSofa.gerverPhaseContribution (X Y : CapTailSpace) : Fin 8 → ℝ

The eight contributions of the source table of the variation of 𝒬: on each group of phases, the cap surface integral of the support difference, minus the active inner-corner integral, plus the active tail integral of the tail support difference.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.gerverPhaseContribution_nonpos (X Y : CapTailSpace) (hphase : GerverPhaseMeasureIdentities X.cap X.rightBody X.leftBody) (hbaseB : ∀ t ∈ gerverPhaseAngles 3 ∪ gerverPhaseAngles 4, supportValue (↑↑↑X.cap) t + (oppositeSurfaceData X.rightBody).2 t = 1) (hbaseD : ∀ t ∈ gerverPhaseAngles 5 ∪ gerverPhaseAngles 6, supportValue (↑↑↑X.cap) t + (oppositeSurfaceData X.leftBody).2 t = 1) (i : Fin 8) : gerverPhaseContribution X Y i ≤ 0

Each of the eight phase contributions is nonpositive: the phase measure identities cancel the cap measure against the active corner and tail measures, and the cap-tail constraints sign the remaining tail integrands.

The four variation integrals as the eight phase contributions

theorem MovingSofa.qVariationIntegral_eq_phaseSum (X Y : CapTailSpace) (hinactiveB : (oppositeSurfaceData X.rightBody).1 ((fun (s : ℝ) => ↑s) '' Set.Ioo paperGerverConstants.2.1 (Real.pi / 2 - GerversSofa.θ)) = 0) (hinactiveD : (oppositeSurfaceData X.leftBody).1 ((fun (s : ℝ) => ↑s) '' Set.Ioo (Real.pi / 2 + GerversSofa.θ) (Real.pi / 2 + paperGerverConstants.2.2)) = 0) : qVariationIntegral X Y = ∑ i : Fin 8, gerverPhaseContribution X Y i

The four integrals of the variation formula regroup into the eight contributions of the source table, given that the two tails carry no surface measure between their active windows.

Gerver's cap attains the upper bound Q

gerver_upperBoundQ_matches evaluates the upper-bound functional Q at the cap of Gerver's sofa together with its two canonical tails, and finds the sofa area functional A there.

The niche area is read off the four-piece counterclockwise traversal of the niche boundary (gerver_niche_orientation): additivity of the curve area functional over that traversal (curveArea_concatenation) expresses the niche area as the curve area of the middle corner path minus the curve areas of the two inner contact curves, because the two contact pieces are traversed backwards and the base segment lies on the line y = 0. The tail geometry (gerver_tailGeometry) identifies the two contact curves with the two convex tail arcs, so their curve areas are the two convexArcArea terms of Q, and it identifies the two corners of Q's connector segments, whose signed areas therefore vanish.

The four-piece traversal of the niche boundary

The niche area of the Gerver cap

theorem MovingSofa.gerver_capNiche_area_eq (K : SpecialCapSpace) (hK : ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) : ClassicalResults.area (capNiche ↑K) = curveAreaFunctional (capMiddleBV K) - curveAreaFunctional gerverRightContactBV - curveAreaFunctional gerverLeftContactBV

The niche area of the Gerver cap, in terms of the signed curve areas of the three nondegenerate pieces of its boundary traversal: the middle corner path, and the two inner contact curves, which the traversal runs backwards.

The value of Q at Gerver's cap

theorem MovingSofa.gerver_upperBoundQ_matches (X : CapTailSpace) (hK : ↑↑↑X.cap = capOfSofa paperGerverSofa (Real.pi / 2)) (hB : ↑X.rightBody = (canonicalTailSets X.cap).1) (hD : ↑X.leftBody = (canonicalTailSets X.cap).2) : rightAngleAreaFunctional ↑X.cap = upperBoundQ X

The variation of 𝒬 at Gerver's cap is nonpositive

At the Gerver base triple the tail geometry identifies the two tail endpoints with the two cap corners, so upperBoundQ_variation presents the derivative as qVariationIntegral. Two of its four integration windows are larger than the two active tail windows, and the excess is null: on (φᴿ, π/2 - θ) one and the same contact point supports the right tail at both endpoint normals, and likewise for the left tail on (π/2 + θ, π/2 + φᴸ), so oppositeSurfaceData_angleImage_Ioo_eq_zero_of_mem_exposedEdge applies.

The variation integral is therefore the sum of the eight phase contributions (qVariationIntegral_eq_phaseSum), and each of them is nonpositive (gerverPhaseContribution_nonpos) because the tail support sums are exactly 1 on the two active windows while the competitor's are at most 1.

theorem MovingSofa.gerver_upperBoundQ_variation (X Y : CapTailSpace) (hK : ↑↑↑X.cap = capOfSofa paperGerverSofa (Real.pi / 2)) (hB : ↑X.rightBody = (canonicalTailSets X.cap).1) (hD : ↑X.leftBody = (canonicalTailSets X.cap).2) : convexDirectionalDerivative capTailCombination upperBoundQ X Y ≤ 0

Moving sofa: related mathematical developments

• Bounds.Upper.Properties.

Bounds / Upper / Properties

theorem MovingSofa.upperBoundQ_quadratic_concave : IsQuadraticFunctional capTailCombination upperBoundQ ∧ IsConvexFunctional capTailCombination upperBoundQ true

theorem MovingSofa.areaFunctional_le_upperBoundQ (X : CapTailSpace) (hB : ↑X.rightBody = (canonicalTailSets X.cap).1) (hD : ↑X.leftBody = (canonicalTailSets X.cap).2) : rightAngleAreaFunctional ↑X.cap ≤ upperBoundQ X

theorem MovingSofa.gerver_upperBoundQ_maximum : ∃ (X : CapTailSpace), ↑↑↑X.cap = capOfSofa paperGerverSofa (Real.pi / 2) ∧ ↑X.rightBody = (canonicalTailSets X.cap).1 ∧ ↑X.leftBody = (canonicalTailSets X.cap).2 ∧ ∀ (Y : CapTailSpace), upperBoundQ Y ≤ upperBoundQ X

Moving sofa: related mathematical developments

• Sofa.Balanced.
• Sofa.BalancedConsumed.

Sofa / Balanced

def MovingSofa.IsBalancedMaximumSofa (s : Set Point) (ω : ℝ) : Prop

A monotonized standard-position sofa whose associated cap is a balanced maximum cap.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.exists_balancedMaximumSofa (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) : ∃ (K : CapSpace ω), IsBalancedMaximumCap K ∧ IsBalancedMaximumSofa (↑↑K \ capNiche K) ω ∧ ∀ (s : Set Point), HasRotationAngle s ω → ClassicalResults.area s ≤ ClassicalResults.area (↑↑K \ capNiche K)

Sofa / Balanced Consumed

theorem MovingSofa.balancedMaximumCap_consumed {ω : ℝ} (K : CapSpace ω) (hω : Real.arccos (5 / 11) ≤ ω) (hω' : ω < Real.pi / 2) (hBalanced : IsBalancedMaximumCap K) (hArea : 11 / 5 ≤ capAreaFunctional K) : ∃ t ∈ Set.Ioo 0 ω, {0, (stripParallelogram ω).2.2 - tangentVector 0, (stripParallelogram ω).2.2 - normalVector ↑ω} ⊆ (rotatingHallwayParts ↑↑K ↑t).innerQuadrant

Moving sofa: related mathematical developments

• Motion.RotationAngle.

Motion / Rotation Angle

theorem MovingSofa.balancedMaximumSofa_rightAngle (s : Set Point) (ω : ℝ) (hs : IsBalancedMaximumSofa s ω) (hω : ω ∈ Set.Icc (Real.arccos (5 / 11)) (Real.pi / 2)) (hArea : 11 / 5 ≤ ClassicalResults.area s) : ∃ (α : Real.Angle), HasRotationAngle (rotationMap α '' s) (Real.pi / 2)

theorem MovingSofa.movingSofa_rotationAngle_bound (s : Set Point) (hs : IsPaperMovingSofa s) (hArea : 11 / 5 ≤ ClassicalResults.area s) : ∃ ω ∈ Set.Icc (Real.arccos (5 / 11)) (Real.pi / 2), HasRotationAngle s ω

Moving sofa: related mathematical developments

• Sofa.BalancedRightAngle.

Sofa / Balanced Right Angle

theorem MovingSofa.exists_dominating_balancedRightAngleSofa (s : Set Point) (hs : IsPaperMovingSofa s) (harea : 11 / 5 ≤ ClassicalResults.area s) : ∃ (s' : Set Point), IsBalancedMaximumSofa s' (Real.pi / 2) ∧ ClassicalResults.area s ≤ ClassicalResults.area s'

Moving sofa: related mathematical developments

• Sofa.Maximum.

Gerver's sofa attains the maximum moving-sofa area

The paper's main theorem: Gerver's paper-frame set paperGerverSofa is a moving sofa, and every moving sofa has area at most its area.

The proof splits on the certified lower bound 11 / 5. A sofa below that bound is dominated outright. A sofa at or above it is dominated by a balanced maximum sofa of angle π / 2, whose cap lies in the special domain and extends to a triple in the cap-tail space; the area functional is then bounded by Q, which is maximized by Gerver's triple and matches the area functional there.

theorem MovingSofa.paperGerverSofa_maximum : IsPaperMovingSofa paperGerverSofa ∧ ∀ (s : Set Point), IsPaperMovingSofa s → ClassicalResults.area s ≤ ClassicalResults.area paperGerverSofa

Moving sofa: related mathematical developments

• Motion.CanonicalUpperBound.

The paper's upper bound transported to the canonical target

The paper's main theorem bounds the real area of every moving sofa in the paper normalization by the area of the paper Gerver sofa. The canonical and paper Gerver sets coincide, every admissible set is a paper moving sofa, and admissible sets are compact, so the comparison of real areas is a comparison of Lebesgue measures.

theorem MovingSofa.areaUpperBound : AreaUpperBound

Every admissible set has Lebesgue measure at most that of Gerver's sofa.

The moving sofa problem: proofs

The imported development proves uniqueness of Gerver's defining parameters in MovingSofa.GerversSofa.ABφθSpec.existsUnique and admissibility of the resulting shape in MovingSofa.isMovingSofa_gerversSofa. The main theorem combines this admissibility result with the proved area upper bound MovingSofa.areaUpperBound.

theorem MovingSofa.sofaConstant_eq_volume_gerversSofa : sofaConstant = MeasureTheory.volume gerversSofa

Gerver's sofa attains the sofa constant (Baek, arXiv:2411.19826).