Counting the solutions of exactly the threshold size

A threshold problem in the unary representation asks for a set at least, or at most, as large as a marked set, and its counting version counts the solutions of exactly that size. Such a count is #P-definable as soon as the property of the set is first-order, and this file says so once for all of them (DescriptiveComplexity.sharpPDefinable_of_sized, and DescriptiveComplexity.sharpPDefinable_of_sized_set when the set is the whole certificate).

The input is a kernel φ₀ over a block B, one of whose unary variables i₀ is the set being sized, and the symbol mk of the marked set. The kernel may read the order (DescriptiveComplexity.sharpPDefinable_of_sized_ordered, for a certificate walking the order, as the reachability clock of Steiner Tree does) or not (DescriptiveComplexity.sharpPDefinable_of_sized). The counting kernel (DescriptiveComplexity.sizedKernel) adds one binary variable and asks it to be the graph of the monotone bijection from the marked set onto the set (DescriptiveComplexity.MonoBij): a bijection certifies the size, and the monotone one is the only certificate, so the witnesses of the kernel are the assignments of B satisfying φ₀ whose set has the size of the marked one (DescriptiveComplexity.witnessCount_sizedKernel), whatever the linear order.

The extra variable is that of DescriptiveComplexity.SOBlock.withOrder, reused for its assignment bookkeeping: there it is an order being re-quantified, here a bijection.

def DescriptiveComplexity.sizedLHom (L : FirstOrder.Language) (B : SOBlock) : (L.sum FirstOrder.Language.order).sum B.lang →ᴸ (L.sum FirstOrder.Language.order).sum B.withOrder.lang

The inclusion of the vocabulary of a kernel into that of the sized kernel: the bijection variable is added to the block.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.szMkSym (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 1) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Relations 1

The mark symbol over the vocabulary of the sized kernel.

Equations

• DescriptiveComplexity.szMkSym L B mk = Sum.inl (Sum.inl mk)

@[reducible, inline]

abbrev DescriptiveComplexity.szSelSym (L : FirstOrder.Language) (B : SOBlock) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Relations 1

The sized set, as a symbol of the sized kernel.

Equations

• DescriptiveComplexity.szSelSym L B i₀ h₀ = Sum.inr ⟨Sum.inr i₀, h₀⟩

@[reducible, inline]

abbrev DescriptiveComplexity.szBijSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Relations 2

The bijection variable, as a symbol of the sized kernel.

Equations

• DescriptiveComplexity.szBijSym L B = Sum.inr B.orderSym

@[reducible, inline]

abbrev DescriptiveComplexity.szLeSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Relations 2

The order symbol over the vocabulary of the sized kernel.

Equations

• DescriptiveComplexity.szLeSym L B = Sum.inl (Sum.inr FirstOrder.Language.leSymb)

def DescriptiveComplexity.szMk (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 1) {α : Type} (x : α) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Formula α

x is marked, as a formula of the sized kernel.

Equations

• DescriptiveComplexity.szMk L B mk x = (DescriptiveComplexity.szMkSym L B mk).formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.szSel (L : FirstOrder.Language) (B : SOBlock) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) {α : Type} (x : α) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Formula α

x belongs to the sized set, as a formula.

Equations

• DescriptiveComplexity.szSel L B i₀ h₀ x = (DescriptiveComplexity.szSelSym L B i₀ h₀).formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.szBij (L : FirstOrder.Language) (B : SOBlock) {α : Type} (x y : α) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Formula α

The bijection relates x to y, as a formula.

Equations

• DescriptiveComplexity.szBij L B x y = (DescriptiveComplexity.szBijSym L B).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.szLe (L : FirstOrder.Language) (B : SOBlock) {α : Type} (x y : α) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Formula α

x ≤ y, as a formula of the sized kernel.

Equations

• DescriptiveComplexity.szLe L B x y = (DescriptiveComplexity.szLeSym L B).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.monoBijS (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Sentence

The extra variable is the graph of a monotone bijection from the marked set onto the sized set: DescriptiveComplexity.MonoBij, as a sentence.

Equations

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

noncomputable def DescriptiveComplexity.sizedKernel (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (φ₀ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) : ((L.sum FirstOrder.Language.order).sum B.withOrder.lang).Sentence

The sized kernel: the kernel φ₀, which may read the order, and the extra variable is the monotone bijection from the marked set onto the set i₀.

Equations

• DescriptiveComplexity.sizedKernel L B mk i₀ h₀ φ₀ = (DescriptiveComplexity.sizedLHom L B).onSentence φ₀ ⊓ DescriptiveComplexity.monoBijS L B mk i₀ h₀

theorem DescriptiveComplexity.witnessCount_sizedKernel (L : FirstOrder.Language) (B : SOBlock) {A : Type} (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (φ₀ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) [instA : L.Structure A] [LinearOrder A] [Finite A] : witnessCount B.withOrder (sizedKernel L B mk i₀ h₀ φ₀) A = Nat.card { ρ₀ : B.Assignment A // A ⊨ φ₀ ∧ {a : A | ρ₀ i₀ fun (x : Fin (B.arity i₀)) => a}.ncard = {a : A | FirstOrder.Language.Structure.RelMap mk ![a]}.ncard }

The witnesses of the sized kernel are the assignments of the block satisfying the kernel whose set has exactly the size of the marked set, bijectively.

theorem DescriptiveComplexity.sharpPDefinable_of_sized_ordered {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (B : SOBlock) (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (φ₀ : ((L.sum FirstOrder.Language.order).sum B.lang).Sentence) (hC : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A], C.Count A = Nat.card { ρ₀ : B.Assignment A // A ⊨ φ₀ ∧ {a : A | ρ₀ i₀ fun (x : Fin (B.arity i₀)) => a}.ncard = {a : A | FirstOrder.Language.Structure.RelMap mk ![a]}.ncard }) : SharpPDefinable C

A count of the solutions of exactly the threshold size is #P-definable, when the property of the solution is first-order over the ordered expansion: the size is certified by the monotone bijection with the marked set, the one certificate a linear order offers. The kernel may read the order, and then has to define the same count whatever the order.

theorem DescriptiveComplexity.sharpPDefinable_of_sized {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (B : SOBlock) (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (φ₀ : (L.sum B.lang).Sentence) (hC : ∀ (A : Type) [instA : L.Structure A] [Finite A], C.Count A = Nat.card { ρ₀ : B.Assignment A // A ⊨ φ₀ ∧ {a : A | ρ₀ i₀ fun (x : Fin (B.arity i₀)) => a}.ncard = {a : A | FirstOrder.Language.Structure.RelMap mk ![a]}.ncard }) : SharpPDefinable C

A count of the solutions of exactly the threshold size is #P-definable, when the property of the solution is first-order: the case of DescriptiveComplexity.sharpPDefinable_of_sized_ordered where the kernel does not read the order.

def DescriptiveComplexity.unaryAssignEquiv (B : SOBlock) [Subsingleton B.ι] (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (A : Type) : (A → Prop) ≃ B.Assignment A

Sets, as the assignments of a block whose only variable is unary.

Equations

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

theorem DescriptiveComplexity.sharpPDefinable_of_sized_set {L : FirstOrder.Language} [L.IsRelational] (C : CountingProblem L) (B : SOBlock) [Subsingleton B.ι] (mk : L.Relations 1) (i₀ : B.ι) (h₀ : B.arity i₀ = 1) (φ₀ : (L.sum B.lang).Sentence) (P : (A : Type) → [L.Structure A] → (A → Prop) → Prop) (hφ : ∀ (A : Type) [instA : L.Structure A] (ρ₀ : B.Assignment A), A ⊨ φ₀ ↔ P A fun (a : A) => ρ₀ i₀ fun (x : Fin (B.arity i₀)) => a) (hC : ∀ (A : Type) [inst : L.Structure A] [Finite A], C.Count A = Nat.card { S : A → Prop // P A S ∧ {a : A | S a}.ncard = {a : A | FirstOrder.Language.Structure.RelMap mk ![a]}.ncard }) : SharpPDefinable C

DescriptiveComplexity.sharpPDefinable_of_sized for a block with a single variable, the solution itself: a count of the sets with a first-order property and exactly the size of the marked set is #P-definable.