The graph X₄ has no ordinary one-obstacle drawing

Open

OPG37357.X4_not_obstacleNumberAtMost_one

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

computational-geometrygraph-theorysatvisibility-graphs

No injective placement of the ten vertices of $X_4$ can realize exactly its adjacencies using a single polygonal obstacle in the mission model.

\operatorname{obs}(X_4)>1.

This is the lower-bound component of the published computer-assisted result and is the principal remaining formalization frontier.

Preamble

import Definitions.Def_OPG37357_X4

Formal statement

namespace OPG37357

/-- The explicit ten-vertex witness graph cannot be realized with one polygonal obstacle. -/
theorem X4_not_obstacleNumberAtMost_one : ¬ ObstacleNumberAtMost X4 1 := 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, pp. 1115--1117, Lemma 5.1, Observation 5.2, and Proposition 5.3(1)

View graph