#Dominating Set: counting the dominating sets of the threshold size

The counting version of DescriptiveComplexity.DominatingSet: the number of dominating sets with exactly as many vertices as the marked set (DescriptiveComplexity.DomSetOfSize). Its support is Dominating Set, a dominating set smaller than the threshold extending to one of exactly that size (DescriptiveComplexity.sharpDominatingSet_support_iff).

Membership in #P (DescriptiveComplexity.sharpDominatingSet_mem_sharpP) is the generic argument for a solution of the threshold size (DescriptiveComplexity.sharpPDefinable_of_sized_set), domination being first-order. Parsimonious hardness is in DescriptiveComplexity.Problems.DominatingSet.CountingHardness.

def DescriptiveComplexity.DomOfSizeOn {A : Type} (Adjp : A → A → Prop) (Kp D : A → Prop) : Prop

The set D dominates every vertex and has exactly as many elements as the Kp-marked set.

Equations

• DescriptiveComplexity.DomOfSizeOn Adjp Kp D = ((∀ (v : A), D v ∨ ∃ (u : A), D u ∧ Adjp u v) ∧ {v : A | D v}.ncard = {v : A | Kp v}.ncard)

def DescriptiveComplexity.domOfSizeEquiv {A B : Type} (u : B ≃ A) {AdjB : B → B → Prop} {KB : B → Prop} {AdjA : A → A → Prop} {KA : A → Prop} (hadj : ∀ (b b' : B), AdjB b b' ↔ AdjA (u b) (u b')) (hK : ∀ (b : B), KB b ↔ KA (u b)) : { D : B → Prop // Finite B ∧ DomOfSizeOn AdjB KB D } ≃ { D : A → Prop // Finite A ∧ DomOfSizeOn AdjA KA D }

The dominating sets of the threshold size transport along an equivalence commuting with the two predicates.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.DomSetOfSize (A : Type) [FirstOrder.Language.markedGraph.Structure A] (D : A → Prop) : Prop

The set D is a dominating set with exactly as many vertices as the marked set, in a finite marked graph.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.SharpDominatingSet : CountingProblem FirstOrder.Language.markedGraph

#Dominating Set: the number of dominating sets with exactly as many vertices as the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpDominatingSet_support_iff (A : Type) [FirstOrder.Language.markedGraph.Structure A] [Finite A] : SharpDominatingSet.support.Holds A ↔ DominatingSet.Holds A

The support of #Dominating Set is Dominating Set: a dominating set at most as large as the marked set extends to one of exactly that size. Registered in the Lax archive as Lax280166.DominatingSetComplete.sharpDominatingSet_support_iff.

Membership

def DescriptiveComplexity.domSelBlock : SOBlock

The block of the counting definition of Dominating Set: the dominating set itself.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqDomSelBlockIx : DecidableEq DomSelBlockIx

Equations

• DescriptiveComplexity.instDecidableEqDomSelBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev DescriptiveComplexity.dmMarkedSym : domSelLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.dmMarkedSym = Sum.inl FirstOrder.Language.mgMarked

def DescriptiveComplexity.dmSelRel : domSelBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.dmSelRel = ⟨DescriptiveComplexity.DomSelBlockIx.sel, DescriptiveComplexity.dmSelRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instFintypeDomSelBlockIx : Fintype DomSelBlockIx

Equations

• DescriptiveComplexity.instFintypeDomSelBlockIx = { elems := [DescriptiveComplexity.DomSelBlockIx.sel].toFinset, complete := DescriptiveComplexity.instFintypeDomSelBlockIx._proof_1 }

inductive DescriptiveComplexity.DomSelBlockIx : Type

The relation variables of the block.

• sel : DomSelBlockIx

  The dominating set.

@[reducible, inline]

abbrev DescriptiveComplexity.dmSelSym : domSelLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.dmSelSym = Sum.inr DescriptiveComplexity.dmSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.domSelLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.domSelLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.domSelBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.dmAdjSym : domSelLang.Relations 2

The adj symbol over the sum.

Equations

• DescriptiveComplexity.dmAdjSym = Sum.inl FirstOrder.Language.mgAdj

instance DescriptiveComplexity.instSubsingletonιDomSelBlock : Subsingleton domSelBlock.ι

theorem DescriptiveComplexity.sharpDominatingSet_mem_sharpP : SharpP.Mem SharpDominatingSet

#Dominating Set is in #P.