Polygonal obstacle drawings and ordinary obstacle number
Definitionopg37357_obstacle_numberThis module defines an ordinary obstacle drawing of a finite simple graph. Vertices are placed injectively in . Each obstacle is a closed connected polygonal region represented by a nonempty finite union of filled closed triangles; distinct obstacle regions are disjoint and contain no graph vertex.
Two distinct vertices are adjacent exactly when their closed joining segment is disjoint from every obstacle. ObstacleNumberAtMost G k means that such a drawing exists with indexed obstacles. Straight-line planarity of the abstract graph is defined independently and does not require the obstacle drawing itself to be crossing-free.
Segment contact with an obstacle boundary counts as blocked visibility. Degenerate triangle pieces are not excluded, while the whole obstacle region must be preconnected.
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Topology.Connected.Basic
import Mathlib.Topology.UniformSpace.Real
import Mathlib.Topology.Constructions.SumProd
namespace OPG37357
universe u
abbrev Point := ℝ × ℝ
def affine2 (a b : Point) (t : ℝ) : Point :=
((1 - t) * a.1 + t * b.1, (1 - t) * a.2 + t * b.2)
def closedSegment (a b : Point) : Set Point :=
{x | ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧ x = affine2 a b t}
def closedTriangle (a b c : Point) : Set Point :=
{x | ∃ α β γ : ℝ,
0 ≤ α ∧ 0 ≤ β ∧ 0 ≤ γ ∧ α + β + γ = 1 ∧
x = (α * a.1 + β * b.1 + γ * c.1,
α * a.2 + β * b.2 + γ * c.2)}
/-- A closed connected polygonal obstacle, represented by a nonempty finite
union of filled closed triangles. -/
structure PolygonalObstacle where
pieces : List (Point × Point × Point)
pieces_nonempty : pieces ≠ []
region_connected : IsPreconnected
{x | ∃ t ∈ pieces, x ∈ closedTriangle t.1 t.2.1 t.2.2}
/-- The closed region occupied by a polygonal obstacle. -/
def PolygonalObstacle.region (O : PolygonalObstacle) : Set Point :=
{x | ∃ t ∈ O.pieces, x ∈ closedTriangle t.1 t.2.1 t.2.2}
/-- A drawing by `k` pairwise disjoint polygonal obstacles. Vertices avoid all
obstacles, and two distinct vertices are adjacent exactly when their closed
joining segment avoids every obstacle. -/
structure ObstacleDrawing {V : Type u} (G : SimpleGraph V) (k : ℕ) where
position : V → Point
position_injective : Function.Injective position
obstacle : Fin k → PolygonalObstacle
obstacles_disjoint : ∀ ⦃i j : Fin k⦄, i ≠ j →
Disjoint (obstacle i).region (obstacle j).region
vertices_free : ∀ (v : V) (i : Fin k), position v ∉ (obstacle i).region
realizes : ∀ ⦃u v : V⦄, u ≠ v →
(G.Adj u v ↔ ∀ i : Fin k,
Disjoint (closedSegment (position u) (position v)) (obstacle i).region)
/-- The ordinary obstacle number of `G` is at most `k`. -/
def ObstacleNumberAtMost {V : Type u} (G : SimpleGraph V) (k : ℕ) : Prop :=
Nonempty (ObstacleDrawing G k)
/-- Straight-line planarity, used only to state that the abstract graph is
planar; it does not constrain the obstacle drawing. -/
def IsPlanar {V : Type u} (G : SimpleGraph V) : Prop :=
∃ p : V → Point,
Function.Injective p ∧
(∀ ⦃a b v : V⦄, G.Adj a b → v ≠ a → v ≠ b → p v ∉ closedSegment (p a) (p b)) ∧
(∀ ⦃a b c d : V⦄, G.Adj a b → G.Adj c d →
a ≠ c → a ≠ d → b ≠ c → b ≠ d →
Disjoint (closedSegment (p a) (p b)) (closedSegment (p c) (p d)))
end OPG37357Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
Point is the set of ordered pairs of real numbers. For points a and b and a real number t, affine2 a b t is the point whose coordinates are ((1 − t)a₁ + ta₂? No: more precisely, ((1 − t)a₁ + tb₁, (1 − t)a₂ + tb₂), where a = (a₁,a₂) and b = (b₁,b₂). The set closedSegment a b consists of all points affine2 a b t for real t satisfying 0 ≤ t ≤ 1. The set closedTriangle a b c consists of all points (αa₁ + βb₁ + γc₁, αa₂ + βb₂ + γc₂) for real α, β, γ satisfying α ≥ 0, β ≥ 0, γ ≥ 0, and α + β + γ = 1. Degenerate triangles are not excluded.
A PolygonalObstacle consists of a nonempty finite list of ordered triples of points, together with the assertion that the union of the corresponding closed triangles is preconnected in the usual topology on the plane.
For a polygonal obstacle O, O.region is the union of the closed triangles determined by the triples in O's list.
For a simple graph G on a type V and a natural number k, an ObstacleDrawing G k consists of an injective position map from V to the plane, a map assigning a polygonal obstacle to each index i with 0 ≤ i < k, pairwise disjoint regions for distinct obstacle indices, and the requirement that every vertex position lies outside every assigned obstacle region. It also requires that, for every pair of distinct vertices u and v, u and v are adjacent in G exactly when, for every obstacle index i, the segment joining their positions is disjoint from the region of obstacle i. If k = 0, all index-dependent requirements are vacuous and the adjacency condition requires every pair of distinct vertices to be adjacent.
ObstacleNumberAtMost G k means that at least one such k-obstacle drawing of G exists.
IsPlanar G means that there exists an injective map p from the vertices of G to the plane such that every vertex other than the endpoints of an edge lies outside the segment joining those endpoints, and any two edges whose four endpoints are pairwise distinct have disjoint joining segments. The quantifiers range over all vertices and all edges satisfying the stated inequalities.
Confirmed by the mission captain (proposal self-audit).