Lax Lean Archive

Dominating Set

Lax799700.DominatingSet · concepts/Lax799700/DominatingSet.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

    DOMINATING SET: is there a set of vertices, at most as large as the marked set, such that every vertex is in it or adjacent to it? The vocabulary is that of marked graphs, the one Clique and Vertex Cover use. Domination ranges over every element of the universe, so a reduction into it cannot leave junk tuples behind: the first-order reduction from Set Cover makes the junk adjacent to the vertices that a solution always contains. Membership is by an existential second-order definition.

    Concept map
    8 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 dominatingSet_iff proven

    2 dominatingSet_NP_complete proven

    3 hasSmallDominatingSet_iso proven

    Lean source view on GitHub

    1import Mathlib.Data.Fintype.EquivFin
    2import Mathlib.Data.Set.Card
    3import Mathlib.SetTheory.Cardinal.Finite
    4import Mathlib.Logic.Equiv.Prod
    5import Mathlib.ModelTheory.Semantics
    6import Mathlib.ModelTheory.Complexity
    7import Mathlib.Tactic.FinCases
    8import Mathlib.ModelTheory.Syntax
    9import Lax799700.CliqueFamily
    10import Lax904597.Classes
    11import Lax799700.Problems
    12
    13/-!
    14---
    15title: Dominating Set
    16type: theorem
    17---
    18DOMINATING SET: is there a set of vertices, at most as large as the
    19marked set, such that every vertex is in it or adjacent to it? The
    20vocabulary is that of marked graphs, the one Clique and Vertex Cover use.
    21Domination ranges over every element of the universe, so a reduction
    22into it cannot leave junk tuples behind: the first-order reduction from
    23Set Cover makes the junk adjacent to the vertices that a solution always
    24contains. Membership is by an existential second-order definition.
    25
    26-/
    27
    28namespace Lax799700.DominatingSet
    29
    30open Lax799700.CliqueFamily
    31
    32open FirstOrder
    33
    34open Language Structure
    35
    36section Generic
    37
    38variable {A : Type}
    39
    40/-- Some set of vertices dominating the whole graph – every vertex belongs to
    41it or has a neighbor in it – is at most as large as the number encoded by the
    42`Kp`-marked elements. -/
    43def DominatesOn (Adjp : A → A → Prop) (Kp : A → Prop) : Prop :=
    44 ∃ D : A → Prop, (∀ v, D v ∨ ∃ u, D u ∧ Adjp u v) ∧
    45 {v | D v}.ncard ≤ {v | Kp v}.ncard
    46
    47end Generic
    48
    49section Problem
    50
    51variable (A : Type) [markedGraph.Structure A]
    52
    53/-- A marked graph has a dominating set at most as large as its marked set.
    54(Finiteness of the universe is part of the property: cardinality thresholds
    55are only meaningful on finite structures.) -/
    56def HasSmallDominatingSet : Prop :=
    57 Finite A ∧ DominatesOn (MGAdj (A := A)) (MGMarked (A := A))
    58
    59end Problem
    60
    61open Lax904597.Problems Lax904597.Classes Lax799700.Problems
    62
    63/-- The property `HasSmallDominatingSet` is isomorphism-invariant. -/
    64axiom hasSmallDominatingSet_iso : ∀ {A B : Type} [Lax799700.CliqueFamily.markedGraph.Structure A] [Lax799700.CliqueFamily.markedGraph.Structure B],
    65 (A ≃[Lax799700.CliqueFamily.markedGraph] B) → (HasSmallDominatingSet A ↔ HasSmallDominatingSet B)
    66
    67/-- The problem DominatingSet: does the structure satisfy `HasSmallDominatingSet`? -/
    68def DominatingSet : DecisionProblem Lax799700.CliqueFamily.markedGraph :=
    69 DecisionProblem.ofPred HasSmallDominatingSet
    70
    71/-- The yes-instances of DominatingSet are exactly the structures satisfying
    72`HasSmallDominatingSet`. -/
    73axiom dominatingSet_iff : ∀ (A : Type) [Lax799700.CliqueFamily.markedGraph.Structure A], DominatingSet A ↔ HasSmallDominatingSet A
    74
    75/-- DominatingSet is NP-complete. -/
    76axiom dominatingSet_NP_complete : NP.Complete DominatingSet
    77
    78end Lax799700.DominatingSet
    79
    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…