Documentation

DescriptiveComplexity.Numbers.Unary

Unary representation of numbers in finite structures #

The unary encoding: a number carried by an instance is the cardinality of a marked set – Set.ncard is the decoding function, and no order is needed. This file provides the shared lemma kit so that problem files do not hand-roll cardinality reasoning:

Unary representation keeps numbers polynomial in the instance size; problems whose numbers must be exponential (SubsetSum and friends) use the binary representation of DescriptiveComplexity.Numbers.Binary instead.

source
theorem DescriptiveComplexity.ncard_image_equiv {A B : Type} (e : A ≃ B) (s : Set A) :
(⇑e '' s).ncard = s.ncard

The decoded number is invariant under equivalences of the universe.

source
theorem DescriptiveComplexity.ncard_setOf_equiv {A B : Type} (u : B ≃ A) {KB : B → Prop} {KA : A → Prop} (hK : ∀ (b : B), KB b ↔ KA (u b)) :
{b : B | KB b}.ncard = {a : A | KA a}.ncard

The number encoded by a marked set is invariant under an equivalence of universes carrying one mark predicate to the other. This is the form the transport of a threshold along an isomorphism (or along the equivalence underlying a one-dimensional interpretation) takes in practice.

source
theorem DescriptiveComplexity.ncard_setOf_symm {A B : Type} (u : B ≃ A) (S : B → Prop) :
{b : B | S b}.ncard = {a : A | S (u.symm a)}.ncard

Pulling a mark predicate back along u.symm does not change the number it encodes: the special case of DescriptiveComplexity.ncard_setOf_equiv where the predicate on the target universe is the transported one.

source
def DescriptiveComplexity.initSeg (n k : ℕ) :
Set (Fin n)

The canonical unary encoding of k in a universe of size n: the initial segment of Fin n of length k.

Equations
Instances For
    source
    theorem DescriptiveComplexity.ncard_initSeg (n k : ℕ) (h : k ≤ n) :
    (initSeg n k).ncard = k

    The initial segment of length k ≤ n indeed encodes k.

    source
    theorem DescriptiveComplexity.ncard_le_card {A : Type} [Finite A] (s : Set A) :
    s.ncard ≤ Nat.card A

    A decoded number never exceeds the size of the universe.

    source
    theorem DescriptiveComplexity.ncard_compl_eq {A : Type} [Finite A] (s : Set A) :
    sᶜ.ncard = Nat.card A - s.ncard

    Complement cardinality: the marked complement encodes n - k.

    source
    theorem DescriptiveComplexity.ncard_compl_le_ncard_compl_iff {A : Type} [Finite A] (s t : Set A) :
    sᶜ.ncard ≤ tᶜ.ncard ↔ t.ncard ≤ s.ncard

    Complementation reverses the comparison of decoded numbers – the subtraction n - k is monotone decreasing in k. This is the arithmetic content of the Vertex Cover ↔ Independent Set reductions.

    source
    theorem DescriptiveComplexity.ncard_compl_le_iff {A : Type} [Finite A] (s t : Set A) :
    sᶜ.ncard ≤ t.ncard ↔ tᶜ.ncard ≤ s.ncard

    Comparing a complement with a set, the two sides swap under complementation: n - k ≤ l iff n - l ≤ k.

    source
    theorem DescriptiveComplexity.nonempty_embedding_iff_ncard_le {A : Type} [Finite A] (P Q : A → Prop) :
    Nonempty ({ x : A // P x } ↪ { x : A // Q x }) ↔ {x : A | P x}.ncard ≤ {x : A | Q x}.ncard

    Comparing decoded numbers is comparing sizes: on a finite universe the number encoded by the marked set P is at most the one encoded by Q exactly when the P-elements inject into the Q-elements. This is the bridge between the cardinality reading of a threshold and its second-order rendering, where the injection is guessed as a binary relation variable.

    source
    theorem DescriptiveComplexity.nonempty_embedding_iff_ncard_le' {α β : Type} [Finite α] [Finite β] (P : α → Prop) (Q : β → Prop) :
    Nonempty ({ x : α // P x } ↪ { y : β // Q y }) ↔ {x : α | P x}.ncard ≤ {y : β | Q y}.ncard

    Comparing decoded numbers across universes: the same bridge as DescriptiveComplexity.nonempty_embedding_iff_ncard_le, when the two marked sets live on different types. This is what a threshold comparing a count of pairs with a count of elements needs.

    Thresholds on pairs #

    Problems whose objective counts arcs rather than vertices – Feedback Arc Set, Max Cut – need a threshold that can reach n², which a marked subset of the universe cannot. The same unary idea one arity up does reach it: the number is the cardinality of a marked binary relation, decoded as the Set.ncard of the corresponding set of pairs. It stays order-free and isomorphism-invariant, and the whole kit above applies at the type A × A; the two lemmas below are just its curried form.

    source
    theorem DescriptiveComplexity.nonempty_embedding_iff_ncard_le₂ {A : Type} [Finite A] (P Q : A → A → Prop) :
    Nonempty ({ p : A × A // P p.1 p.2 } ↪ { p : A × A // Q p.1 p.2 }) ↔ {p : A × A | P p.1 p.2}.ncard ≤ {p : A × A | Q p.1 p.2}.ncard

    Comparing decoded numbers is comparing sizes, for thresholds carried by a binary relation.

    source
    theorem DescriptiveComplexity.ncard_setOf_equiv₂ {A B : Type} (u : B ≃ A) {RB : B → B → Prop} {RA : A → A → Prop} (hR : ∀ (b b' : B), RB b b' ↔ RA (u b) (u b')) :
    {p : B × B | RB p.1 p.2}.ncard = {p : A × A | RA p.1 p.2}.ncard

    The number encoded by a marked binary relation is invariant under an equivalence of universes carrying one relation to the other.

    source
    theorem DescriptiveComplexity.ncard_tagged_eq_sum {T A : Type} [Fintype T] [Finite A] (s : T → Set A) :
    {p : T × A | p.2 ∈ s p.1}.ncard = ∑ t : T, (s t).ncard

    Cardinality under tag-disjoint union: on a universe of tagged elements, the cardinalities of the per-tag marked sets add up. This is how the tagged framework represents addition.

    source
    theorem DescriptiveComplexity.ncard_univ_pi {ι A : Type} [Fintype ι] [Finite A] (s : ι → Set A) :
    (Set.univ.pi s).ncard = ∏ i : ι, (s i).ncard

    Cardinality of a product of marked sets over tuple coordinates: the cardinalities multiply. This is how the tagged framework represents multiplication.