Documentation

DescriptiveComplexity.Problems.GraphIso.Gadget

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 :

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.

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.GraphGadget.instDecidableEqGTag :

DecidableEq GTag

Equations

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

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.GraphGadget.instFintypeGTag :

Equations

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

Dependency graph

instance DescriptiveComplexity.GraphGadget.instNonemptyGTag :

Dependency graph

The defining formula #

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₁ = ⊥

Instances For

Dependency graph

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.

Instances For

Dependency graph

The points #

def DescriptiveComplexity.GraphGadget.pt {G : Type} (t : GTag) (u v : 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])

Instances For

Dependency graph

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

The vertex node of a vertex.

Equations

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

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.m₁Pt {G : Type} (u : G) :

The lollipop node attached to a vertex.

Equations

DescriptiveComplexity.GraphGadget.m₁Pt u = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.m₁ u u

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.m₂Pt {G : Type} (u : G) :

One corner of a lollipop triangle.

Equations

DescriptiveComplexity.GraphGadget.m₂Pt u = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.m₂ u u

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.m₃Pt {G : Type} (u : G) :

The other corner of a lollipop triangle.

Equations

DescriptiveComplexity.GraphGadget.m₃Pt u = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.m₃ u u

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.aPt {G : Type} (u v : G) :

The subdivision node next to an arc's tail.

Equations

DescriptiveComplexity.GraphGadget.aPt u v = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.a u v

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.bPt {G : Type} (u v : G) :

The middle subdivision node of an arc.

Equations

DescriptiveComplexity.GraphGadget.bPt u v = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.b u v

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.cPt {G : Type} (u v : G) :

The subdivision node next to an arc's head.

Equations

DescriptiveComplexity.GraphGadget.cPt u v = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.c u v

Instances For

Dependency graph

def DescriptiveComplexity.GraphGadget.pPt {G : Type} (u v : G) :

The pendant marking an arc's tail.

Equations

DescriptiveComplexity.GraphGadget.pPt u v = DescriptiveComplexity.GraphGadget.pt DescriptiveComplexity.GraphGadget.GTag.p u v

Instances For

Dependency graph

theorem DescriptiveComplexity.GraphGadget.pt_eta {G : Type} (q : gadget.Map G) :

q = pt q.1 (q.2 0) (q.2 1)

Every point is a named one: one eta lemma for all eight kinds.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.pt_tag {G : Type} (t : GTag) (u v : G) :

(pt t u v).1 = t

Dependency graph

Which pairs are edges #

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

Adjacency in the input digraph.

Equations

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

Instances For

Dependency graph

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

Adjacency in the constructed graph.

Equations

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

Instances For

Dependency graph

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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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

Dependency graph

@[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'

Dependency graph

@[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

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

@[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'

Dependency graph

Which tag pairs can be joined at all #

def DescriptiveComplexity.GraphGadget.TagAdj :

GTag → GTag → Prop

The tag pairs the gadget joins: the lollipop's four edges in both directions, the arc path's four, and the pendant's one.

Equations

Instances For

Dependency graph

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

TagAdj p.1 q.1

An edge joins only the tag pairs the construction lists. The forty-six other pairs need no argument: their defining formula is ⊥, so the hypothesis is False.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.edge_irrefl_pt {G : Type} [FirstOrder.Language.graph.Structure G] (t : GTag) (u v : G) :

¬GEdge (pt t u v) (pt t u v)

No clause relates a tag to itself, so the construction has no loops.

Dependency graph

The construction is a simple graph #

theorem DescriptiveComplexity.GraphGadget.edge_symm_pt {G : Type} [FirstOrder.Language.graph.Structure G] (t s : GTag) (u v u' v' : G) :

GEdge (pt t u v) (pt s u' v') ↔ GEdge (pt s u' v') (pt t u v)

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

Dependency 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.

Dependency graph

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

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

Dependency graph

The neighbors of each kind of node #

theorem DescriptiveComplexity.GraphGadget.nbr_of_vPt {G : Type} [FirstOrder.Language.graph.Structure G] {u : G} {q : gadget.Map G} (h : GEdge (vPt u) q) :

q = m₁Pt u ∨ (∃ (v : G), GAdj u v ∧ q = aPt u v) ∨ ∃ (w : G), GAdj w u ∧ q = cPt w u

The neighbors of a vertex node: its lollipop, the tail-side subdivision of each arc out of it, and the head-side subdivision of each arc into it.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.nbr_of_m₁Pt {G : Type} [FirstOrder.Language.graph.Structure G] {u : G} {q : gadget.Map G} (h : GEdge (m₁Pt u) q) :

q = vPt u ∨ q = m₂Pt u ∨ q = m₃Pt u

Dependency graph

theorem DescriptiveComplexity.GraphGadget.nbr_of_aPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} {q : gadget.Map G} (h : GEdge (aPt u v) q) :

q = vPt u ∨ q = bPt u v ∨ q = pPt u v

Dependency graph

theorem DescriptiveComplexity.GraphGadget.nbr_of_bPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} {q : gadget.Map G} (h : GEdge (bPt u v) q) :

q = aPt u v ∨ q = cPt u v

Dependency graph

theorem DescriptiveComplexity.GraphGadget.nbr_of_cPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} {q : gadget.Map G} (h : GEdge (cPt u v) q) :

q = bPt u v ∨ q = vPt v

Dependency graph

theorem DescriptiveComplexity.GraphGadget.nbr_of_pPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} {q : gadget.Map G} (h : GEdge (pPt u v) q) :

q = aPt u v

Dependency graph

The structural predicates that recover the levels #

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

Lying on a triangle.

Equations

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

Instances For

Dependency graph

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

Being adjacent to a node that lies on a triangle.

Equations

DescriptiveComplexity.GraphGadget.AdjTri p = ∃ (q : DescriptiveComplexity.GraphGadget.gadget.Map G), DescriptiveComplexity.GraphGadget.GEdge p q ∧ DescriptiveComplexity.GraphGadget.OnTri q

Instances For

Dependency graph

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

Having exactly one neighbor.

Equations

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

Instances For

Dependency graph

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

Having a neighbor with exactly one neighbor.

Equations

DescriptiveComplexity.GraphGadget.HasLeafNbr p = ∃ (q : DescriptiveComplexity.GraphGadget.gadget.Map G), DescriptiveComplexity.GraphGadget.GEdge p q ∧ DescriptiveComplexity.GraphGadget.Leaf q

Instances For

Dependency graph

theorem DescriptiveComplexity.GraphGadget.onTri_m₁Pt {G : Type} [FirstOrder.Language.graph.Structure G] (u : G) :

OnTri (m₁Pt u)

The lollipop triangle is a triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_onTri_vPt {G : Type} [FirstOrder.Language.graph.Structure G] (u : G) :

¬OnTri (vPt u)

A vertex node lies on no triangle: no two of its neighbors are joined.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_onTri_aPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬OnTri (aPt u v)

A tail-side subdivision node lies on no triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_onTri_bPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬OnTri (bPt u v)

A middle subdivision node lies on no triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_onTri_cPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬OnTri (cPt u v)

A head-side subdivision node lies on no triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_onTri_pPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬OnTri (pPt u v)

A pendant lies on no triangle.

Dependency graph

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.

theorem DescriptiveComplexity.GraphGadget.isolated_vtx {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬u = v) (q : gadget.Map G) :

¬GEdge (pt GTag.vtx u v) q

A vtx node off the diagonal is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_m₁ {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬u = v) (q : gadget.Map G) :

¬GEdge (pt GTag.m₁ u v) q

A m₁ node off the diagonal is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_m₂ {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬u = v) (q : gadget.Map G) :

¬GEdge (pt GTag.m₂ u v) q

A m₂ node off the diagonal is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_m₃ {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬u = v) (q : gadget.Map G) :

¬GEdge (pt GTag.m₃ u v) q

A m₃ node off the diagonal is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_a {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬GAdj u v) (q : gadget.Map G) :

¬GEdge (pt GTag.a u v) q

An a node on a pair that is not an arc is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_b {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬GAdj u v) (q : gadget.Map G) :

¬GEdge (pt GTag.b u v) q

An b node on a pair that is not an arc is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_c {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬GAdj u v) (q : gadget.Map G) :

¬GEdge (pt GTag.c u v) q

An c node on a pair that is not an arc is isolated.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.isolated_p {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : ¬GAdj u v) (q : gadget.Map G) :

¬GEdge (pt GTag.p u v) q

An p node on a pair that is not an arc is isolated.

Dependency graph

Adjacency to a triangle: the vertices #

theorem DescriptiveComplexity.GraphGadget.adjTri_vPt {G : Type} [FirstOrder.Language.graph.Structure G] (u : G) :

A vertex node is adjacent to its lollipop.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_adjTri_aPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬AdjTri (aPt u v)

No subdivision node is adjacent to a triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_adjTri_bPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬AdjTri (bPt u v)

No subdivision node is adjacent to a triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_adjTri_cPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬AdjTri (cPt u v)

No subdivision node is adjacent to a triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_adjTri_pPt {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

¬AdjTri (pPt u v)

No subdivision node is adjacent to a triangle.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.onTri_m₂Pt {G : Type} [FirstOrder.Language.graph.Structure G] (u : G) :

OnTri (m₂Pt u)

The other two corners of a lollipop lie on its triangle too.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.onTri_m₃Pt {G : Type} [FirstOrder.Language.graph.Structure G] (u : G) :

OnTri (m₃Pt u)

The other two corners of a lollipop lie on its triangle too.

Dependency graph

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

¬OnTri p ∧ AdjTri p ↔ ∃ (u : G), p = vPt u

The vertices are recoverable from adjacency alone: they are the nodes adjacent to a triangle without lying on one. Junk points fail the test by being isolated, lollipop nodes by lying on their triangle, and subdivision nodes and pendants by touching no triangle.

Dependency graph

Leaves: the pendant marks the tail #

theorem DescriptiveComplexity.GraphGadget.leaf_pPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : GAdj u v) :

Leaf (pPt u v)

The pendant of an arc is a leaf.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_leaf_bPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : GAdj u v) :

¬Leaf (bPt u v)

A middle subdivision node is not a leaf: it has both an a and a c neighbor, and those have different tags.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_leaf_vPt_of_out {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : GAdj u v) :

A vertex node incident to an arc is not a leaf: it has its lollipop and the arc's subdivision node.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_leaf_vPt_of_in {G : Type} [FirstOrder.Language.graph.Structure G] {w u : G} (h : GAdj w u) :

A vertex node incident to an arc is not a leaf: it has its lollipop and the arc's subdivision node.

Dependency graph

Which nodes have a leaf neighbor: the tail side #

theorem DescriptiveComplexity.GraphGadget.hasLeafNbr_aPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : GAdj u v) :

HasLeafNbr (aPt u v)

The tail-side subdivision node has the pendant as a neighbor.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.not_hasLeafNbr_cPt {G : Type} [FirstOrder.Language.graph.Structure G] {u v : G} (h : GAdj u v) :

¬HasLeafNbr (cPt u v)

The head-side subdivision node has none: its neighbors are the middle node and the head, and the head is incident to this very arc.

Dependency graph

The arcs are recoverable #

theorem DescriptiveComplexity.GraphGadget.arc_iff {G : Type} [FirstOrder.Language.graph.Structure G] (u v : G) :

GAdj u v ↔ ∃ (p : gadget.Map G) (q : gadget.Map G) (r : gadget.Map G), GEdge (vPt u) p ∧ ¬OnTri p ∧ ¬AdjTri p ∧ HasLeafNbr p ∧ GEdge p q ∧ ¬OnTri q ∧ ¬AdjTri q ∧ ¬Leaf q ∧ GEdge q r ∧ ¬OnTri r ∧ ¬HasLeafNbr r ∧ GEdge r (vPt v)

An arc of the input is a guarded path of length four between the two vertex nodes. Each guard rules out a concrete impostor: without ¬OnTri the lollipop of an isolated vertex closes the chain, without ¬AdjTri it turns back through the vertex node, without ¬Leaf it goes out to the pendant and back, and without ¬HasLeafNbr it returns along the tail-side node – each of which would claim an arc from a vertex to itself. The direction of the arc is carried by HasLeafNbr: only the tail side has a pendant.

Dependency graph

An isomorphism of the constructions is one of the inputs #

theorem DescriptiveComplexity.GraphGadget.edge_map {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p q : gadget.Map G) :

GEdge (φ p) (φ q) ↔ GEdge p q

An isomorphism preserves and reflects the constructed adjacency.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.edge_map_symm {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p q : gadget.Map H) :

GEdge (φ.symm p) (φ.symm q) ↔ GEdge p q

Dependency graph

theorem DescriptiveComplexity.GraphGadget.onTri_map {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p : gadget.Map G) :

OnTri (φ p) ↔ OnTri p

Lying on a triangle is preserved.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.adjTri_map {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p : gadget.Map G) :

AdjTri (φ p) ↔ AdjTri p

Adjacency to a triangle is preserved.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.leaf_map {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p : gadget.Map G) :

Leaf (φ p) ↔ Leaf p

Being a leaf is preserved: the uniqueness clause transfers because every neighbor of the image is the image of a neighbor.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.hasLeafNbr_map {G H : Type} [FirstOrder.Language.graph.Structure G] [FirstOrder.Language.graph.Structure H] (φ : FirstOrder.Language.graph.Equiv (gadget.Map G) (gadget.Map H)) (p : gadget.Map G) :

HasLeafNbr (φ p) ↔ HasLeafNbr p

Having a leaf neighbor is preserved.

Dependency graph

theorem DescriptiveComplexity.GraphGadget.vPt_injective {G : Type} :

Function.Injective vPt

Dependency graph

theorem DescriptiveComplexity.GraphGadget.gadget_isoReflecting :

IsoReflecting gadget

The gadget reflects isomorphism: an isomorphism of the constructed graphs restricts to the vertex nodes, and the arcs are read off it by DescriptiveComplexity.GraphGadget.arc_iff. Together with functoriality – free for an interpretation – this says the construction is faithful.

Dependency graph