A finite planar graph of obstacle number two
OpenOPG37357.planar_graph_above_oneThere exists a finite simple planar graph whose ordinary obstacle number is exactly two in the mission's polygonal model:
This is the published positive answer to the first part of OPG-37357. The existential statement permits formalization using any of the planar examples proved in the cited paper.
import Definitions.Def_opg37357_obstacle_number
namespace OPG37357
/-- Published positive answer to the first part: some finite planar graph has
ordinary obstacle number exactly two. -/
theorem planar_graph_above_one :
∃ n : ℕ, ∃ G : SimpleGraph (Fin n),
IsPlanar G ∧ ObstacleNumberAtMost G 2 ∧ ¬ ObstacleNumberAtMost G 1 := by sorry
end OPG37357Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
There exist a natural number n and a simple graph G whose vertex set is the set of natural numbers less than n such that all three conditions hold: G has a map p into the plane that is injective, places every vertex other than the endpoints of an edge outside that edge's joining segment, and gives disjoint joining segments to any two edges with four pairwise distinct endpoints; there exists a 2-obstacle drawing of G; and there does not exist a 1-obstacle drawing of G. Here a k-obstacle drawing means an injective placement of the vertices in the plane, one polygonal obstacle for each index i with 0 ≤ i < k, pairwise disjoint obstacle regions, every vertex outside every obstacle region, and, for every distinct pair of vertices u and v, adjacency exactly when the joining segment is disjoint from every obstacle region. Each polygonal obstacle is specified by a nonempty finite list of ordered triples of plane points; its region is the union of the corresponding sets of nonnegative affine combinations whose three coefficients sum to 1, and that union is preconnected. The assertion includes all natural n, including n = 0, as possible witnesses.
Confirmed by the mission captain (proposal self-audit).