Disjoint graph copies as a tagged reduction

Taking a positive number of disjoint copies preserves and reflects bipartiteness. The forward coloring ignores the tag; the reverse coloring restricts to one copy. This supplies a reduction with a genuinely larger universe and tests the tagged interface against an independently defined graph property. It is not a hardness result.

def Complexity.DescriptiveComplexity.GraphQuery.disjointCopies (copies : ℕ) (hcopies : 0 < copies) : TaggedFOInterpretation Vocabulary.graph Vocabulary.graph copies 1

A fixed positive number of disjoint copies of the source graph.

Equations

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

theorem Complexity.DescriptiveComplexity.GraphQuery.disjointCopies_edge (copies : ℕ) (hcopies : 0 < copies) (A : FinStruct Vocabulary.graph) (x y : Fin (copies * A.card ^ 1)) : Edge ((disjointCopies copies hcopies).apply A) x y ↔ ((TaggedFOInterpretation.elementEquiv A.card copies 1) x).1 = ((TaggedFOInterpretation.elementEquiv A.card copies 1) y).1 ∧ Edge A (((TaggedFOInterpretation.elementEquiv A.card copies 1) x).2 0) (((TaggedFOInterpretation.elementEquiv A.card copies 1) y).2 0)

Edges stay within one copy and agree there with the source graph.

theorem Complexity.DescriptiveComplexity.GraphQuery.disjointCopies_bipartite (copies : ℕ) (hcopies : 0 < copies) (A : FinStruct Vocabulary.graph) : Bipartite ((disjointCopies copies hcopies).apply A) ↔ Bipartite A

A positive disjoint union of copies is bipartite exactly when the source is.

def Complexity.DescriptiveComplexity.GraphQuery.bipartiteProblem : DecisionProblem Vocabulary.graph

Bipartiteness as an invariant decision problem.

Equations

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

def Complexity.DescriptiveComplexity.GraphQuery.disjointCopiesReduction (copies : ℕ) (hcopies : 0 < copies) : TaggedFOReduction bipartiteProblem bipartiteProblem

Disjoint copies give a first-order reduction of bipartiteness to itself.

Equations

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