#Clique: counting the cliques of the threshold size

The counting version of DescriptiveComplexity.Clique: the number of cliques having exactly as many vertices as the marked set (DescriptiveComplexity.CliqueOfSize). Its support is Clique, a clique at least as large as the threshold containing one of exactly that size.

Membership in #P (DescriptiveComplexity.sharpClique_mem_sharpP) is the first in the catalog whose kernel reads the order of the instance. The Σ₁ definition of Clique certifies the threshold by an injection of the marked set into the clique, and a clique has many; even for the exact size, a bijection is one among k!. The counting kernel asks for the monotone one, which exists and is unique on a finite linear order. That argument is generic (DescriptiveComplexity.sharpPDefinable_of_sized_set), and what this file supplies is the order-free part: a set is a clique (DescriptiveComplexity.cliqueSelKernel).

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

The set S is a clique 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.

theorem DescriptiveComplexity.CliqueOfSize.map {A : Type} [FirstOrder.Language.markedGraph.Structure A] {B : Type} [FirstOrder.Language.markedGraph.Structure B] (e : FirstOrder.Language.markedGraph.Equiv A B) {S : A → Prop} (h : CliqueOfSize A S) : CliqueOfSize B fun (b : B) => S (e.symm b)

Cliques of the threshold size transport along an isomorphism.

The order-free kernel

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqCliqueSelBlockIx : DecidableEq CliqueSelBlockIx

Equations

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

inductive DescriptiveComplexity.CliqueSelBlockIx : Type

The relation variables of the block.

• sel : CliqueSelBlockIx

  The clique.

def DescriptiveComplexity.cliqueSelBlock : SOBlock

The block of the counting definition of Clique: the clique itself. Its size is certified generically, by DescriptiveComplexity.sharpPDefinable_of_sized_set.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.csMarkedSym : cliqueSelLang.Relations 1

The marked symbol over the sum.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.csAdjSym : cliqueSelLang.Relations 2

The adj symbol over the sum.

Equations

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

def DescriptiveComplexity.csSelRel : cliqueSelBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.csSelRel = ⟨DescriptiveComplexity.CliqueSelBlockIx.sel, DescriptiveComplexity.csSelRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.cliqueSelLang : FirstOrder.Language

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

Equations

• DescriptiveComplexity.cliqueSelLang = FirstOrder.Language.markedGraph.sum DescriptiveComplexity.cliqueSelBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.csSelSym : cliqueSelLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.csSelSym = Sum.inr DescriptiveComplexity.csSelRel

@[instance_reducible]

instance DescriptiveComplexity.instFintypeCliqueSelBlockIx : Fintype CliqueSelBlockIx

Equations

• DescriptiveComplexity.instFintypeCliqueSelBlockIx = { elems := [DescriptiveComplexity.CliqueSelBlockIx.sel].toFinset, complete := DescriptiveComplexity.instFintypeCliqueSelBlockIx._proof_1 }

instance DescriptiveComplexity.instSubsingletonιCliqueSelBlock : Subsingleton cliqueSelBlock.ι

The counting problem

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

#Clique: the number of cliques with exactly as many vertices as the marked set.

Equations

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

theorem DescriptiveComplexity.sharpClique_support_iff (A : Type) [FirstOrder.Language.markedGraph.Structure A] [Finite A] : SharpClique.support.Holds A ↔ Clique.Holds A

The support of #Clique is Clique: a clique at least as large as the marked set contains one of exactly that size. Registered in the Lax archive as Lax280166.CliqueComplete.sharpClique_support_iff.

theorem DescriptiveComplexity.sharpClique_mem_sharpP : SharpP.Mem SharpClique

#Clique is in #P: a clique of the threshold size has exactly one monotone bijection with the marked set.