Moving sofa: related mathematical developments

• Area.Applications.Development001.
• Area.Applications.Development002.
• Area.Applications.Development003.
• Cap.Applications.Development001.
• Gerver.Applications.Development001.
• Gerver.Applications.Development002.
• Polygon.Applications.Development001.

Moving sofa: related mathematical developments

• Area.Middle.

The middle part of the niche

capMiddle_area_lower_bound bounds the area of the part of a special cap's niche outside both distinguished tail half-planes from below by the three signed areas of the middle fan: the two wedge triangles and the inner-corner arc.

The geometry is that of the paper's proof. Writing φ for the right distinguished angle, l = π/2 - φ for the left one and k = tan φ, the two distinguished tail support lines are X = w - k y and X = z + k y, where w and z are the horizontal coordinates of the two fan points W and Z; the inner corner runs from the first line to the second through the open cone between them, with strictly decreasing horizontal coordinate. Adding a base line y = -h strictly below the arc turns the arc together with the two side segments into a strictly monotone three-piece roof over that base line, and the region under the roof exceeds the base trapezoid by the asserted three signed areas. Every point of the open region above the trapezoid lies in the niche, because the roof point vertically above it exhibits a time whose open inward quadrant contains it.

noncomputable def MovingSofa.upperBoundMiddle (K : SpecialCapSpace) : ℝ

The middle area bound obtained from cap area, endpoint segments and the corner-path integral.

Equations

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

Arithmetic of a side segment of the middle cone

The two side segments of the four-piece loop run along the two tail support lines, so their displacements (Δ₀, Δ₁) satisfy Δ₀ cos = Δ₁ sin for the relevant frame angle. The two lemmas below are the resulting sign computations for a point δ below such a segment.

The cone between the two distinguished tail support lines

The niche contains the open region above the base trapezoid

The lower estimate

theorem MovingSofa.capMiddle_area_lower_bound (K : SpecialCapSpace) : segmentArea (distinguishedCapSides ↑K).1.fanPoint (distinguishedCapSides ↑K).1.corner + curveAreaFunctional (capMiddleBV K) + segmentArea (distinguishedCapSides ↑K).2.corner (distinguishedCapSides ↑K).2.fanPoint ≤ ClassicalResults.area ((capNiche ↑K \ (distinguishedCapSides ↑K).1.upperHalfPlane) \ (distinguishedCapSides ↑K).2.upperHalfPlane)

Moving sofa: related mathematical developments

• Area.Mamikon.Properties.

Area / Mamikon / Properties

noncomputable def MovingSofa.mamikonOffset (K : ConvexBody Point) {a b : ℝ} (z : ContinuousBVPaths a b) (t : ℝ) : ℝ

The tangential displacement from an exposed-edge endpoint to the path, extended by zero.

Equations

• MovingSofa.mamikonOffset K z t = if ht : t ∈ Set.Icc a b then inner ℝ (↑z ⟨t, ht⟩ - (MovingSofa.edgeVertices K ↑t).1) (MovingSofa.tangentVector ↑t) else 0

theorem MovingSofa.sqIntegral_quadratic_convex {α : Type u_1} {Ω : Type u_2} [MeasurableSpace Ω] (c : ↑unitInterval → α → α → α) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (g : α → Ω → ℝ) (hmeas : ∀ (x : α), Measurable (g x)) (hbdd : ∀ (x : α), ∃ (C : ℝ), ∀ (ω : Ω), |g x ω| ≤ C) (hlin : ∀ (s : ↑unitInterval) (x y : α) (ω : Ω), g (c s x y) ω = (1 - ↑s) * g x ω + ↑s * g y ω) (f : α → ℝ) (hf : ∀ (x : α), f x = (∫ (ω : Ω), g x ω ^ 2 ∂μ) / 2) : IsQuadraticFunctional c f ∧ IsConvexFunctional c f false

Half the square integral of a bounded measurable family of integrands that is pointwise convex-linear in its parameter is a quadratic and convex functional of that parameter.

theorem MovingSofa.mamikonOffset_convexBodyCombination (s : ↑unitInterval) (K L : ConvexBody Point) {a b : ℝ} (zK zL : ContinuousBVPaths a b) (t : ℝ) : mamikonOffset (convexBodyCombination s K L) (bvPathCombination s zK zL) t = (1 - ↑s) * mamikonOffset K zK t + ↑s * mamikonOffset L zL t

The Mamikon offset is convex-linear in the body along a convex-linear family of paths.

theorem MovingSofa.mamikon_integral (K : ConvexBody Point) (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) (z : ContinuousBVPaths a b) (hz : ∀ (t : ↑(Set.Icc a b)), ↑z t ∈ (supportingLineHalfPlane ↑K ↑↑t).1) : Measurable (mamikonOffset K z) ∧ (∃ (C : ℝ), ∀ (t : ℝ), |mamikonOffset K z t| ≤ C) ∧ (∀ (t : ↑(Set.Icc a b)), ↑z t = (edgeVertices K ↑↑t).1 + mamikonOffset K z ↑t • tangentVector ↑↑t) ∧ mamikonFunctional K a b hab hba z hz = (∫ (t : ℝ) in Set.Icc a b, mamikonOffset K z t ^ 2) / 2

theorem MovingSofa.mamikon_quadratic_convex (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) (F : ConvexBody Point → ContinuousBVPaths a b) (hF : ∀ (K : ConvexBody Point) (t : ↑(Set.Icc a b)), ↑(F K) t ∈ (supportingLineHalfPlane ↑K ↑↑t).1) (hlinear : IsConvexLinear convexBodyCombination bvPathCombination F) : (IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => mamikonFunctional K a b hab hba (F K) ⋯) ∧ IsConvexFunctional convexBodyCombination (fun (K : ConvexBody Point) => mamikonFunctional K a b hab hba (F K) ⋯) false

Moving sofa: related mathematical developments

• Area.Mamikon.Tails.

Area / Mamikon / Tails

noncomputable def MovingSofa.tangentMamikonValue (K : ConvexBody Point) (a b : ℝ) : ℝ

The signed area between a convex boundary arc and its endpoint tangent segments.

Equations

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

noncomputable def MovingSofa.rightTailMamikon (B : ConvexBody Point) : ℝ

The Mamikon value of the right tail on its Gerver angle interval.

Equations

• MovingSofa.rightTailMamikon B = MovingSofa.tangentMamikonValue B (Real.pi + MovingSofa.paperGerverConstants.2.1) (3 * Real.pi / 2)

noncomputable def MovingSofa.leftTailMamikon (D : ConvexBody Point) : ℝ

The Mamikon value of the left tail on its Gerver angle interval.

Equations

• MovingSofa.leftTailMamikon D = MovingSofa.tangentMamikonValue D (3 * Real.pi / 2) (3 * Real.pi / 2 + MovingSofa.paperGerverConstants.2.2)

noncomputable def MovingSofa.tailMamikonFunctionals : (ConvexBody Point → ℝ) × (ConvexBody Point → ℝ)

Bundle the right and left tail Mamikon functionals.

Equations

• MovingSofa.tailMamikonFunctionals = (MovingSofa.rightTailMamikon, MovingSofa.leftTailMamikon)

theorem MovingSofa.tailFanPoint_identities (K : RightAngleCapSpace) (B D : ConvexBody Point) {r l : ℝ} (hr : r ∈ Set.Ioo 0 (Real.pi / 2)) (hl : l ∈ Set.Ioo 0 (Real.pi / 2)) (hB1 : supportValue ↑B ↑(Real.pi + r) = 1 - supportValue ↑↑K ↑r) (hB2 : supportValue ↑B ↑(3 * Real.pi / 2) = 0) (hD1 : supportValue ↑D ↑(3 * Real.pi / 2) = 0) (hD2 : supportValue ↑D ↑(3 * Real.pi / 2 + l) = 1 - supportValue ↑↑K ↑(Real.pi / 2 + l)) : supportingIntersection B ↑(Real.pi + r) ↑(3 * Real.pi / 2) = (wedgeEndpoints K r).1 ∧ supportingIntersection D ↑(3 * Real.pi / 2) ↑(3 * Real.pi / 2 + l) = (wedgeEndpoints K l).2 ∧ segmentArea (wedgeEndpoints K r).1 (edgeVertices B ↑(3 * Real.pi / 2)).2 = 0 ∧ segmentArea (edgeVertices D ↑(3 * Real.pi / 2)).1 (wedgeEndpoints K l).2 = 0 ∧ segmentArea (capInnerCorner K r) (wedgeEndpoints K r).1 - segmentArea (edgeVertices B ↑(Real.pi + r)).1 (wedgeEndpoints K r).1 = segmentArea (capInnerCorner K r) (edgeVertices B ↑(Real.pi + r)).1 ∧ segmentArea (wedgeEndpoints K l).2 (capInnerCorner K l) - segmentArea (wedgeEndpoints K l).2 (edgeVertices D ↑(3 * Real.pi / 2 + l)).2 = segmentArea (edgeVertices D ↑(3 * Real.pi / 2 + l)).2 (capInnerCorner K l)

The support and endpoint identities of a cap-tail triple, in segment-area form.

theorem MovingSofa.upperBoundQ_decomposition (X : CapTailSpace) : upperBoundQ X = upperBoundMiddle X.cap - rightTailMamikon X.rightBody - leftTailMamikon X.leftBody

Moving sofa: related mathematical developments

• Cap.PolylineBoundary.
• Cap.PolylineDefinition.
• Cap.Polyline.
• Cap.UpperBoundary.Polygon.

Cap / Polyline Boundary

noncomputable def MovingSofa.capBAffine {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ℝ) : ℝ × ℝ

The slope and intercept of the inner B-wall line at angle t.

Equations

• MovingSofa.capBAffine K t = (-Real.cos t / Real.sin t, (MovingSofa.supportValue ↑↑↑K ↑t - 1) / Real.sin t)

noncomputable def MovingSofa.capDAffine {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ℝ) : ℝ × ℝ

The slope and intercept of the inner D-wall line at angle t.

Equations

• MovingSofa.capDAffine K t = (Real.sin t / Real.cos t, (MovingSofa.supportValue ↑↑↑K ↑(t + Real.pi / 2) - 1) / Real.cos t)

noncomputable def MovingSofa.fanAffine (ω : ℝ) : ℝ × ℝ

The slope and zero intercept of the slanted fan boundary.

Equations

• MovingSofa.fanAffine ω = (-Real.cos ω / Real.sin ω, 0)

noncomputable def MovingSofa.capBoundaryHeight {Θ : AngleSet} (K : PolygonCapSpace Θ) (x : ℝ) : ℝ

The lower boundary height of a polygon cap after removing its niche.

Equations

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

theorem MovingSofa.capFan_sdiff_polygonNiche_eq_epigraph {Θ : AngleSet} (K : PolygonCapSpace Θ) : capFan Θ.angle \ polygonNiche Θ ↑K = {p : Point | capBoundaryHeight K (p.ofLp 0) ≤ p.ofLp 1}

The fan outside the polygon niche is the epigraph of its boundary height.

theorem MovingSofa.capFan_sdiff_polygonNiche_closed_frontier {Θ : AngleSet} (K : PolygonCapSpace Θ) : IsClosed (capFan Θ.angle \ polygonNiche Θ ↑K) ∧ frontier (capFan Θ.angle \ polygonNiche Θ ↑K) = Set.range (pointOnGraph (capBoundaryHeight K))

The cap outside its polygon niche is closed, with frontier the boundary graph.

theorem MovingSofa.exists_capBoundary_graphPolyline {Θ : AngleSet} (K : PolygonCapSpace Θ) {a b : ℝ} (hab : a < b) : ∃ (p : XMonotonePolylineData), 0 < p.edges ∧ p.vertices 0 = pointOnGraph (capBoundaryHeight K) a ∧ p.vertices (Fin.last p.edges) = pointOnGraph (capBoundaryHeight K) b ∧ p.carrier = pointOnGraph (capBoundaryHeight K) '' Set.Icc a b ∧ ∀ (i : Fin p.edges), ∃ t ∈ angleDomain Θ, inner ℝ (p.vertices i.succ - p.vertices i.castSucc) (normalVector ↑t) = 0

Every compact interval of the polygon-cap boundary graph is a finite polyline.

theorem MovingSofa.capVertices_zero_snd_eq {Θ : AngleSet} (K : PolygonCapSpace Θ) : (capVertices (↑K) 0).1.2 = supportValue (↑↑↑K) 0 • normalVector 0

The lower endpoint of the zero-angle cap face lies on the horizontal axis.

theorem MovingSofa.capVertices_angle_fst_eq {Θ : AngleSet} (K : PolygonCapSpace Θ) : (capVertices (↑K) Θ.angle).2.1 = supportValue ↑↑↑K ↑(Θ.angle + Real.pi / 2) • tangentVector ↑Θ.angle

The terminal positive cap contact lies on the lower fan ray.

theorem MovingSofa.polygonCap_left_x_lt_right_x {Θ : AngleSet} (K : PolygonCapSpace Θ) : (capVertices (↑K) Θ.angle).2.1.ofLp 0 < (capVertices (↑K) 0).1.2.ofLp 0

The terminal cap contacts occur in strictly increasing horizontal order.

theorem MovingSofa.pointOnGraph_capBoundaryHeight_rightEndpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) : pointOnGraph (capBoundaryHeight K) ((capVertices (↑K) 0).1.2.ofLp 0) = (capVertices (↑K) 0).1.2

The right cap contact lies on the boundary graph.

theorem MovingSofa.pointOnGraph_capBoundaryHeight_leftEndpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) : pointOnGraph (capBoundaryHeight K) ((capVertices (↑K) Θ.angle).2.1.ofLp 0) = (capVertices (↑K) Θ.angle).2.1

The left cap contact lies on the boundary graph.

theorem MovingSofa.capRightOpenRay_eq_graph_image {Θ : AngleSet} (K : PolygonCapSpace Θ) : {q : Point | ∃ (s : ℝ), 0 < s ∧ q = (capVertices (↑K) 0).1.2 + s • normalVector 0} = pointOnGraph (capBoundaryHeight K) '' Set.Ioi ((capVertices (↑K) 0).1.2.ofLp 0)

The open ray to the right of a polygon-cap boundary is the right graph tail.

theorem MovingSofa.capLeftOpenRay_eq_graph_image {Θ : AngleSet} (K : PolygonCapSpace Θ) : {q : Point | ∃ (s : ℝ), 0 < s ∧ q = (capVertices (↑K) Θ.angle).2.1 + s • tangentVector ↑Θ.angle} = pointOnGraph (capBoundaryHeight K) '' Set.Iio ((capVertices (↑K) Θ.angle).2.1.ofLp 0)

The open ray to the left of a polygon-cap boundary is the left graph tail.

Cap / Polyline Definition

def MovingSofa.openRay (p v : Point) : Set Point

The open ray starting at p in direction v, excluding its initial point.

Equations

• MovingSofa.openRay p v = {q : MovingSofa.Point | ∃ (s : ℝ), 0 < s ∧ q = p + s • v}

def MovingSofa.IsCapPolyline {Θ : AngleSet} (K : PolygonCapSpace Θ) (p : XMonotonePolylineData) : Prop

The polyline and two disjoint endpoint rays describe the fan-minus-niche frontier.

Equations

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

theorem MovingSofa.polygonCap_polyline {Θ : AngleSet} (K : PolygonCapSpace Θ) : ∃ (p : XMonotonePolylineData), IsCapPolyline K p

Cap / Polyline

noncomputable def MovingSofa.polygonCapPolyline {Θ : AngleSet} (K : PolygonCapSpace Θ) : XMonotonePolylineData

A chosen monotone polyline describing the polygonal cap’s niche boundary.

Equations

• MovingSofa.polygonCapPolyline K = ⋯.choose

noncomputable def MovingSofa.polygonCapPolylineLength {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) : ℝ

Sum the lengths of polyline edges perpendicular to a prescribed wall direction.

Equations

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

def MovingSofa.IsBalancedPolygonCap {Θ : AngleSet} (K : PolygonCapSpace Θ) : Prop

The cap’s surface measure at each wall direction equals the corresponding polyline length.

Equations

• MovingSofa.IsBalancedPolygonCap K = ∀ (t : ↑(MovingSofa.angleDomain Θ)), (MovingSofa.surfaceAreaMeasure ↑↑K) {↑↑t} = ENNReal.ofReal (MovingSofa.polygonCapPolylineLength K t)

Cap / Upper Boundary / Polygon

theorem MovingSofa.PolygonCapSpace.capVertices_fst_bounds {Θ : AngleSet} (K : PolygonCapSpace Θ) {q : Point} (hq : q ∈ ↑↑↑K) : (capVertices (↑K) Θ.angle).2.1.ofLp 0 ≤ q.ofLp 0 ∧ q.ofLp 0 ≤ (capVertices (↑K) 0).1.2.ofLp 0

The terminal cap contacts bound every horizontal coordinate of a polygon cap.

theorem MovingSofa.PolygonCapSpace.sum_hausdorffMeasure_exposedEdge_mul_sin {Θ : AngleSet} (K : PolygonCapSpace Θ) (D : Finset ℝ) (hne : D.Nonempty) (hD : ↑D = angleDomain Θ) : ∑ t ∈ D, ((MeasureTheory.Measure.hausdorffMeasure 1) (exposedEdge ↑↑K ↑t)).toReal * Real.sin t = (capVertices (↑K) 0).1.2.ofLp 0 - (capVertices (↑K) Θ.angle).2.1.ofLp 0

The sine-weighted exposed-face lengths equal the horizontal separation of cap contacts.

Moving sofa: related mathematical developments

• Gerver.Area.Evaluator.
• Gerver.Area.CapFan.
• Gerver.Area.NicheCover.
• Gerver.Area.

Soundness of the contact evaluator

GerverAreaCert.evalZ s z kind evaluates one of the five phase formulas of Gerver's sofa, and one of its four contact curves, on an interval of rotation angles. This module proves that it encloses the analytic value: gerverBranch_eq identifies the branch that the piecewise vendor definitions GerverSofa.Romik.path and GerverSofa.PartC.alphaBetaAt select, the five per-stage lemmas verify the phase formulas and the two velocity coefficients against GerverSofa.Romik.path1 … path5 and GerverSofa.Romik.alphaBeta1 … alphaBeta5, and evalZ_sound assembles them through the coordinate dictionary fromPlane_paperGerverContacts. contactZ_sound and evalZ_interval_sound specialise this to a grid angle and to a whole grid subinterval.

The contact evaluator

noncomputable def MovingSofa.gerverBranchPath : ℕ → ℝ → GerverSofa.Point

The five certified phase maps, selected by stage index.

Equations

• MovingSofa.gerverBranchPath 1 = GerverSofa.Romik.path1 GerverSofa.PartB.params
• MovingSofa.gerverBranchPath 2 = GerverSofa.Romik.path2 GerverSofa.PartB.params
• MovingSofa.gerverBranchPath 3 = GerverSofa.Romik.path3 GerverSofa.PartB.params
• MovingSofa.gerverBranchPath 4 = GerverSofa.Romik.path4 GerverSofa.PartB.params
• MovingSofa.gerverBranchPath x✝ = GerverSofa.Romik.path5 GerverSofa.PartB.params

noncomputable def MovingSofa.gerverBranchAlphaBeta : ℕ → ℝ → GerverSofa.Point

The five certified velocity-coefficient pairs, selected by stage index.

Equations

• MovingSofa.gerverBranchAlphaBeta 1 = GerverSofa.Romik.alphaBeta1 GerverSofa.PartB.params
• MovingSofa.gerverBranchAlphaBeta 2 = GerverSofa.Romik.alphaBeta2 GerverSofa.PartB.params
• MovingSofa.gerverBranchAlphaBeta 3 = GerverSofa.Romik.alphaBeta3 GerverSofa.PartB.params
• MovingSofa.gerverBranchAlphaBeta 4 = GerverSofa.Romik.alphaBeta4 GerverSofa.PartB.params
• MovingSofa.gerverBranchAlphaBeta x✝ = GerverSofa.Romik.alphaBeta5 GerverSofa.PartB.params

theorem MovingSofa.gerverBranch_eq (s : ℕ) (hs1 : 1 ≤ s) (hs5 : s ≤ 5) {x : ℝ} (hxhi : x ≤ gerverStageTime s) (hxlo : 2 ≤ s → gerverStageTime (s - 1) < x) : GerverSofa.Romik.path GerverSofa.PartB.params x = gerverBranchPath s x ∧ GerverSofa.PartC.alphaBetaAt x = gerverBranchAlphaBeta s x

On a grid angle of stage s both piecewise definitions select branch s.

theorem MovingSofa.evalZ_zero_sound (s : ℕ) (hs1 : 1 ≤ s) (hs5 : s ≤ 5) {z : GerverAreaCert.SI} {x : ℝ} (hz : z.Contains x) (hsin : (GerverAreaCert.trigZ z).1.Contains (Real.sin x)) (hcos : (GerverAreaCert.trigZ z).2.Contains (Real.cos x)) : (GerverAreaCert.evalZ s z 0).1.Contains (gerverBranchPath s x).1 ∧ (GerverAreaCert.evalZ s z 0).2.Contains (gerverBranchPath s x).2

Per-stage soundness of the phase-map evaluation, i.e. of the kind = 0 output. Pure interval arithmetic against GerverSofa.Romik.path1 … path5: five cases, each a chain of SI.contains_* applications on top of contains_params, hsin and hcos.

theorem MovingSofa.evalZ_offset_sound (s : ℕ) (hs1 : 1 ≤ s) (hs5 : s ≤ 5) {z : GerverAreaCert.SI} {x : ℝ} (hz : z.Contains x) (hsin : (GerverAreaCert.trigZ z).1.Contains (Real.sin x)) (hcos : (GerverAreaCert.trigZ z).2.Contains (Real.cos x)) : (GerverAreaCert.evalZ s z 2).1.Contains ((gerverBranchPath s x).1 - (gerverBranchAlphaBeta s x).1 * Real.sin x) ∧ (GerverAreaCert.evalZ s z 2).2.Contains ((gerverBranchPath s x).2 + (gerverBranchAlphaBeta s x).1 * Real.cos x) ∧ (GerverAreaCert.evalZ s z 4).1.Contains ((gerverBranchPath s x).1 - (gerverBranchAlphaBeta s x).2 * Real.cos x) ∧ (GerverAreaCert.evalZ s z 4).2.Contains ((gerverBranchPath s x).2 - (gerverBranchAlphaBeta s x).2 * Real.sin x)

Per-stage soundness of the B and D offsets, i.e. of the two velocity coefficients α and β against GerverSofa.Romik.alphaBeta1 … alphaBeta5. Note evalZ s z 1 = evalZ s z 2 shifted by (cos x, sin x) and evalZ s z 3 = evalZ s z 4 shifted by (-sin x, cos x), so the remaining two kinds need no separate stage analysis.

theorem MovingSofa.evalZ_sound (s : ℕ) (hs1 : 1 ≤ s) (hs5 : s ≤ 5) {z : GerverAreaCert.SI} {x : ℝ} (hz : z.Contains x) (hx0 : 0 ≤ x) (hxT : x ≤ Real.pi / 2) (hxhi : x ≤ gerverStageTime s) (hxlo : 2 ≤ s → gerverStageTime (s - 1) < x) (kind : ℕ) (hk : kind ≤ 4) : (GerverAreaCert.evalZ s z kind).1.Contains ((gerverContactPoint kind x).ofLp 0) ∧ (GerverAreaCert.evalZ s z kind).2.Contains ((gerverContactPoint kind x).ofLp 1)

Soundness of the executable phase/contact evaluator: on the branch that the piecewise definitions select, the interval evaluation encloses both coordinates of the selected curve. Reduces to gerverBranch_eq, evalZ_zero_sound, evalZ_offset_sound, trigZ_sound and the coordinate dictionary fromPlane_paperGerverContacts (GerverSofa.u t = (cos t, sin t), GerverSofa.v t = (-sin t, cos t)).

theorem MovingSofa.stageTime_pred_le_gerverGridTime (m : ℕ) (hm : m + 1 ≤ 5 * GerverAreaCert.NN) (h2 : 2 ≤ GerverAreaCert.stageOf (m + 1)) : gerverStageTime (GerverAreaCert.stageOf (m + 1) - 1) ≤ gerverGridTime m

The left endpoint of the branch selected at the right end of a grid subinterval does not exceed the left end of that subinterval.

theorem MovingSofa.contactZ_sound (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) (kind : ℕ) (hk : kind ≤ 4) : (GerverAreaCert.contactZ m kind).1.Contains ((gerverContactPoint kind (gerverGridTime m)).ofLp 0) ∧ (GerverAreaCert.contactZ m kind).2.Contains ((gerverContactPoint kind (gerverGridTime m)).ofLp 1)

The evaluator at a grid angle.

theorem MovingSofa.evalZ_interval_sound (m : ℕ) (hm : m + 1 ≤ 5 * GerverAreaCert.NN) (kind : ℕ) (hk : kind ≤ 4) {x : ℝ} (hx : x ∈ Set.Ioc (gerverGridTime m) (gerverGridTime (m + 1))) : (GerverAreaCert.evalZ (GerverAreaCert.stageOf (m + 1)) { lo := (GerverAreaCert.ttZ m).lo, hi := (GerverAreaCert.ttZ (m + 1)).hi } kind).1.Contains ((gerverContactPoint kind x).ofLp 0) ∧ (GerverAreaCert.evalZ (GerverAreaCert.stageOf (m + 1)) { lo := (GerverAreaCert.ttZ m).lo, hi := (GerverAreaCert.ttZ (m + 1)).hi } kind).2.Contains ((gerverContactPoint kind x).ofLp 1)

The evaluator over a whole grid subinterval, on the branch selected at its right endpoint (which is the branch of every angle in the half-open subinterval).

The support-contact fan of the Gerver outer cap

The literal Gerver outer cap is a compact convex subset of the plane lying in the closed quadrant above the fan anchor L = C (π / 2), which sits on the wall. The 640 listed contacts A (t) and C (t) at the grid angles attain the cap support at the strictly increasing normals t and t + π / 2 of [0, π), so supportContact_fan_area bounds the cap area below by half the shoelace sum of the fan over the anchor. The certificate encloses that sum (capDoubledZ_sound), and its kernel-checked numeric conclusion GerverAreaCert.capOK_true turns the enclosure into 28609 / 10000 ≤ |K₀|.

Elementary geometry of the outer cap

theorem MovingSofa.paperGerverPath_zero : paperGerverPath 0 = 0

The paper path starts at the origin.

theorem MovingSofa.gerverOuterCap_eq_iInter : gerverOuterCap = {q : Point | 0 ≤ inner ℝ q (normalVector ↑(Real.pi / 2))} ∩ ⋂ t ∈ Set.Icc 0 (Real.pi / 2), {q : Point | inner ℝ q (normalVector ↑t) ≤ inner ℝ (paperGerverPath t) (normalVector ↑t) + 1} ∩ {q : Point | inner ℝ q (tangentVector ↑t) ≤ inner ℝ (paperGerverPath t) (tangentVector ↑t) + 1}

The outer cap written as an intersection of closed half-planes.

theorem MovingSofa.isClosed_gerverOuterCap : IsClosed gerverOuterCap

The outer cap is closed, being an intersection of closed half-spaces.

theorem MovingSofa.convex_gerverOuterCap : Convex ℝ gerverOuterCap

The outer cap is convex, being an intersection of half-spaces.

theorem MovingSofa.gerverOuterCap_subset_box : gerverOuterCap ⊆ {p : Point | p.ofLp 0 ∈ Set.Icc (-(inner ℝ (paperGerverPath (Real.pi / 2)) (tangentVector ↑(Real.pi / 2)) + 1)) 1 ∧ p.ofLp 1 ∈ Set.Icc 0 1}

The outer cap is contained in an explicit coordinate rectangle.

theorem MovingSofa.isCompact_gerverOuterCap : IsCompact gerverOuterCap

The outer cap is compact: it is closed and contained in a coordinate rectangle.

theorem MovingSofa.measurableSet_gerverOuterCap : MeasurableSet gerverOuterCap

The outer cap is Borel measurable.

theorem MovingSofa.volume_gerverOuterCap_lt_top : MeasureTheory.volume gerverOuterCap < ⊤

The outer cap has finite planar volume.

The support-contact fan and the cap lower bound

noncomputable def MovingSofa.gerverFanAnchor : Point

The fan anchor L = C (π / 2).

Equations

• MovingSofa.gerverFanAnchor = MovingSofa.paperGerverContacts (Real.pi / 2) 2

noncomputable def MovingSofa.gerverFanPoint (i : ℕ) : Point

The i-th listed support contact, i < fanCount.

Equations

• MovingSofa.gerverFanPoint i = MovingSofa.gerverContactPoint (MovingSofa.GerverAreaCert.fanKind i) (MovingSofa.gerverGridTime (MovingSofa.GerverAreaCert.fanIdx i))

noncomputable def MovingSofa.gerverFanNormal (i : ℕ) : ℝ

The support normal of the i-th listed contact.

Equations

• MovingSofa.gerverFanNormal i = if i ≤ 5 * MovingSofa.GerverAreaCert.NN then MovingSofa.gerverGridTime i else MovingSofa.gerverGridTime (i - 5 * MovingSofa.GerverAreaCert.NN) + Real.pi / 2

theorem MovingSofa.gerverOuterCap_support_A (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) {q : Point} (hq : q ∈ gerverOuterCap) : inner ℝ q (normalVector ↑t) ≤ inner ℝ (paperGerverContacts t 0) (normalVector ↑t)

A t attains the cap support at normal t.

theorem MovingSofa.gerverOuterCap_support_C (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) {q : Point} (hq : q ∈ gerverOuterCap) : inner ℝ q (normalVector ↑(t + Real.pi / 2)) ≤ inner ℝ (paperGerverContacts t 2) (normalVector ↑(t + Real.pi / 2))

C t attains the cap support at normal t + π / 2.

theorem MovingSofa.gerverFanAnchor_snd : gerverFanAnchor.ofLp 1 = 0

The anchor sits on the wall.

theorem MovingSofa.gerverOuterCap_quadrant {q : Point} (hq : q ∈ gerverOuterCap) : gerverFanAnchor.ofLp 0 ≤ q.ofLp 0 ∧ 0 ≤ q.ofLp 1

The cap lies in the closed quadrant above the anchor.

theorem MovingSofa.gerverFanNormal_lt_succ (i : ℕ) (hi : i + 1 < GerverAreaCert.fanCount) : gerverFanNormal i < gerverFanNormal (i + 1)

The listed support normals are strictly increasing.

theorem MovingSofa.gerverFanNormal_mem_Ico (i : ℕ) (hi : i < GerverAreaCert.fanCount) : 0 ≤ gerverFanNormal i ∧ gerverFanNormal i < Real.pi

The listed support normals lie in [0, π).

theorem MovingSofa.gerverFanPoint_mem (i : ℕ) (hi : i < GerverAreaCert.fanCount) : gerverFanPoint i ∈ gerverOuterCap

Every listed contact lies in the cap.

theorem MovingSofa.gerverFanPoint_support (i : ℕ) (hi : i < GerverAreaCert.fanCount) {q : Point} (hq : q ∈ gerverOuterCap) : inner ℝ q (normalVector ↑(gerverFanNormal i)) ≤ inner ℝ (gerverFanPoint i) (normalVector ↑(gerverFanNormal i))

Every listed contact attains the cap support at its listed normal.

theorem MovingSofa.capDoubledZ_sound : GerverAreaCert.capDoubledZ.Contains (∑ i ∈ Finset.range (GerverAreaCert.fanCount - 1), planeCrossProduct (gerverFanPoint i - gerverFanAnchor) (gerverFanPoint (i + 1) - gerverFanAnchor))

The certificate encloses the fan shoelace sum.

theorem MovingSofa.gerverOuterCap_area_certified_lower_bound : 28609 / 10000 ≤ ClassicalResults.area gerverOuterCap

The cap area lower bound.

The rectangle cover of the literal Gerver niche

The literal niche is the union of the strict vertical fills under the three pieces of its roof (gerver_niche_vertical_fills). Each piece is traversed with monotone horizontal coordinate, so subdividing the seven monotone roof stretches at the grid angles covers the niche by 7 * NN coordinate rectangles whose widths and heights the certificate encloses (gerverNicheRect_covers). The kernel-checked numeric conclusion GerverAreaCert.nicheOK_true bounds the total rectangle area, hence |N₀| ≤ 3301 / 5000.

theorem MovingSofa.measurableSet_gerverLiteralNiche : MeasurableSet gerverLiteralNiche

The literal niche is Borel measurable: it is a closed half-plane intersected with a countable union of open sets.

The rectangle cover and the niche upper bound

def MovingSofa.gerverNicheRect (r j : ℕ) : Set Point

The covering rectangle of the j-th subinterval of roof piece r.

Equations

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

theorem MovingSofa.strictVerticalFill_Icc_union {f : ℝ → Point} {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : strictVerticalFill f (Set.Icc a c) = strictVerticalFill f (Set.Icc a b) ∪ strictVerticalFill f (Set.Icc b c)

A strict vertical fill splits along a subdivision of its parameter interval.

theorem MovingSofa.gerverNicheRow_monotone (r : ℕ) (hr : r < 7) : (GerverAreaCert.rowFwd r = true → MonotoneOn (fun (t : ℝ) => (gerverContactPoint (GerverAreaCert.rowKind r) t).ofLp 0) (Set.Icc (gerverStageTime (GerverAreaCert.rowStage r - 1)) (gerverStageTime (GerverAreaCert.rowStage r)))) ∧ (GerverAreaCert.rowFwd r = false → AntitoneOn (fun (t : ℝ) => (gerverContactPoint (GerverAreaCert.rowKind r) t).ofLp 0) (Set.Icc (gerverStageTime (GerverAreaCert.rowStage r - 1)) (gerverStageTime (GerverAreaCert.rowStage r))))

Each roof piece has monotone horizontal coordinate in the direction recorded by rowFwd.

theorem MovingSofa.gerverNicheRect_covers (r j : ℕ) (hr : r < 7) (hj : j < GerverAreaCert.NN) : strictVerticalFill (gerverContactPoint (GerverAreaCert.rowKind r)) (Set.Icc (gerverGridTime (GerverAreaCert.rowBase r j)) (gerverGridTime (GerverAreaCert.rowBase r j + 1))) ⊆ gerverNicheRect r j

Each covering rectangle contains the strict vertical fill of its subinterval.

theorem MovingSofa.gerverLiteralNiche_subset_rects : gerverLiteralNiche ⊆ ⋃ r ∈ Finset.range 7, ⋃ j ∈ Finset.range GerverAreaCert.NN, gerverNicheRect r j

The 7 * NN rectangles cover the literal niche.

theorem MovingSofa.volume_gerverNicheRect (r j : ℕ) : MeasureTheory.volume (gerverNicheRect r j) = ENNReal.ofReal (↑(GerverAreaCert.rectHiZ r j - GerverAreaCert.rectLoZ r j) / ↑GerverAreaCert.M) * ENNReal.ofReal (↑(GerverAreaCert.rectHZ r j) / ↑GerverAreaCert.M)

The planar volume of one covering rectangle.

theorem MovingSofa.gerverNicheRect_volume_sum_le : ∑ r ∈ Finset.range 7, ∑ j ∈ Finset.range GerverAreaCert.NN, MeasureTheory.volume (gerverNicheRect r j) ≤ ENNReal.ofReal (3301 / 5000)

The certificate bounds the total rectangle volume.

theorem MovingSofa.gerver_niche_volume_le : MeasureTheory.volume gerverLiteralNiche ≤ ENNReal.ofReal (3301 / 5000)

The niche volume bound.

Rational area bounds for the canonical Gerver sofa

The canonical Gerver sofa is the paper's literal set (gerver_canonical_paper_literal), the difference of the literal outer cap and the literal niche. The cap and the niche are Borel of finite area with 28609 / 10000 ≤ |K₀| and |N₀| ≤ 3301 / 5000 (gerver_geometric_area_bounds), both numeric bounds coming from the kernel-checked certificate MovingSofa.Gerver.AreaCertificate through the fan bound of MovingSofa.Gerver.Area.CapFan and the rectangle cover of MovingSofa.Gerver.Area.NicheCover. Subadditivity of area then gives 11 / 5 ≤ |G| (gerver_area_lower_bound).

theorem MovingSofa.gerver_canonical_paper_literal : gerversSofa = paperGerverSofa ∧ paperGerverSofa = gerverLiteralSofa

theorem MovingSofa.gerver_geometric_area_bounds : MeasurableSet gerverOuterCap ∧ MeasureTheory.volume gerverOuterCap < ⊤ ∧ MeasurableSet gerverLiteralNiche ∧ MeasureTheory.volume gerverLiteralNiche < ⊤ ∧ 28609 / 10000 ≤ ClassicalResults.area gerverOuterCap ∧ ClassicalResults.area gerverLiteralNiche ≤ 3301 / 5000

theorem MovingSofa.gerver_area_lower_bound : MeasureTheory.volume gerversSofa < ⊤ ∧ 11 / 5 ≤ ClassicalResults.area gerversSofa

Moving sofa: related mathematical developments

• Gerver.CapIdentification.
• Gerver.Niche.Identification.
• Gerver.SurfaceDensity.
• Gerver.VelocityAndCapArea.

Gerver / Cap Identification

theorem MovingSofa.gerver_capSupport_identification : (∀ q ∈ gerverOuterCap, ∃ p ∈ gerverLiteralSofa, p.ofLp 0 = q.ofLp 0 ∧ q.ofLp 1 ≤ p.ofLp 1) ∧ paperGerverSofa = gerverLiteralSofa ∧ IsStandardPosition gerverLiteralSofa (Real.pi / 2) ∧ (∀ s ∈ Set.Icc 0 Real.pi, supportValue gerverLiteralSofa ↑s = supportValue gerverOuterCap ↑s) ∧ capOfSofa gerverLiteralSofa (Real.pi / 2) = gerverOuterCap ∧ (∃ (K : CapSpace (Real.pi / 2)), ↑↑K = gerverOuterCap ∧ (∀ t ∈ Set.Ioo 0 (Real.pi / 2), exposedEdge ↑K ↑t = {paperGerverContacts t 0} ∧ exposedEdge ↑K ↑(t + Real.pi / 2) = {paperGerverContacts t 2}) ∧ paperGerverContacts 0 0 = (edgeVertices (↑K) 0).1 ∧ paperGerverContacts (Real.pi / 2) 0 = (edgeVertices ↑K ↑(Real.pi / 2)).2 ∧ paperGerverContacts 0 2 = (edgeVertices ↑K ↑(Real.pi / 2)).1 ∧ paperGerverContacts (Real.pi / 2) 2 = (edgeVertices ↑K ↑Real.pi).2) ∧ ∀ S ∈ {gerverOuterCap, gerverLiteralSofa}, ∀ t ∈ Set.Icc 0 (Real.pi / 2), supportValue S ↑t = inner ℝ (paperGerverPath t) (normalVector ↑t) + 1 ∧ supportValue S ↑(Real.pi / 2 + t) = inner ℝ (paperGerverPath t) (tangentVector ↑t) + 1

Gerver / Niche / Identification

theorem MovingSofa.gerver_paperNiche_identification : (∀ t ∈ Set.Icc 0 (Real.pi / 2), supportingHallway gerverOuterCap ↑t = supportingHallway paperGerverSofa ↑t ∧ supportingHallway paperGerverSofa ↑t = (fun (p : Point) => rotationMap (↑t) p + paperGerverPath t) '' hallway ∧ (rotatingHallwayParts gerverOuterCap ↑t).innerCorner = paperGerverPath t) ∧ (∃ (K : CapSpace (Real.pi / 2)), ↑↑K = gerverOuterCap ∧ capNiche K = gerverLiteralNiche) ∧ monotonization paperGerverSofa (Real.pi / 2) = paperGerverSofa ∧ IsMonotoneSofa paperGerverSofa

Surface densities of the certified Gerver cap

The certified Gerver cap carries the two envelope densities GerverSofa.PartC.Stage2.rhoA and rhoC of the vendor development: its surface-area measure is rhoA (t) dt on the angular arc [0, π/2) and rhoC (t - π/2) dt on (π/2, π].

The argument is stage by stage. On each of the five closed stages the selected (positive) vertex of the cap is a globally analytic branch of the certified phase curves, with derivative rhoA t • v t for the first contact and -rhoC t • u t for the third, so surfaceAreaMeasure_angleImage_eq_withDensity_of_hasDerivAt identifies the surface measure with the exact Lebesgue density on that stage. The stages are then glued with measure_angleImage_eq_of_union; only the last rhoA stage needs an interior exhaustion, because the positive vertex jumps at π/2.

The same stagewise phase curves describe the two inner contacts, because B = A - u and D = C - v differ from the outer contacts by a frame vector (paperGerverContacts_one_eq_sub, paperGerverContacts_three_eq_sub). Subtracting the frame vector from a phase curve therefore produces a globally differentiable branch curve for B on the last two stages and for D on the first two, with the nonnegative speeds 1 - rhoA and 1 - rhoC (exists_branch_paperGerverContacts_one, exists_branch_paperGerverContacts_three); the two speed bounds are again coarse box bounds on the certified parameters.

Coordinate transport of derivatives

The certified switching angles

The contact curves as transported certified phase curves

Contact derivatives on the open stages

theorem MovingSofa.hasDerivAt_of_eqOn_stage {G F w : ℝ → Point} {i : Fin 5} (hF : ∀ (s : ℝ), HasDerivAt F (w s) s) (hGF : ∀ t ∈ gerverStageIntervals i, G t = F t) {t : ℝ} (ht : t ∈ Set.Ioo (gerverStageTimes i.castSucc) (gerverStageTimes i.succ)) : HasDerivAt G (w t) t

A branch curve agreeing with a global curve on a closed stage computes the global derivative at every interior parameter of that stage.

Singleton faces have no surface atom

Measurability and boundedness of the two envelope densities

Elementary facts about the stage endpoints and the frame

Almost every parameter lies in an open stage

theorem MovingSofa.mem_openStage_of_mem_Ico {t : ℝ} (ht : t ∈ Set.Ico 0 (Real.pi / 2)) (hne : ∀ (k : Fin 6), t ≠ gerverStageTimes k) : ∃ (j : Fin 5), t ∈ Set.Ioo (gerverStageTimes j.castSucc) (gerverStageTimes j.succ)

A parameter of the rotation interval that is none of the six stage times lies in an open stage.

theorem MovingSofa.ae_mem_openStage (c : ℝ) {S : Set ℝ} (hS : MeasurableSet S) (hSsub : S ⊆ Set.Icc c (c + Real.pi / 2)) : ∀ᵐ (u : ℝ) ∂MeasureTheory.volume.restrict S, ∃ (j : Fin 5), u - c ∈ Set.Ioo (gerverStageTimes j.castSucc) (gerverStageTimes j.succ)

Almost every parameter of a measurable subset of the shifted rotation interval lies in a shifted open stage.

Branch curves for the two inner contacts

The second contact B = x + α v is the first contact A = x + α v + u translated by -u, and the fourth contact D = x - β u is the third contact C = x - β u + v translated by -v. So subtracting a frame vector from the transported phase curve of a stage produces a globally differentiable branch curve for B and for D, whose speed against the frame is 1 - rhoA resp. 1 - rhoC. Both are nonnegative exactly where the inner contact is a genuine contact: after the third stage time for B and before the second for D.

theorem MovingSofa.paperGerverContacts_one_eq_sub (t : ℝ) : paperGerverContacts t 1 = paperGerverContacts t 0 - normalVector ↑t

The second contact curve is the first one translated by -u_t.

theorem MovingSofa.paperGerverContacts_three_eq_sub (t : ℝ) : paperGerverContacts t 3 = paperGerverContacts t 2 - tangentVector ↑t

The fourth contact curve is the third one translated by -v_t.

theorem MovingSofa.exists_branch_paperGerverContacts_one {i : Fin 5} (hi : i = 3 ∨ i = 4) : ∃ (F : ℝ → Point) (g : ℝ → ℝ), (∀ (s : ℝ), HasDerivAt F (-g s • tangentVector ↑s) s) ∧ Continuous g ∧ (∀ t ∈ Set.Ioc (gerverStageTimes i.castSucc) (gerverStageTimes i.succ), 0 ≤ g t) ∧ ∀ t ∈ gerverStageIntervals i, paperGerverContacts t 1 = F t

On each of the last two stages the second contact curve agrees with a globally differentiable branch curve whose derivative is -(g t) • v_t for a continuous factor g that is nonnegative on the stage.

theorem MovingSofa.exists_branch_paperGerverContacts_three {i : Fin 5} (hi : i = 0 ∨ i = 1) : ∃ (F : ℝ → Point) (g : ℝ → ℝ), (∀ (s : ℝ), HasDerivAt F (g s • normalVector ↑s) s) ∧ Continuous g ∧ (∀ t ∈ Set.Ioc (gerverStageTimes i.castSucc) (gerverStageTimes i.succ), 0 ≤ g t) ∧ ∀ t ∈ gerverStageIntervals i, paperGerverContacts t 3 = F t

On each of the first two stages the fourth contact curve agrees with a globally differentiable branch curve whose derivative is g t • u_t for a continuous factor g that is nonnegative on the stage.

The certified cap witness and its positive vertex curves

The stagewise density identities

Exhausting the last stage of the first arc from inside

Gluing two adjacent arcs

The density identity on each full arc

theorem MovingSofa.gerver_surface_densities : ∃ (K : RightAngleCapSpace), ↑↑K = capOfSofa paperGerverSofa (Real.pi / 2) ∧ ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s ∧ (∃ (M : ℝ), ∀ t ∈ Set.Icc 0 (Real.pi / 2), ↑(r t) ≤ M ∧ ↑(s t) ≤ M) ∧ ∀ (i : Fin 5), ∀ t ∈ Set.Ioo (gerverStageTimes i.castSucc) (gerverStageTimes i.succ), HasDerivAt (fun (u : ℝ) => paperGerverContacts u 0) (↑(r t) • tangentVector ↑t) t ∧ HasDerivAt (fun (u : ℝ) => paperGerverContacts u 2) (-↑(s t) • normalVector ↑t) t

Gerver / Velocity And Cap Area

theorem MovingSofa.gerver_strict_velocity (t : ℝ) (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : (paperGerverVelocityComponents t).1 < 0 ∧ 0 < (paperGerverVelocityComponents t).2 ∧ inner ℝ (deriv paperGerverPath t) (normalVector ↑t) < 0 ∧ 0 < inner ℝ (deriv paperGerverPath t) (tangentVector ↑t)

theorem MovingSofa.paperGerverVelocityComponents_fst_nonpos {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : (paperGerverVelocityComponents t).1 ≤ 0

The tangential velocity component is nonpositive on the whole closed rotation interval: the strict inequality of gerver_strict_velocity holds on the open interval, and the component is continuous, so the closed condition propagates to the two endpoints.

theorem MovingSofa.paperGerverVelocityComponents_snd_nonneg {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : 0 ≤ (paperGerverVelocityComponents t).2

The normal velocity component is nonnegative on the whole closed rotation interval; see paperGerverVelocityComponents_fst_nonpos for the argument.

theorem MovingSofa.gerver_cap_area_lower_bound : 2 * GerverSofa.PartB.params.a1 ≤ ClassicalResults.area gerverOuterCap ∧ 12 / 5 ≤ 2 * GerverSofa.PartB.params.a1 ∧ 11 / 5 < 12 / 5

Moving sofa: related mathematical developments

• Polygon.BalancedContainment.
• Polygon.Polyline.Length.Basic.
• Polygon.Polyline.Length.Boundary.
• Polygon.Polyline.Length.
• Polygon.Balancing.Coefficients.
• Polygon.Balancing.Estimate.
• Polygon.Balancing.
• Polygon.EdgeNormals.

Polygon / Balanced Containment

theorem MovingSofa.polygonCapPolyline_inner_le_of_balanced {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsBalancedPolygonCap K) (D : Finset ℝ) (hD : ↑D = angleDomain Θ) (s : ℝ) {q : Point} (hq : q ∈ (polygonCapPolyline K).carrier) : inner ℝ q (normalVector ↑s) ≤ inner ℝ (capVertices (↑K) 0).1.2 (normalVector ↑s) + ∑ u ∈ D, ((surfaceAreaMeasure ↑↑K) {↑u}).toReal * max (Real.sin (s - u)) 0

Balance bounds the polyline projections by the surface-area atoms.

theorem MovingSofa.polygonCapPolyline_inner_le_support_of_balanced {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsBalancedPolygonCap K) (D : Finset ℝ) (hD : ↑D = angleDomain Θ) {s : ℝ} (hs : s ∈ Set.Ioo 0 Real.pi) {q : Point} (hq : q ∈ (polygonCapPolyline K).carrier) : inner ℝ q (normalVector ↑s) ≤ supportValue ↑↑↑K ↑s

A balanced polygon cap bounds every upper-normal projection of its polyline.

theorem MovingSofa.polygonCapPolyline_subset_of_balanced {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsBalancedPolygonCap K) : (polygonCapPolyline K).carrier ⊆ ↑↑↑K

The polyline of a balanced polygon cap lies inside the cap.

theorem MovingSofa.polygonNiche_subset_of_polyline_subset {Θ : AngleSet} (K : PolygonCapSpace Θ) (hpoly : (polygonCapPolyline K).carrier ⊆ ↑↑↑K) : polygonNiche Θ ↑K ⊆ ↑↑↑K

A polygon niche lies in its cap whenever its upper boundary polyline does.

theorem MovingSofa.polygonNiche_subset_of_balanced {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsBalancedPolygonCap K) : polygonNiche Θ ↑K ⊆ ↑↑↑K

Every balanced polygon cap contains its polygon niche.

Polygon / Polyline / Length / Basic

noncomputable def MovingSofa.polygonPolylineLengthAt {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ℝ) : ℝ

Extend the directional polyline-length function by zero outside the angle domain.

Equations

• MovingSofa.polygonPolylineLengthAt K t = if ht : t ∈ MovingSofa.angleDomain Θ then MovingSofa.polygonCapPolylineLength K ⟨t, ht⟩ else 0

noncomputable def MovingSofa.nicheBoundaryLength {Θ : AngleSet} (K : PolygonCapSpace Θ) (S : Set Point) : ℝ

The one-dimensional Hausdorff measure of the niche frontier inside a specified set.

Equations

• MovingSofa.nicheBoundaryLength K S = ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (MovingSofa.polygonNiche Θ ↑K) ∩ S)).toReal

Polygon / Polyline / Length / Boundary

theorem MovingSofa.isClosed_capFan (ω : ℝ) : IsClosed (capFan ω)

The fan clipping the niche is closed.

theorem MovingSofa.isOpen_innerQuadrant (S : Set Point) (t : ℝ) : IsOpen (innerQuadrant S t)

The inward quadrant of a supporting hallway is open.

theorem MovingSofa.polygonNiche_fanLine_lengths {Θ : AngleSet} (K : PolygonCapSpace Θ) {t : ℝ} (ht : t ∈ {Θ.angle, Real.pi / 2}) : nicheBoundaryLength K (normalLine (↑t) 0) = ((surfaceAreaMeasure ↑↑K) {↑(t + Real.pi)}).toReal - polygonPolylineLengthAt K t ∧ ((MeasureTheory.Measure.hausdorffMeasure 1) (polygonNiche Θ ↑K ∩ normalLine (↑t) 0)).toReal = ((surfaceAreaMeasure ↑↑K) {↑(t + Real.pi)}).toReal - polygonPolylineLengthAt K t

The niche trace on a fan line is the lower face length minus polyline length.

theorem MovingSofa.polygonNiche_wall_lengths {Θ : AngleSet} (K : PolygonCapSpace Θ) {t : ℝ} (ht : t ∈ Θ.directions) : nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).b = polygonPolylineLengthAt K t ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).bRay = polygonPolylineLengthAt K t ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).d = polygonPolylineLengthAt K (t + Real.pi / 2) ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).dRay = polygonPolylineLengthAt K (t + Real.pi / 2)

Inner-wall and inner-ray niche lengths agree with the corresponding polyline lengths.

Polygon / Polyline / Length

theorem MovingSofa.polygonCap_polyline_lengths {Θ : AngleSet} (K : PolygonCapSpace Θ) : (∀ t ∈ Θ.directions, nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).b = polygonPolylineLengthAt K t ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).bRay = polygonPolylineLengthAt K t ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).d = polygonPolylineLengthAt K (t + Real.pi / 2) ∧ nicheBoundaryLength K (rotatingHallwayParts ↑↑↑K ↑t).dRay = polygonPolylineLengthAt K (t + Real.pi / 2)) ∧ ∀ t ∈ {Θ.angle, Real.pi / 2}, nicheBoundaryLength K (normalLine (↑t) 0) = ((surfaceAreaMeasure ↑↑K) {↑(t + Real.pi)}).toReal - polygonPolylineLengthAt K t ∧ ((MeasureTheory.Measure.hausdorffMeasure 1) (polygonNiche Θ ↑K ∩ normalLine (↑t) 0)).toReal = ((surfaceAreaMeasure ↑↑K) {↑(t + Real.pi)}).toReal - polygonPolylineLengthAt K t

theorem MovingSofa.polygonCap_not_balanced_positive {Θ : AngleSet} (K : PolygonCapSpace Θ) (h : ¬IsBalancedPolygonCap K) : ∃ (t : ↑(angleDomain Θ)), ENNReal.ofReal (polygonCapPolylineLength K t) < (surfaceAreaMeasure ↑↑K) {↑↑t}

Polygon / Balancing / Coefficients

theorem MovingSofa.frontier_inter_supportingLine_eq_exposedEdge (K : ConvexBody Point) (t : Real.Angle) : frontier ↑K ∩ normalLine t (supportValue (↑K) t) = exposedEdge K t

A convex body's frontier on a supporting line is its exposed edge.

theorem MovingSofa.hausdorffMeasure_frontier_inter_supportingLine (K : ConvexBody Point) (t : Real.Angle) : (MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑K ∩ normalLine t (supportValue (↑K) t)) = (surfaceAreaMeasure K) {t}

The surface-area atom is the length of the frontier on its supporting line.

theorem MovingSofa.hausdorffMeasure_frontier_inter_lowerLine_of_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) {t : ℝ} (ht : t ∈ {Θ.angle, Real.pi / 2}) : (MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑↑↑K ∩ normalLine (↑t) (supportValue ↑↑↑K ↑t - 1)) = (surfaceAreaMeasure ↑↑K) {↑(t + Real.pi)}

An endpoint cap's lower wall has the surface-area atom of the opposite normal.

theorem MovingSofa.nicheBoundaryLength_lowerLine_of_not_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∉ {Θ.angle, Real.pi / 2}) : nicheBoundaryLength K (normalLine (↑↑t) (supportValue ↑↑↑K ↑↑t - 1)) = polygonCapPolylineLength K t

Away from endpoint normals, the niche boundary on the lower wall has polyline length.

theorem MovingSofa.nicheBoundaryLength_lowerLine_of_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∈ {Θ.angle, Real.pi / 2}) : nicheBoundaryLength K (normalLine (↑↑t) (supportValue ↑↑↑K ↑↑t - 1)) = ((surfaceAreaMeasure ↑↑K) {↑(↑t + Real.pi)}).toReal - polygonCapPolylineLength K t

At an endpoint normal, the lower-wall niche length is the opposite-face length minus the polyline length.

Polygon / Balancing / Estimate

theorem MovingSofa.polygonCap_balancing_estimate_of_not_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∉ {Θ.angle, Real.pi / 2}) : ∃ (C : ℝ) (eta : ℝ), 0 ≤ C ∧ 0 < eta ∧ ∀ (varepsilon : ℝ), 0 ≤ varepsilon → varepsilon ≤ eta → |polygonHeightArea (raisedPolygonSupport K t varepsilon) - polygonHeightArea (raisedPolygonSupport K t 0) - (((surfaceAreaMeasure ↑↑K) {↑↑t}).toReal - polygonCapPolylineLength K t) * varepsilon| ≤ C * varepsilon ^ 2

The balancing area estimate when the perturbed normal is not an endpoint.

theorem MovingSofa.polygonCap_balancing_estimate_of_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∈ {Θ.angle, Real.pi / 2}) : ∃ (C : ℝ) (eta : ℝ), 0 ≤ C ∧ 0 < eta ∧ ∀ (varepsilon : ℝ), 0 ≤ varepsilon → varepsilon ≤ eta → |polygonHeightArea (raisedPolygonSupport K t varepsilon) - polygonHeightArea (raisedPolygonSupport K t 0) - (((surfaceAreaMeasure ↑↑K) {↑↑t}).toReal - polygonCapPolylineLength K t) * varepsilon| ≤ C * varepsilon ^ 2

The balancing area estimate for a simultaneous endpoint-wall displacement.

Polygon / Balancing

theorem MovingSofa.polygonCap_balancing_estimate {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) : ∃ (C : ℝ) (η : ℝ), 0 ≤ C ∧ 0 < η ∧ ∀ (ε : ℝ), 0 ≤ ε → ε ≤ η → |polygonHeightArea (raisedPolygonSupport K t ε) - polygonHeightArea (raisedPolygonSupport K t 0) - (((surfaceAreaMeasure ↑↑K) {↑↑t}).toReal - polygonCapPolylineLength K t) * ε| ≤ C * ε ^ 2

A support-height increment has the balancing first-order area term.

theorem MovingSofa.maximumPolygonCap_balanced {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsMaximumPolygonCap Θ K) : IsBalancedPolygonCap K

A maximum polygon cap has balanced boundary coefficients.

Edge normals and contact vertices of a finite half-plane intersection

A convex body presented as a finite intersection of closed half-planes has only finitely many possible contact points and only finitely many possible proper edge normals. This file records both facts in the form used by the discrete estimates on polygon caps:

• exists_active_constraint_of_mem_notMem_interior: a boundary point activates a constraint;
• exists_active_constraint_of_forall_notMem_add_smul: a direction that immediately leaves the body activates a constraint increasing along it;
• properEdgeNormal_eq_constraint_or_add_pi: a nondegenerate exposed edge has a constraint normal, up to half a turn;
• properEdgeNormal_eq_constraint: the same, without the antipodal alternative;
• PolygonCapSpace.properEdgeNormal_mem_allowed_or_antipodal and PolygonCapSpace.properEdgeNormal_mem_allowed: the polygon-cap versions;
• finiteConstraintVertices: the finite set of transversal constraint-line intersections, which contains every singleton exposed edge;
• PolygonCapSpace.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero: the surface measure of a polygon cap is carried by its proper edge normals.

theorem MovingSofa.exists_active_constraint_of_mem_notMem_interior (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (S : Set Point) (hS : S = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) {x : Point} (hxS : x ∈ S) (hxint : x ∉ interior S) : ∃ c ∈ C, inner ℝ x (normalVector c.1) = c.2

A point of a finite half-plane intersection off its interior lies on an active constraint.

theorem MovingSofa.properEdgeNormal_eq_constraint_or_add_pi (K : ConvexBody Point) (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (hK : ↑K = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) (t : Real.Angle) (ht : (edgeVertices K t).1 ≠ (edgeVertices K t).2) : ∃ c ∈ C, t = c.1 ∨ t = c.1 + ↑Real.pi

A nondegenerate exposed edge has the normal angle of one of the constraints, up to half a turn.

theorem MovingSofa.exists_active_constraint_of_forall_notMem_add_smul (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (S : Set Point) (hS : S = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) {x w : Point} (hxS : x ∈ S) (hw : ∀ (r : ℝ), 0 < r → x + r • w ∉ S) : ∃ c ∈ C, inner ℝ x (normalVector c.1) = c.2 ∧ 0 < inner ℝ w (normalVector c.1)

If a direction immediately leaves a finite intersection of closed half-planes at a point of it, some constraint is active there and increases along that direction.

theorem MovingSofa.properEdgeNormal_eq_constraint (K : ConvexBody Point) (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (hK : ↑K = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) (t : Real.Angle) (ht : (edgeVertices K t).1 ≠ (edgeVertices K t).2) : ∃ c ∈ C, t = c.1

The normal of a nondegenerate exposed edge of a finite intersection of closed half-planes is itself a constraint normal.

theorem MovingSofa.finite_polygonCapNormals (Θ : AngleSet) : ((fun (r : ℝ) => ↑r) '' angleDomain Θ ∪ capLowerNormals Θ.angle).Finite

The allowed normal set of a polygon cap is finite.

theorem MovingSofa.PolygonCapSpace.properEdgeNormal_mem_allowed_or_antipodal {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : Real.Angle) (ht : (edgeVertices (↑↑K) t).1 ≠ (edgeVertices (↑↑K) t).2) : t ∈ (fun (r : ℝ) => ↑r) '' angleDomain Θ ∪ capLowerNormals Θ.angle ∪ (fun (u : Real.Angle) => u + ↑Real.pi) '' ((fun (r : ℝ) => ↑r) '' angleDomain Θ ∪ capLowerNormals Θ.angle)

Every nondegenerate exposed edge of a polygon cap has an allowed or antipodal normal.

theorem MovingSofa.PolygonCapSpace.properEdgeNormal_mem_allowed {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : Real.Angle) (ht : (edgeVertices (↑↑K) t).1 ≠ (edgeVertices (↑↑K) t).2) : t ∈ (fun (r : ℝ) => ↑r) '' angleDomain Θ ∪ capLowerNormals Θ.angle

Every proper edge normal of a polygon cap is an allowed normal.

def MovingSofa.finiteConstraintVertices (C : Set (Real.Angle × ℝ)) : Set Point

The finitely many transversal intersection points of a finite constraint family.

Equations

• MovingSofa.finiteConstraintVertices C = ⋃ c ∈ C, ⋃ d ∈ C, if c.1 = d.1 ∨ c.1 = d.1 + ↑Real.pi then ∅ else MovingSofa.normalLine c.1 c.2 ∩ MovingSofa.normalLine d.1 d.2

theorem MovingSofa.finite_finiteConstraintVertices (C : Set (Real.Angle × ℝ)) (hC : C.Finite) : (finiteConstraintVertices C).Finite

A finite constraint family has finitely many transversal intersection points.

theorem MovingSofa.singleton_exposedEdge_mem_finiteConstraintVertices (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (K : ConvexBody Point) (hK : ↑K = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) {t : Real.Angle} {p : Point} (hp : exposedEdge K t = {p}) : p ∈ finiteConstraintVertices C

A singleton exposed edge of a finite half-plane intersection is a constraint vertex.

theorem MovingSofa.finiteConstraintVertices_measure_zero (C : Set (Real.Angle × ℝ)) (hC : C.Finite) : (MeasureTheory.Measure.hausdorffMeasure 1) (finiteConstraintVertices C) = 0

The transversal constraint vertices form a one-dimensional null set.

theorem MovingSofa.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero_of_finite_constraints (C : Set (Real.Angle × ℝ)) (hC : C.Finite) (K : ConvexBody Point) (hK : ↑K = ⋂ c ∈ C, normalHalfPlane c.1 c.2 false false) : (surfaceAreaMeasure K) {t : Real.Angle | (edgeVertices K t).1 = (edgeVertices K t).2} = 0

Surface measure of a finite intersection of closed half-planes is carried by its proper edge normals.

theorem MovingSofa.PolygonCapSpace.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero {Θ : AngleSet} (K : PolygonCapSpace Θ) : (surfaceAreaMeasure ↑↑K) {t : Real.Angle | (edgeVertices (↑↑K) t).1 = (edgeVertices (↑↑K) t).2} = 0

Surface measure of a polygon cap is carried by its proper edge normals.