Certified Geometry and Admissible Motion of Gerver's Sofa
Abstract
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 Φ_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.
Related
- New certified lower bounds for the moving sofa problem in a three-dimensional snaky corridor
- Learning the Geometry of Admissible Hypotheses through Inductive Bias in Training Distributions
- The data geometry of masking diffusion: Certified-optimal schedules via unmasking growth complexity
- Common-Center Geometry and Certified Radial Reconstruction for Energy-Form Full Conformal Regions
- Brown-Gerver-Ramsey Theorems in Small Dimensions
BibTeX
@misc{trela2026certified,
title = {{Certified Geometry and Admissible Motion of Gerver's Sofa}},
author = {Dawid Trela},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.13955},
eprint = {2610.13955},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.13955},
}
RIS
TY - UNPB
TI - Certified Geometry and Admissible Motion of Gerver's Sofa
AU - Dawid Trela
PY - 2026
DA - 2026/10/01
PB - arXiv
DO - 10.48550/arxiv.2610.13955
UR - https://arxiv.org/abs/2610.13955
AB - 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 Φ_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.
ER -