The gyroelongated square bipyramid graph is planar

Proved

OPG37357.X4_isPlanar

by Yuning · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-geometrygraph-theoryplanar-graphs

The graph $X_4$ , the 1-skeleton of the gyroelongated square bipyramid, admits a straight-line planar embedding. In the mission model this means its vertices can be placed injectively in the plane so that no vertex lies in the interior of an edge segment and disjoint edges have disjoint closed segments.

X_4\text{ is planar}.

This supplies the planarity component of the published ten-vertex witness.

Preamble

import Definitions.Def_OPG37357_X4

Formal statement

namespace OPG37357

/-- The explicit ten-vertex witness graph is planar. -/
theorem X4_isPlanar : IsPlanar X4 := by sorry

end OPG37357

Source

Berman--Chappell--Faudree--Gimbel--Hartman--Williams, Graphs with Obstacle Number Greater than One, JGAA 21(6) (2017), https://doi.org/10.7155/jgaa.00452, p. 1117, paragraph following Proposition 5.3 (polyhedral skeletons are planar)

View graph