Lax Lean Archive

3-colorability

Lax799700.ThreeColorability · concepts/Lax799700/ThreeColorability.lean · lax-799700

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A graph is a structure of Mathlib's graph vocabulary, a single binary relation; ThreeColorable says some map into three colors separates every adjacent pair, and ThreeCol is the decision problem. A self-loop makes a structure a no-instance. On structures arising from Mathlib's simple graphs the property agrees with Mathlib's colorability. Membership in NP is by a first-order reduction to SAT, hardness by an ordered first-order reduction from SAT.

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 threeCol_iff proven

    2 threeCol_NP_complete proven

    3 threeColorable_iso proven

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Graph
    2import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
    3import Mathlib.ModelTheory.Semantics
    4import Mathlib.ModelTheory.Complexity
    5import Mathlib.Tactic.FinCases
    6import Lax904597.Classes
    7import Lax799700.Problems
    8
    9/-!
    10---
    11title: 3-colorability
    12type: theorem
    13---
    14A graph is a structure of Mathlib's graph vocabulary, a single binary
    15relation; ThreeColorable says some map into three colors separates every
    16adjacent pair, and ThreeCol is the decision problem. A self-loop makes a
    17structure a no-instance. On structures arising from Mathlib's simple
    18graphs the property agrees with Mathlib's colorability. Membership in NP
    19is by a first-order reduction to SAT, hardness by an ordered first-order
    20reduction from SAT.
    21
    22-/
    23
    24namespace Lax799700.ThreeColorability
    25
    26open FirstOrder
    27
    28open Language Structure
    29
    30section Graph
    31
    32variable (V : Type) [Language.graph.Structure V]
    33
    34/-- A `Language.graph`-structure is 3-colorable if the vertices can be colored
    35with 3 colors so that adjacent vertices get distinct colors. (On structures
    36with self-loops this is never satisfiable, matching the usual convention.) -/
    37def ThreeColorable : Prop :=
    38 ∃ c : V → Fin 3, ∀ x y : V, RelMap adj ![x, y] → c x ≠ c y
    39
    40end Graph
    41
    42open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    43
    44/-- The property `ThreeColorable` is isomorphism-invariant. -/
    45axiom threeColorable_iso : ∀ {A B : Type} [FirstOrder.Language.graph.Structure A] [FirstOrder.Language.graph.Structure B],
    46 (A ≃[FirstOrder.Language.graph] B) → (ThreeColorable A ↔ ThreeColorable B)
    47
    48/-- The problem ThreeCol: does the structure satisfy `ThreeColorable`? -/
    49def ThreeCol : DecisionProblem FirstOrder.Language.graph :=
    50 DecisionProblem.ofPred ThreeColorable
    51
    52/-- The yes-instances of ThreeCol are exactly the structures satisfying
    53`ThreeColorable`. -/
    54axiom threeCol_iff : ∀ (A : Type) [FirstOrder.Language.graph.Structure A], ThreeCol A ↔ ThreeColorable A
    55
    56/-- ThreeCol is NP-complete. -/
    57axiom threeCol_NP_complete : NP.Complete ThreeCol
    58
    59end Lax799700.ThreeColorability
    60
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…