Circular colorings and straight-line planarity for OPG-401
Definitionopg401_circular_coloringThis module fixes the finite graph model for OPG-401. A planar graph is supplied with an injective straight-line drawing in the real plane: no third vertex lies on an edge segment, and segments for nonincident edges are disjoint. Triangle-free and subcubic predicates are literal graph conditions.
For residues modulo , the circular distance is the shorter of the two directed modular differences. Two colors are -compatible when their circular distance lies between and , inclusive. A -coloring assigns compatible residues to every adjacent pair. The module also defines the exact allowed-color set next to a residue for the palette .
The definitions include disconnected and empty finite graphs. Values are represented by Fin p, and natural subtraction is used only in formulas where the residue representatives make the modular differences well-defined.
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Finset.Card
import Mathlib.Data.Real.Basic
import Mathlib.Data.Set.Card
namespace OPG401
universe u
abbrev Point := ℝ × ℝ
def pointOnSegment (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 = pointOnSegment a b t}
def openSegment (a b : Point) : Set Point :=
{x | ∃ t : ℝ, 0 < t ∧ t < 1 ∧ x = pointOnSegment a b t}
/-- A finite graph is represented as planar by an injective straight-line drawing:
no third vertex lies on an edge, and nonincident edges are disjoint. -/
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)))
/-- The graph contains no triangle. -/
def IsTriangleFree {V : Type u} (G : SimpleGraph V) : Prop :=
∀ ⦃a b c : V⦄, G.Adj a b → G.Adj b c → ¬ G.Adj c a
/-- Every vertex has at most three neighbors. -/
def IsSubcubic {V : Type u} (G : SimpleGraph V) : Prop :=
∀ v : V, (G.neighborSet v).encard ≤ 3
/-- Shortest cyclic distance between two residues modulo `p`. -/
def circularDistance {p : ℕ} (a b : Fin p) : ℕ :=
min ((a.val + p - b.val) % p) ((b.val + p - a.val) % p)
/-- The edge constraint for a `(p,q)`-coloring, using shortest cyclic distance. -/
def PQCompatible (p q : ℕ) (a b : Fin p) : Prop :=
q ≤ circularDistance a b ∧ circularDistance a b ≤ p - q
/-- A `(p,q)`-coloring of a simple graph. -/
def IsPQColoring {V : Type u} (G : SimpleGraph V) (p q : ℕ)
(color : V → Fin p) : Prop :=
∀ ⦃u v : V⦄, G.Adj u v → PQCompatible p q (color u) (color v)
/-- The colors that may be assigned next to a vertex of color `a` in a
`(20,7)`-coloring. -/
noncomputable def allowedColors (a : Fin 20) : Finset (Fin 20) := by
classical
exact Finset.univ.filter fun z => PQCompatible 20 7 z a
end OPG401Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
Point and segment definitions. Point is the type ℝ × ℝ of ordered pairs of real numbers. For points a = (a₁,a₂), b = (b₁,b₂), and t ∈ ℝ, pointOnSegment a b t is the point ((1 − t)a₁ + t b₁, (1 − t)a₂ + t b₂). closedSegment a b is the set of points x for which there exists t ∈ ℝ with 0 ≤ t ≤ 1 and x = pointOnSegment a b t; openSegment a b is defined identically but with 0 < t < 1.
IsPlanar. For any type V and simple graph G on V, IsPlanar G means that there exists a function p : V → ℝ × ℝ that is injective, such that for every a,b,v ∈ V, if a is adjacent to b and v ≠ a and v ≠ b, then p(v) is not of the form ((1 − t)p(a)₁ + t p(b)₁, (1 − t)p(a)₂ + t p(b)₂) for any real t with 0 ≤ t ≤ 1; and such that for every a,b,c,d ∈ V, if a is adjacent to b, c is adjacent to d, and a ≠ c, a ≠ d, b ≠ c, and b ≠ d, then the two closed segments from p(a) to p(b) and from p(c) to p(d) have no common point.
IsTriangleFree. For every a,b,c ∈ V, if a is adjacent to b and b is adjacent to c, then c is not adjacent to a. IsSubcubic. Every vertex v ∈ V has a neighbor set whose extended cardinality is at most 3; equivalently, there are at most three distinct neighbors of v.
Circular distance and coloring. For p ∈ ℕ and residues a,b ∈ Fin p, circularDistance a b is the natural number
where a.val and b.val are their natural-number representatives and subtraction is natural-number subtraction. If p = 0 there are no such residues. PQCompatible p q a b means q ≤ circularDistance(a,b) and circularDistance(a,b) ≤ p − q, with the latter subtraction also taken in ℕ and therefore truncated at zero. IsPQColoring G p q color, for a function color : V → Fin p, means that every adjacent pair u,v in G satisfies these two inequalities for color(u) and color(v).
Allowed colors. For a ∈ Fin 20, allowedColors a is the finite set of all z ∈ Fin 20 satisfying
All quantifiers above include empty or degenerate types and graphs where the relevant conditions become vacuous.
Confirmed by the mission captain (proposal self-audit).