The digraph-to-graph gadget

The construction turning a directed graph into a simple one with the same isomorphisms. It is written on a single structure – the doubling that runs it on both sides of an instance is DescriptiveComplexity.GadgetDouble – so everything below speaks about one graph.

Each vertex u gets

• a vertex node V u, and
• a lollipop: M₁ u adjacent to V u, with M₁ u, M₂ u, M₃ u a triangle.

Each arc u ⟶ v gets a path of three subdivision nodes,

  V u — A u v — B u v — C u v — V v

together with a pendant P u v hanging off A u v.

Two design points, both forced:

• Three subdivision nodes, not two. The source is an arbitrary binary relation, so a self-loop u ⟶ u is a legal instance; with two subdivisions it would close a triangle and wreck the triangle test below, with three it closes a 4-cycle.
• The lollipop. Without it, a vertex incident to exactly one arc has degree one, and is interchangeable with the pendant of that arc – the swap is an automorphism, and vertices could not be recovered. With it, every vertex node is adjacent to a triangle and no other node is.

The levels are then recovered from adjacency alone, with no counting beyond “has exactly one neighbor”: the triangle nodes are those lying on a triangle, the vertices those adjacent to one without lying on one, A the nodes with a leaf neighbor, and so on. Points of the tagged power that no clause makes adjacent to anything – an arc node for a pair that is not an arc – are isolated, hence harmless: an isomorphism matches them by degree.

The nodes

inductive DescriptiveComplexity.GraphGadget.GTag : Type

The eight kinds of node: a vertex, its three lollipop nodes, the three subdivision nodes of an arc, and the pendant marking the arc's tail.

• vtx : GTag

  The copy of a vertex.

• m₁ : GTag

  The lollipop node attached to a vertex.

• m₂ : GTag

  One corner of the lollipop triangle.

• m₃ : GTag

  The other corner of the lollipop triangle.

• a : GTag

  The subdivision node next to an arc's tail.

• b : GTag

  The middle subdivision node of an arc.

• c : GTag

  The subdivision node next to an arc's head.

• p : GTag

  The pendant marking an arc's tail.

@[instance_reducible]

instance DescriptiveComplexity.GraphGadget.instDecidableEqGTag : DecidableEq GTag

Equations

• DescriptiveComplexity.GraphGadget.instDecidableEqGTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.GraphGadget.instFintypeGTag : Fintype GTag

Equations

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

instance DescriptiveComplexity.GraphGadget.instNonemptyGTag : Nonempty GTag

The defining formula

def DescriptiveComplexity.GraphGadget.diagF {α : Type} (x₀ x₁ : α) : FirstOrder.Language.graph.Formula α

The two coordinates are equal: the point is a vertex-side node, which is indexed by the diagonal.

Equations

• DescriptiveComplexity.GraphGadget.diagF x₀ x₁ = (FirstOrder.Language.var x₀).equal (FirstOrder.Language.var x₁)

def DescriptiveComplexity.GraphGadget.arcF {α : Type} (x₀ x₁ : α) : FirstOrder.Language.graph.Formula α

The two coordinates form an arc: the point is an arc-side node.

Equations

• DescriptiveComplexity.GraphGadget.arcF x₀ x₁ = FirstOrder.Language.adj.formula₂ (FirstOrder.Language.var x₀) (FirstOrder.Language.var x₁)

def DescriptiveComplexity.GraphGadget.sameVtxF {α : Type} (x₀ y₀ : α) : FirstOrder.Language.graph.Formula α

The two points carry the same vertex.

Equations

• DescriptiveComplexity.GraphGadget.sameVtxF x₀ y₀ = (FirstOrder.Language.var x₀).equal (FirstOrder.Language.var y₀)

def DescriptiveComplexity.GraphGadget.sameArcF {α : Type} (x₀ x₁ y₀ y₁ : α) : FirstOrder.Language.graph.Formula α

The two points carry the same arc.

Equations

• DescriptiveComplexity.GraphGadget.sameArcF x₀ x₁ y₀ y₁ = (FirstOrder.Language.var x₀).equal (FirstOrder.Language.var y₀) ⊓ (FirstOrder.Language.var x₁).equal (FirstOrder.Language.var y₁)

def DescriptiveComplexity.GraphGadget.edgeF {α : Type} (t s : GTag) (x₀ x₁ y₀ y₁ : α) : FirstOrder.Language.graph.Formula α

The edges of the gadget, tag pair by tag pair. Every clause is stated in both directions, so the result is symmetric; no clause relates a tag to itself on the same point, so it is irreflexive.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.GraphGadget.edgeF t s x₀ x₁ y₀ y₁ = ⊥

def DescriptiveComplexity.GraphGadget.gadget : FOInterpretation FirstOrder.Language.graph FirstOrder.Language.graph GTag 2

The gadget: a directed graph becomes a simple graph with the same isomorphisms. Eight tags, dimension two.

Equations

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

The points

def DescriptiveComplexity.GraphGadget.pt {G : Type} (t : GTag) (u v : G) : gadget.Map G

A point of the construction: a tag and two coordinates. The vertex-side kinds are the diagonal ones.

Equations

• DescriptiveComplexity.GraphGadget.pt t u v = (t, ![u, v])

def DescriptiveComplexity.GraphGadget.vPt {G : Type} (u : G) : gadget.Map G

The vertex node of a vertex.

Equations

• DescriptiveComplexity.GraphGadget.vPt u = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.vtx u u

Which pairs are edges

def DescriptiveComplexity.GraphGadget.GAdj {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) : Prop

Adjacency in the input digraph.

Equations

• DescriptiveComplexity.GraphGadget.GAdj u v = FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![u, v]

def DescriptiveComplexity.GraphGadget.GEdge {G : Type} [FirstOrder.Language.graph.Structure G] (p q : gadget.Map G) : Prop

Adjacency in the constructed graph.

Equations

• DescriptiveComplexity.GraphGadget.GEdge p q = FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![p, q]

Every clause of DescriptiveComplexity.GraphGadget.edgeF, read on general points. The coordinates of a neighbor are not known to be diagonal before the clause is read, so these are the forms the case analysis needs; the diagonal corollaries follow.

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_vtx_m₁ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.vtx u v) (pt GTag.m₁ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₁_vtx {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₁ u v) (pt GTag.vtx u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₁_m₂ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₁ u v) (pt GTag.m₂ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₂_m₁ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₂ u v) (pt GTag.m₁ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₁_m₃ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₁ u v) (pt GTag.m₃ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₃_m₁ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₃ u v) (pt GTag.m₁ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₂_m₃ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₂ u v) (pt GTag.m₃ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_m₃_m₂ {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.m₃ u v) (pt GTag.m₂ u' v') ↔ u = v ∧ u' = v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_vtx_a {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.vtx u v) (pt GTag.a u' v') ↔ u = v ∧ GAdj u' v' ∧ u = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_a_vtx {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.a u v) (pt GTag.vtx u' v') ↔ GAdj u v ∧ u' = v' ∧ u' = u

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_c_vtx {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.c u v) (pt GTag.vtx u' v') ↔ GAdj u v ∧ u' = v' ∧ v = u'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_vtx_c {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.vtx u v) (pt GTag.c u' v') ↔ u = v ∧ GAdj u' v' ∧ v' = u

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_a_b {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.a u v) (pt GTag.b u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_b_a {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.b u v) (pt GTag.a u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_b_c {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.b u v) (pt GTag.c u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_c_b {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.c u v) (pt GTag.b u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_a_p {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.a u v) (pt GTag.p u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

@[simp]

theorem DescriptiveComplexity.GraphGadget.edge_p_a {G : Type} [FirstOrder.Language.graph.Structure G] (u v u' v' : G) : GEdge (pt GTag.p u v) (pt GTag.a u' v') ↔ GAdj u v ∧ GAdj u' v' ∧ u = u' ∧ v = v'

Which tag pairs can be joined at all

The construction is a simple graph

theorem DescriptiveComplexity.GraphGadget.edge_symm {G : Type} [FirstOrder.Language.graph.Structure G] (p q : gadget.Map G) : GEdge p q ↔ GEdge q p

Symmetric: every clause of DescriptiveComplexity.GraphGadget.edgeF is stated in both directions, so the constructed relation is undirected.

theorem DescriptiveComplexity.GraphGadget.edge_irrefl {G : Type} [FirstOrder.Language.graph.Structure G] (p : gadget.Map G) : ¬GEdge p p

Irreflexive: no clause relates a tag to itself, so the constructed graph has no loops.

The neighbors of each kind of node

The structural predicates that recover the levels

Junk points are isolated

A point whose coordinates do not fit its tag – a lollipop node off the diagonal, a subdivision node on a pair that is not an arc – is joined to nothing, so an isomorphism can only match it with another such point. This is what lets the recovery below case over all points rather than only the well-formed ones.

Adjacency to a triangle: the vertices

Leaves: the pendant marks the tail

Which nodes have a leaf neighbor: the tail side

The arcs are recoverable

An isomorphism of the constructions is one of the inputs

theorem DescriptiveComplexity.GraphGadget.vPt_injective {G : Type} : Function.Injective vPt