The graph X₄ has an ordinary two-obstacle drawing

Open

OPG37357.X4_obstacleNumberAtMost_two

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

computational-geometrygraph-theoryvisibility-graphs

The graph $X_4$ has an ordinary obstacle representation using two polygonal obstacles in the mission model. Vertices are placed injectively; distinct vertices are adjacent exactly when their joining segment avoids both obstacles.

\operatorname{obs}(X_4)\le 2.

This is the constructive upper-bound component of the published result.

Preamble

import Definitions.Def_OPG37357_X4

Formal statement

namespace OPG37357

/-- The explicit ten-vertex witness graph has a drawing with two polygonal obstacles. -/
theorem X4_obstacleNumberAtMost_two : ObstacleNumberAtMost X4 2 := 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. 1112--1113, Proposition 3 and Figure 4 (a two-obstacle representation of X_4); also p. 1117, Proposition 5.3(1)

View graph