A lower bound you can move, an upper-bound proof you can inspect

Eighteen Curves Turn the Corner

Turn Gerver's equation-built sofa through a unit-width corner, recompute its area, then operate the injectivity iteration behind Jineon Baek's claimed proof of optimality. The result is presented as a preprint claim because completed peer review could not be verified.

Claimed resolution in arXiv:2411.19826 v1, peer review not verified complete

Layer one: make it fit

Drag first. The sofa stays fixed while the hallway follows Romik's five-phase rotation path. This dual viewpoint is mathematically equivalent to moving the sofa through a fixed hallway. The pale shape is regenerated from the solved path as an intersection of sampled hallway positions, not traced from an image.

Rotation

solving equations

The canvas will report the rotation, phase, active contacts, solved area, and hallway width here.

A C D
corner A C D
corner A C
corner A B C
A B C
area from live quadraturecomputing
active boundary membersA C D
scale checkarea × width²

Gerver's boundary has 18 analytic pieces in the source decomposition: 3 straight segments and 15 curved segments. The live canvas uses the equivalent hallway-intersection definition from Romik's Equation 8. Its finite sampling is a visualization of feasibility, not a continuous collision certificate.

Layer two: fitting is not optimality

A successful turn only supplies a lower bound. It cannot rule out a larger shape with a stranger motion. Baek's preprint closes that gap through an injectivity condition and then a concave quadratic upper-bound functional. The first instrument below runs the actual lower-bound operator from Definitions 6.5.1 and 6.5.2. The second exposes the quadratic identity on a normalized support-mode slice.

Baek iteration

f₀ at t = π/4

A text report of the selected lower-bound function appears here.

The actual recurrence

m₀(x) = x − max(|x−1|, (|x−1|+1)/2)
Ff(x) = 1 + ∫₀ˣ m₀(f(π/2−u)) du
fₙ₊₁(x) = max(fₙ(x), Ffₙ(x))

The analytic certificate

computing the two closed-form margins

The curves are finite-grid numerical illustrations. The printed 1/12 ladder is Baek's analytic argument. This page evaluates its closed-form margins with ordinary floating point, not directed-rounding interval arithmetic, so the browser display is not itself a rigorous interval proof.

A normalized quadratic support-mode slice

q(0) = area

The selected quadratic value and concavity identity appear here.

This is an exact one-mode demonstration of the quadratic concavity identity, normalized so q(0) equals the computed Gerver area and q′(0) equals zero. It is not a browser evaluation of Baek's full geometric functional Q(K,B,D). That full functional, its enclosing region, and its directional-derivative proof remain in Chapter 8 of the preprint.

Open variant

solving Romik's cubics

X²(X+3)=8, Y(4Y²+3)=1, area = X+atan(Y)

The positive roots and residuals are computed in this browser. This candidate turns both left and right. Neither Romik's paper nor the sources checked for this page prove that it is the largest ambidextrous sofa.

The check

Six independent readouts expose the load-bearing computations. Every value below is filled by the page's own JavaScript after load.

1. Breakpoint system

waiting

2. Path joins

waiting

3. Area cross-check

waiting

4. Motion sampling

waiting

5. Conditional bound

waiting

6. Ambidextrous roots

waiting

Conventions, free choices, approximations, and uncertainties
  • Units: quoted constants use hallway width 1. Length scales with width and area with width squared.
  • Viewpoint: the sofa is fixed and the hallway moves. This is Romik's dual convention.
  • Root finding: damped Newton iteration starts from the freely chosen seed (A,B,φ,θ) = (0.1,1.4,0.04,0.68). Ordinary binary64 arithmetic is used.
  • Quadrature: adaptive Simpson integration stops at a requested tolerance. The doubling cross-check uses an independently coded composite Simpson rule.
  • Equation transcription can be wrong. The offline verifier extracts this page's shipped functions and compares them with separately written formulas and source values.
  • The rendered shape intersects 121 sampled hallway positions. Finite sampling shows the motion but does not certify every time in a continuum.
  • The ODE path check covers four phase joins. It does not independently certify positional continuity at every endpoint of the source's 18-piece boundary decomposition.
  • The f curves use 1,600 grid intervals. The analytic inequalities printed beside them come from Baek's proof, but the browser does not implement directed rounding.
  • The quadratic slice is a faithful algebraic demonstration, not Baek's complete Q functional.
  • Publication status: arXiv still exposed only v1 when checked on 29 July 2026. POSTECH notices dated 6 January and 2 February 2026 said peer review was in progress. No completed refereed publication was located, which is not proof that none exists.
What is still open

Romik's ambidextrous problem asks for one connected shape that can turn both left and right through unit-width right-angle corners. His exact candidate is computed above, but optimality was not verified. The related T-junction variant may share its optimum, but the checked source does not prove that equality. Baek's theorem concerns the original single right-angle turn. It does not settle general turn angles, curved hallways, several nearby turns, or three-dimensional corridors.

Primary sources and status
  1. Jineon Baek, Optimality of Gerver's Sofa, arXiv:2411.19826v1, submitted 29 November 2024 at 16:37:23 UTC. Preprint, 119 pages. This is the claimed optimality proof and source of the f iteration and Q proof chain.
  2. Joseph L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42, 267 to 283, June 1992, DOI 10.1007/BF02414066. Peer-reviewed. This is the 18-piece construction.
  3. Dan Romik, Differential Equations and Exact Solutions in the Moving Sofa Problem, Experimental Mathematics 27(3), 316 to 330, online 19 January 2017, DOI 10.1080/10586458.2016.1270858. Peer-reviewed. This is the ODE path, contact equations, area computation, and ambidextrous candidate.
  4. Yoav Kallus and Dan Romik, Improved upper bounds in the moving sofa problem, Advances in Mathematics 340, 960 to 982, 15 December 2018, DOI 10.1016/j.aim.2018.10.022. Peer-reviewed. This is the prior 2.37 upper bound and a published decimal for Gerver's area.
  5. Jineon Baek, A Conditional Upper Bound for the Moving Sofa Problem, arXiv:2406.10725, submitted 15 June 2024. Preprint. This is the injectivity-conditional bound recomputed below.
  6. Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner, Mathematical exploration and discovery at scale, arXiv:2511.02864v3, revised 22 December 2025. Preprint. Its moving-sofa section still describes Romik's ambidextrous value as a lower bound whose sharpness is open.
  7. POSTECH Department of Mathematics, institutional notice dated 6 January 2026. Announcement, not peer review. It said the paper was undergoing peer review.