OPG-37357: a universal obstacle bound for planar graphs
OpenOPG37357.universal_planar_boundThere exists one natural number such that every finite simple planar graph has an ordinary obstacle drawing using at most polygonal obstacles:
The bound is chosen before the graph and is independent of graph order. The obstacle drawing need not be a crossing-free drawing of the graph.
import Definitions.Def_opg37357_obstacle_number
namespace OPG37357
/-- The still-open second part: a uniform finite obstacle bound for all finite
planar graphs. -/
theorem universal_planar_bound :
∃ k : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)),
IsPlanar G → ObstacleNumberAtMost G k := by sorry
end OPG37357Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
There exists a natural number k such that, for every natural number n, including n = 0, and every simple graph G on the vertex set of natural numbers less than n, the following implication holds: if there is an injective placement p of the vertices in the plane such that no nonendpoint vertex lies on the joining segment of an edge and the joining segments of any two edges with four pairwise distinct endpoints are disjoint, then there exists a k-obstacle drawing of G. Such a drawing has an injective vertex placement, one polygonal obstacle for each index i with 0 ≤ i < k, pairwise disjoint obstacle regions, every vertex outside every obstacle region, and adjacency of each distinct vertex pair exactly when its joining segment avoids every obstacle region. Each obstacle region is the union of the triangle sets generated by a nonempty finite list of ordered triples of plane points, and each such union is preconnected. The natural number k is not otherwise restricted, so k = 0 is included.
Confirmed by the mission captain (proposal self-audit).