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:

• DescriptiveComplexity.ncard_image_equiv and its predicate form DescriptiveComplexity.ncard_setOf_equiv: invariance of the decoded number under equivalences (this is what feeds DecisionProblem.iso_invariant proofs);
• DescriptiveComplexity.initSeg and DescriptiveComplexity.ncard_initSeg: the canonical encoding of k ≤ n as the initial segment of Fin n;
• DescriptiveComplexity.ncard_compl_eq and DescriptiveComplexity.ncard_compl_le_ncard_compl_iff: complement cardinality (n - k) and the resulting reversal of comparisons, which is what the Vertex Cover ↔ Independent Set reductions run on;
• DescriptiveComplexity.nonempty_embedding_iff_ncard_le: comparing decoded numbers is comparing sizes – the bridge to the second-order rendering of a threshold, where the injection witnessing the comparison is guessed as a relation variable (used by the Σ₁ definition of Clique);
• DescriptiveComplexity.nonempty_embedding_iff_ncard_le₂ and DescriptiveComplexity.ncard_setOf_equiv₂: the same, for a threshold carried by a marked binary relation – the arity-2 form of the representation, which is what problems counting arcs rather than vertices need;
• DescriptiveComplexity.ncard_tagged_eq_sum: cardinality under tag-disjoint union – the tagged framework's addition;
• DescriptiveComplexity.ncard_univ_pi: cardinality of a product of marked sets over the coordinates of a tuple – the tagged framework's multiplication.

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.

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.

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.

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.

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

• DescriptiveComplexity.initSeg n k = {i : Fin n | ↑i < k}

theorem DescriptiveComplexity.ncard_initSeg (n k : ℕ) (h : k ≤ n) : (initSeg n k).ncard = k

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.