Graph constructions by tagged interpretations

The two-copy construction of Senellart and Gnatenko (2026), Section 3.2, https://arxiv.org/abs/2609.18261, creates a left and a right copy of every vertex and copies edges only from left to right. We verify the relation semantics, exact size, and a Boolean bipartition for every input graph. This is an interpretation example, not a hardness reduction for bipartiteness.

def Complexity.DescriptiveComplexity.GraphQuery.doubleCover : TaggedFOInterpretation Vocabulary.graph Vocabulary.graph 2 1

Two copies of the source graph, with edges only from the left copy to the right.

Equations

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

theorem Complexity.DescriptiveComplexity.GraphQuery.doubleCover_card (A : FinStruct Vocabulary.graph) : (doubleCover.apply A).card = 2 * A.card

The double cover has exactly twice as many vertices as its source.

theorem Complexity.DescriptiveComplexity.GraphQuery.doubleCover_rel (A : FinStruct Vocabulary.graph) (args : Fin 2 → Fin (2 * A.card ^ 1)) : (doubleCover.apply A).rel 0 args ↔ ((TaggedFOInterpretation.elementEquiv A.card 2 1) (args 0)).1 = 0 ∧ ((TaggedFOInterpretation.elementEquiv A.card 2 1) (args 1)).1 = 1 ∧ A.rel 0 fun (j : Fin (Vocabulary.graph.relArity 0)) => ((TaggedFOInterpretation.elementEquiv A.card 2 1) (args j)).2 0

Double-cover edges are precisely source edges with left-to-right tags.

theorem Complexity.DescriptiveComplexity.GraphQuery.doubleCover_bipartite (A : FinStruct Vocabulary.graph) : Bipartite (doubleCover.apply A)

The tag supplies a bipartition of the double cover, regardless of the source graph.