Counting the solutions of exactly the threshold size, for sets of pairs

DescriptiveComplexity.Counting.Sized one arity up. Where the objective of a threshold problem counts arcs – Feedback Arc Set – the threshold is the size of a marked binary relation, the solution is a binary relation too, and “the two have the same size” is certified by a bijection between two sets of pairs. The unique one is again the monotone one, for the lexicographic order on pairs, and the variable that guesses it is quaternary (DescriptiveComplexity.sizedPairsKernel, DescriptiveComplexity.witnessCount_sizedPairsKernel, DescriptiveComplexity.sharpPDefinable_of_sizedPairs).

def DescriptiveComplexity.SOBlock.withBij₂ (B : SOBlock) : SOBlock

The block B extended with one quaternary relation variable, the monotone bijection between two sets of pairs.

Equations

• B.withBij₂ = { ι := Unit ⊕ B.ι, ιFinite := ⋯, arity := Sum.elim (fun (x : Unit) => 4) B.arity }

def DescriptiveComplexity.SOBlock.restPart₂ (B : SOBlock) {A : Type} (ρ : B.withBij₂.Assignment A) : B.Assignment A

The assignment of the original variables underlying an assignment of the extended block.

Equations

• B.restPart₂ ρ i = ρ (Sum.inr i)

def DescriptiveComplexity.SOBlock.joinBij₂ (B : SOBlock) {A : Type} (R : (Fin 4 → A) → Prop) (ρ : B.Assignment A) : B.withBij₂.Assignment A

The assignment of the extended block determined by a quaternary relation and an assignment of the original block.

Equations

• B.joinBij₂ R ρ (Sum.inl val) = R
• B.joinBij₂ R ρ (Sum.inr i) = ρ i

def DescriptiveComplexity.sizedPairsLHom (L : FirstOrder.Language) (B : SOBlock) : L.sum B.lang →ᴸ (L.sum FirstOrder.Language.order).sum B.withBij₂.lang

The inclusion of the vocabulary of an order-free kernel into that of the sized kernel.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.sz₂MkSym (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 2) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Relations 2

The mark symbol over the vocabulary of the sized kernel.

Equations

• DescriptiveComplexity.sz₂MkSym L B mk = Sum.inl (Sum.inl mk)

@[reducible, inline]

abbrev DescriptiveComplexity.sz₂SelSym (L : FirstOrder.Language) (B : SOBlock) (i₀ : B.ι) (h₀ : B.arity i₀ = 2) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Relations 2

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

Equations

• DescriptiveComplexity.sz₂SelSym L B i₀ h₀ = Sum.inr ⟨Sum.inr i₀, h₀⟩

@[reducible, inline]

abbrev DescriptiveComplexity.sz₂BijSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Relations 4

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

Equations

• DescriptiveComplexity.sz₂BijSym L B = Sum.inr ⟨Sum.inl (), ⋯⟩

@[reducible, inline]

abbrev DescriptiveComplexity.sz₂LeSym (L : FirstOrder.Language) (B : SOBlock) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Relations 2

The order symbol over the vocabulary of the sized kernel.

Equations

• DescriptiveComplexity.sz₂LeSym L B = Sum.inl (Sum.inr FirstOrder.Language.leSymb)

def DescriptiveComplexity.szPairLeF (L : FirstOrder.Language) (B : SOBlock) {α : Type} (x y x' y' : α) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Formula α

The pair (x, y) is at most (x', y') lexicographically, as a formula.

Equations

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

def DescriptiveComplexity.szPairBijF (L : FirstOrder.Language) (B : SOBlock) {α : Type} (x y x' y' : α) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Formula α

The bijection relates (x, y) to (x', y'), as a formula.

Equations

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

noncomputable def DescriptiveComplexity.monoBij₂S (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 2) (i₀ : B.ι) (h₀ : B.arity i₀ = 2) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Sentence

The quaternary variable is the graph of a monotone bijection from the marked pairs onto the sized relation, as a sentence.

Equations

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

def DescriptiveComplexity.pairArg (B : SOBlock) {A : Type} (i₀ : B.ι) (h₀ : B.arity i₀ = 2) (a b : A) : Fin (B.arity i₀) → A

The pair (a, b), as an argument of a variable of arity two.

Equations

• DescriptiveComplexity.pairArg B i₀ h₀ a b j = ![a, b] (Fin.cast h₀ j)

theorem DescriptiveComplexity.pairArg_eta (B : SOBlock) {A : Type} (i₀ : B.ι) (h₀ : B.arity i₀ = 2) (w : Fin (B.arity i₀) → A) : pairArg B i₀ h₀ (w (Fin.cast ⋯ 0)) (w (Fin.cast ⋯ 1)) = w

noncomputable def DescriptiveComplexity.sizedPairsKernel (L : FirstOrder.Language) (B : SOBlock) (mk : L.Relations 2) (i₀ : B.ι) (h₀ : B.arity i₀ = 2) (φ₀ : (L.sum B.lang).Sentence) : ((L.sum FirstOrder.Language.order).sum B.withBij₂.lang).Sentence

The sized kernel, for pairs: the order-free kernel φ₀, and the extra variable is the monotone bijection from the marked pairs onto the relation i₀.

Equations

• DescriptiveComplexity.sizedPairsKernel L B mk i₀ h₀ φ₀ = (DescriptiveComplexity.sizedPairsLHom L B).onSentence φ₀ ⊓ DescriptiveComplexity.monoBij₂S L B mk i₀ h₀

theorem DescriptiveComplexity.witnessCount_sizedPairsKernel (L : FirstOrder.Language) (B : SOBlock) {A : Type} (mk : L.Relations 2) (i₀ : B.ι) (h₀ : B.arity i₀ = 2) (φ₀ : (L.sum B.lang).Sentence) [instA : L.Structure A] [LinearOrder A] [Finite A] : witnessCount B.withBij₂ (sizedPairsKernel L B mk i₀ h₀ φ₀) A = Nat.card { ρ₀ : B.Assignment A // A ⊨ φ₀ ∧ {p : A × A | ρ₀ i₀ (pairArg B i₀ h₀ p.1 p.2)}.ncard = {p : A × A | FirstOrder.Language.Structure.RelMap mk ![p.1, p.2]}.ncard }

The witnesses of the sized kernel for pairs are the assignments of the block satisfying the order-free kernel whose relation has exactly as many pairs as the marked relation, bijectively and whatever the linear order.

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

A count of the sets of pairs of exactly the threshold size is #P-definable, when the property of the solution is first-order: the size is certified by the monotone bijection, for the lexicographic order, with the marked relation.