Source-linked AI summary
Certified Geometry and Admissible Motion of Gerver's Sofa
Dawid Trela
TL;DR
The moving sofa problem asks which planar sets can pass through a unit-width right-angled hallway, but certifying Gerver’s construction requires exact parameters and global geometric constraints. The paper gives an exact-rational certification and explicit admissible motion, and establishes properties of the certified cap and fixed set while limiting its uniqueness claim to a specified box.
Problem
Numerical root-finder output and plots do not prove the exact parameter vector or certify continuum hallway constraints, niche topology, and moving-sofa conditions.
Source: §1 · pp. 1–2Method
The paper combines exact-rational Krawczyk certificates with interval-based geometric verification and derives admissible motion by an inverse rigid transformation.
Source: §1 · p. 2Results
The certified set is a compact cap with the stated support normalization, and its fixed set is nonempty.
Source: §4.1 · p. 9, §5.2 · p. 14Takeaways & Limitations
The paper supplies an explicit admissible rigid motion for Gerver’s construction using a set-theoretic argument from the cap and niche definitions.
Source: §1 · p. 2Uniqueness is proved only for the full system’s zero in the explicit rational box, not globally for all real zeros of Romik’s system.
Source: §6 · p. 17
Abstract
from arXiv · showhide
The moving sofa problem asks for the largest planar set that can pass through a unit-width right-angled hallway. Gerver's 1992 construction remains the largest explicit example, but its defining switching parameters, continuum of supporting hallways, and contact topology involve transcendental equations and global inequalities. We give a reproducible exact-rational certification of the construction. A strict four-dimensional Krawczyk inclusion encloses the reduced switching system, while an independent twenty-two-dimensional Krawczyk calculation verifies Romik's full matching and contact equations in an explicit rational box. Exact interval propagation through the five analytic phases proves the support identities, global half-plane constraints, inner-wall separation, niche topology, oriented contacts, injectivity, and area bounds. From the certified support functions we identify every supporting hallway as L_t=x(t)+R_tL. For G=K_0\setminus\mathcal N(K_0) we prove directly that G is nonempty, closed, and connected and that \Phi_t(q)=R_{-t}(q-x(t)) is a continuous path in SE(2) carrying G through the hallway, with the correct initial and final arms. We further identify G with Romik's reconstruction of Gerver's classical eighteen-piece sofa. The deterministic companion verifier uses only Python's standard library and exact rational arithmetic. As a consequence, the Gerver-specific geometric hypotheses in Baek's recent variational framework are rigorously certified; we also clarify the one-sided tangent-speed convention at two contact-curve junctions.
1 Introduction
The introduction frames Gerver’s sofa as a certification problem involving exact parameters, continuum hallway constraints, and topology. It previews an exact-rational proof of the construction and an explicit admissible motion.
1 Introduction
- Numerical roots and plots alone do not establish the exact parameter vector, continuum hallway constraints, niche topology, or moving-sofa conditions.The smallest visible geometric margin is only of order 10^-3.Source: §1 · p. 2
- A strict four-dimensional Krawczyk enclosure and an independent twenty-two-dimensional certificate verify the reduced switching system and Romik’s full matching and contact system.The certification uses an explicit rational box for the full system.Source: §1 · p. 2
- Exact-rational certification establishes global support inequalities, critical inner-wall separation, niche topology, contacts, injectivity, and an area threshold.The supporting hallway is identified as L_t = x(t) + R_tL for every angle.Source: §1 · p. 2
- The fixed set G = K0 \ N(K0) is nonempty, closed, and connected, and is contained in every supporting hallway; the cited material also gives a continuous rigid-motion path.The path is Φt(q) = R−t(q − x(t)).Source: §1 · p. 2
- The fixed set is identified with Romik’s reconstruction of Gerver’s classical eighteen-piece sofa [6].Source: §1 · p. 2
- The work provides a deterministic standard-library verifier and certifies Gerver-specific geometric input to Baek’s variational framework, including a one-sided tangent-speed convention at two junctions.Source: §1 · p. 2
2 The hallway, moving sofas, and Gerver’s construction
The section defines the unit-width L-shaped hallway and the conditions for a set to move through it. It then specifies Gerver’s motion as a five-phase rotation path whose constants satisfy matching and contact conditions.
2.1 The standard hallway and rigid motions
- The standard unit-width hallway has horizontal and vertical arms, and the cap fan for a quarter-turn is the upper half-plane.Source: §2.1 · p. 3
- A moving sofa is a nonempty, closed, connected set carried by a continuous path of orientation-preserving rigid motions from the horizontal arm, through the hallway, to the vertical arm.The inner quadrant is open, so contact with either inner wall is allowed.Source: §2.1 · p. 3
- A linear reparametrization allows the motion to use any compact time interval instead of [0, 1].Source: §2.1 · p. 3
2.2 Gerverś five-phase rotation path
- Gerver’s path is represented as five analytic phases over successive angle intervals, following Romik.The phase constants are fixed by symmetry, normalization, C1 matching, and two contact conditions.Source: §2.2 · p. 4
3 Exact certification of the Gerver parameters
The paper certifies the switching parameters first in a reduced four-dimensional system, then independently verifies Romik’s full matching and contact system in a rational box. Together, the certificates establish a unique solution and support the five-phase path’s matching and symmetry properties.
3.1 The reduced four-dimensional system
- The reduced system (6)–(9) has a unique zero in the rational box X under a strict four-dimensional Krawczyk inclusion.The interval calculation encloses the actual value of π and uses exact rational endpoints.Source: §3.1 · p. 5
3.2 Direct certification of Romik’s independent system
- A separate 22-dimensional Krawczyk calculation proves a unique zero of Romik’s independent matching and contact equations in the stated rational box.Its maximum certified radius ratio is at most 0.009409749092.Source: §3.2 · pp. 6–7
- The independent full-system check avoids relying on the symbolic elimination that produces the reduced system.The reduced certificate supplies small angle boxes, while the decisive parameter and contact test uses Romik’s equations [6] directly.Source: §3.2 · pp. 6–7
- The certified equations and symmetry make all five path pieces join C1, with x2(T) = 0 and x(T − t) = (ℓ − x1(t), x2(t)).The endpoint condition follows by integrating the second coordinate from x(0) = (0, 0).Source: §3.2 · p. 7
4 Certified global geometry
Exact interval checks certify the path’s support and separation properties, then identify the niche boundary and inner-wall contacts. These results establish the cap and niche geometry needed for the global construction.
4.1 The cap determined by the path
- The oriented support curves attain the rotating support values, and the global half-plane certificate keeps every path point inside all required supporting half-planes.The verifier certifies a continuum margin greater than 0.171132919416.Source: §4.1 · pp. 7–9
- The resulting K0 is a compact convex cap whose reconstructed inner corner is exactly x, with its associated cap in Baek’s construction equal to K0.The endpoint supports and top horizontal support face establish the normalization and rotation angle T.Source: §4.1 · pp. 9–10
4.2 The critical inner-wall separation
- The critical inner-wall separation is strict in the interior: h(ϕ) = h(η) = 0 while h(t) > 0 between them, with h3 positive on [θ, η).At t = T/2, the certified positive lower endpoint exceeds the enclosure width by more than seventeen orders of magnitude.Source: §4.2 · p. 10
4.3 The niche boundary
- The upper niche boundary is the upper envelope of the instantaneous roofs, with the right and reflected left parts given by B|[η,T] and D|[0,θ].The core segment of the envelope is x|[ϕ,τ].Source: §4.3 · pp. 11–12
- The niche is a Jordan region with the stated positively oriented boundary, and no additional inner-wall crossing or hidden component occurs.Its boundary pieces have consecutive horizontal ranges and close to a counterclockwise Jordan curve.Source: §4.3 · pp. 11–13
4.4 Inner-wall contacts and tangent directions
- The inner-wall contacts lie on the specified oriented rays, and at the two junctions the one-sided tangent vectors are positively collinear but have unequal speeds.A local regular C1 reparametrization exists along each geometric arc, though hallway angle is not a classical differentiable parameter there.Source: §4.4 · p. 13
5 Certified admissible motion
The section derives every supporting hallway from the certified support functions, then proves that the fixed set G is a nonempty, closed, connected set carried through the hallway by a continuous rigid-motion path with the required endpoint arms.
5.1 The explicit supporting hallway
- For every t, the two support inequalities identify the hallway as x(t) + R_tL, giving an explicit supporting hallway at every angle.The orthonormal directions u_t and v_t determine the hallway’s two bounding half-planes.Source: §5.1 · p. 14
5.2 The fixed set and its topology
- G is nonempty, closed, and connected; nonemptiness follows because A(0) = (1, 0) lies in K_0 \ N(K_0).Closedness follows from expressing G as the cap intersected with the complement of the open set U.Source: §5.2 · p. 14
5.3 Full continuum containment
- G avoids every inner quadrant, including at the endpoints, and therefore lies within every supporting hallway throughout the full interval.At t = 0 and t = T, the excluded quadrants would require q_2 < 0, contradicting the base constraint on K_0.Source: §5.3 · p. 15
5.4 The rigid-motion path and endpoint arms
- The inverse rigid motions form a continuous path in SE(2) that carries G through the hallway and places it in the initial and final arms.Continuity follows from the C1 corner path; the endpoint estimates give membership in the horizontal arm initially and the vertical arm finally.Source: §5.4 · pp. 15–16
6 Identification with Gerver’s classical sofa
The paper identifies the certified fixed set G with Romik’s reconstruction of Gerver’s classical sofa. Its boundary has the classical eighteen-piece decomposition, while uniqueness is established only within the explicit rational box.
6 Identification with Gerver’s classical sofa
- G equals Romik’s fixed set S_x for the certified five-phase path, identifying it with the reconstructed Gerver sofa.The proof uses hallway and initial-arm membership to show that the two fixed-set descriptions coincide.Source: §6 · pp. 16–17
- The boundary comprises fifteen nonconstant analytic phase arcs and three line segments, matching the classical eighteen-piece decomposition.The analytic pieces comprise four each of A and C, two each of B and D, and three of x; the straight pieces are the top segment and two outer portions of the bottom segment.Source: §6 · pp. 16–17
- The Krawczyk calculation establishes existence and uniqueness in the explicit rational box, not global uniqueness among all real zeros of Romik’s system.The identification concerns the certified solution in the standard Gerver parameter box and its associated fixed set.Source: §6 · p. 17
7 Additional certified geometric properties
The certified cap meets Baek’s injectivity condition and area threshold, with certified tangent-direction signs along the motion. These properties place the cap in Baek’s class K_i.
7 Additional certified geometric properties
- The cap satisfies Baek’s injectivity condition: its support-point path is C1, with nonnegative surface-area densities on the two open semicircles.The phasewise tangent signs are x′(t) · u_t = α(t) < 0 and x′(t) · v_t = β(t) > 0 for 0 < t < T.Source: §7 · p. 17
- |K_0| > 2.4206448441453 > 2.2, so the certified cap exceeds Baek’s area threshold.A height-one trapezoid formed by four support points has area 2a_1, with a_1 > 1.210322422072688751416085718.Source: §7 · pp. 17–18
- Together, the injectivity condition and area bound establish that K_0 belongs to Baek’s class K_i.Source: §7 · pp. 17–18
8 Relation to Baek’s optimality framework
The certified geometric properties supply the Gerver-specific hypotheses used in Baek’s variational framework. For the admissible competitor triples considered there, the paper reports a nonpositive variational quantity.
8 Relation to Baek’s optimality framework
- For the admissible competitor triples considered in Baek’s framework, DQ(K_0, BK_0, DK_0; K*, B*, D*) ≤ 0.The certified motion, cap and niche geometry, contacts, tangent convention, injectivity, and area bounds supply the cited framework’s Gerver-specific hypotheses.Source: §8 · p. 18
- For the application, version 1 of [1] requires “non-positive” in Theorem 8.5.7 cases (3) and (6), J10 in case (8), and B(t3) in Theorem 8.4.3(2)’s B-side identity.These readings are forced by the surrounding formulas and introduce no additional analytic assumption.Source: §8 · pp. 18–19
9 Reproducibility
The verifier is supplied with the preprint and runs using Python’s standard library; its certificate calculations use exact rational arithmetic.
9 Reproducibility
- Run `python3 gerver_interval_verifier.py` from the extracted-files directory using Python 3.10 or later.No third-party package is required.Source: §9 · p. 19
- Trigonometric enclosures use alternating-series bounds and outward rational rounding, while certificate calculations use exact integer and rational arithmetic.Every program decimal is parsed as an exact rational number.Source: §9 · p. 19
- A successful run exits with status 0 and ends with ALL CERTIFICATES PASSED; the verifier is MIT-licensed and has SHA-256 digest e53dd6cd66f3e0f723562e73547828cfcd1bbfe12c3a474c1f70c986e8c975b7.Source: §9 · p. 19
A.1 Four-dimensional Krawczyk data
The appendix gives interval-certificate data, selected certified margins, and reproducibility information, alongside funding and AI-use disclosures.
A.1 Four-dimensional Krawczyk data
- Each row of the four-dimensional Krawczyk calculation is strictly contained in its corresponding input interval.The section also provides the exact rational preconditioner entries.Source: §A.1 · pp. 19–20
A.2 The direct-system box
- The direct-system box lists certified intervals for the parameters, while the complete C22 matrix and exact Krawczyk image are in the hashed verifier.Source: §A.2 · p. 20
A.3 Selected certified margins
- The 22D output/input radius ratio is <0.0095, continuum Gu and Gv exceed 0.171132919416, and trapezoid area exceeds 2.4206448441453775.Other listed margins include an endpoint support separation L > 1.6137632294302516 and lattice Gu, Gv > 0.335732186461.Source: §A.3 · p. 21
Data and code availability
- No external research dataset is used; numerical inputs, interval boxes, certificate data, and source code are in the article and ancillary files.Source: Data and code availability · p. 21
Funding
- The author received no specific grant from any funding agency in the public, commercial, or not-for-profit sectors.Source: Funding · p. 21
AI-assisted research disclosure
- ChatGPT assisted with proof exploration, symbolic checks, verifier development and adversarial testing, and manuscript drafting and revision; the author independently reviewed and verified the work.The AI system is not an author.Source: AI-assisted research disclosure · pp. 21–22