The Vertex Cover → Hamilton Circuit gadget interpretation

This file defines the relativized ordered first-order interpretation DescriptiveComplexity.hamInterp that reduces VERTEX COVER (on marked graphs) to (undirected) HAMILTON CIRCUIT (on digraphs read symmetrically), the classical twelve-vertex cover-testing-gadget reduction of Karp 1972, read in the tagged framework.

The output graph hamInterp.MapRel A has these vertices (all carried by a pair of input vertices, dim = 2, cut down by a domain formula – hence a relativized interpretation, DescriptiveComplexity.RelFOInterpretation):

• gadget vertices ⟨g i, (a, b)⟩ for i : Fin 6 (tags g0 … g5), one per ordered pair (a, b) of adjacent distinct input vertices. The twelve vertices over the unordered edge {u, v} are (u, v, 0..5) (the u-side) and (v, u, 0..5) (the v-side): the side is which endpoint owns the tuple.
• selector vertices ⟨sel, (m, m)⟩, one per marked input vertex m; they form a self-looped clique and attach to the ends of every vertex's chain.
• one hub vertex ⟨hub, (min, min)⟩, present only for the degenerate input with no edges and no marks (where the output would otherwise be empty); it is a self-looped isolated vertex, so it is a one-element Hamilton circuit, which matches the (vacuous) yes-instance.

The gadget's edges force, in any Hamilton circuit, one of exactly three traversals of {u, v}: through the u-side, through the v-side, or both – never neither. So each edge is covered, and the number of vertices whose chains are traversed – the cover – is at most the number of selectors, the marked set. This file only builds the interpretation and characterizes its adjacency; the two directions of correctness are in Forward and Reverse.

@[reducible, inline]

abbrev DescriptiveComplexity.hamL : FirstOrder.Language

The ordered expansion of the marked-graph vocabulary, the source language of the reduction.

Equations

• DescriptiveComplexity.hamL = FirstOrder.Language.markedGraph.sum FirstOrder.Language.order

@[reducible, inline]

abbrev DescriptiveComplexity.hAdjSym : hamL.Relations 2

The adjacency symbol over the ordered expansion of marked graphs.

Equations

• DescriptiveComplexity.hAdjSym = Sum.inl FirstOrder.Language.mgAdj

@[reducible, inline]

abbrev DescriptiveComplexity.hMarkedSym : hamL.Relations 1

The mark symbol over the ordered expansion of marked graphs.

Equations

• DescriptiveComplexity.hMarkedSym = Sum.inl FirstOrder.Language.mgMarked

Edge and neighbor-order formulas

noncomputable def DescriptiveComplexity.adjOrF {α : Type} (s t : α) : hamL.Formula α

Symmetric adjacency: an arc in either direction.

Equations

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

noncomputable def DescriptiveComplexity.edgeF {α : Type} (s t : α) : hamL.Formula α

The two variables name an (undirected) edge: adjacent in some direction, and distinct.

Equations

• DescriptiveComplexity.edgeF s t = DescriptiveComplexity.adjOrF s t ⊓ FirstOrder.Language.BoundedFormula.not ((FirstOrder.Language.var s).equal (FirstOrder.Language.var t))

noncomputable def DescriptiveComplexity.minNbrF {α : Type} (a b : α) : hamL.Formula α

b is the least neighbor of a: it is ≤ every neighbor of a.

Equations

• DescriptiveComplexity.minNbrF a b = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.edgeF (Sum.inl a) (Sum.inr 0)).imp (DescriptiveComplexity.leF (Sum.inl b) (Sum.inr 0)))

noncomputable def DescriptiveComplexity.maxNbrF {α : Type} (a b : α) : hamL.Formula α

b is the greatest neighbor of a.

Equations

• DescriptiveComplexity.maxNbrF a b = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.edgeF (Sum.inl a) (Sum.inr 0)).imp (DescriptiveComplexity.leF (Sum.inr 0) (Sum.inl b)))

noncomputable def DescriptiveComplexity.succNbrF {α : Type} (a b c : α) : hamL.Formula α

c is the immediate neighbor-successor of b in a's neighbor list: c is a neighbor of a, b < c, and no neighbor of a lies strictly between b and c.

Equations

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

Edge predicate on the input

def DescriptiveComplexity.HEdge {A : Type} [FirstOrder.Language.markedGraph.Structure A] (a b : A) : Prop

The undirected edge relation on the input: adjacent in some direction, and distinct.

Equations

• DescriptiveComplexity.HEdge a b = ((DescriptiveComplexity.MGAdj a b ∨ DescriptiveComplexity.MGAdj b a) ∧ a ≠ b)

theorem DescriptiveComplexity.hEdge_symm {A : Type} [FirstOrder.Language.markedGraph.Structure A] {a b : A} (h : HEdge a b) : HEdge b a

Realization of the edge and neighbor formulas

@[simp]

theorem DescriptiveComplexity.realize_adjOrF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {α : Type} (v : α → A) (s t : α) : (adjOrF s t).Realize v ↔ MGAdj (v s) (v t) ∨ MGAdj (v t) (v s)

@[simp]

theorem DescriptiveComplexity.realize_edgeF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {α : Type} (v : α → A) (s t : α) : (edgeF s t).Realize v ↔ HEdge (v s) (v t)

The tags and the interpretation

inductive DescriptiveComplexity.HTag : Type

The tags of the interpreted structure. Six gadget-node indices (the side, u vs v, is encoded by which endpoint owns the carrying tuple), one selector, one degenerate-case hub. Named constructors, not Fin 8, so the tag match inside the defining formulas reduces definitionally in the characterizations.

• g0 : HTag

  Gadget node 0: the entrance of a side.

• g1 : HTag

  Gadget node 1.

• g2 : HTag

  Gadget node 2.

• g3 : HTag

  Gadget node 3.

• g4 : HTag

  Gadget node 4.

• g5 : HTag

  Gadget node 5: the exit of a side.

• sel : HTag

  A selector, one per marked vertex.

• hub : HTag

  The degenerate-case hub.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqHTag : DecidableEq HTag

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instFintypeHTag : Fintype HTag

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instInhabitedHTag : Inhabited HTag

Equations

• DescriptiveComplexity.instInhabitedHTag = { default := DescriptiveComplexity.HTag.sel }

noncomputable def DescriptiveComplexity.hEqTupF : hamL.Formula (Fin 2 × Fin 2)

Two tuples are equal, coordinatewise.

Equations

• DescriptiveComplexity.hEqTupF = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 0)) ⊓ (FirstOrder.Language.var (0, 1)).equal (FirstOrder.Language.var (1, 1))

noncomputable def DescriptiveComplexity.hSwapTupF : hamL.Formula (Fin 2 × Fin 2)

The second tuple is the first swapped.

Equations

• DescriptiveComplexity.hSwapTupF = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 1)) ⊓ (FirstOrder.Language.var (0, 1)).equal (FirstOrder.Language.var (1, 0))

noncomputable def DescriptiveComplexity.hChain50F : hamL.Formula (Fin 2 × Fin 2)

The chain edge from an exit ⟨g5, (a, b)⟩ to the next entrance ⟨g0, (a, c)⟩: same owner, and c the neighbor-successor of b.

Equations

• DescriptiveComplexity.hChain50F = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 0)) ⊓ DescriptiveComplexity.succNbrF (0, 0) (0, 1) (1, 1)

noncomputable def DescriptiveComplexity.hChain05F : hamL.Formula (Fin 2 × Fin 2)

The chain edge the other way, from ⟨g0, (a, c)⟩ to ⟨g5, (a, b)⟩.

Equations

• DescriptiveComplexity.hChain05F = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 0)) ⊓ DescriptiveComplexity.succNbrF (0, 0) (1, 1) (0, 1)

noncomputable def DescriptiveComplexity.noMarksF : hamL.Formula (Fin 2)

No vertex is marked.

Equations

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

noncomputable def DescriptiveComplexity.noEdgesF : hamL.Formula (Fin 2)

No two vertices form an edge.

Equations

• DescriptiveComplexity.noEdgesF = FirstOrder.Language.Formula.iAlls (Fin 2) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.edgeF (Sum.inr 0) (Sum.inr 1)))

noncomputable def DescriptiveComplexity.hamInterp : RelFOInterpretation hamL FirstOrder.Language.digraph HTag 2

The reduction of Vertex Cover into Hamilton Circuit: the twelve-vertex cover-testing gadget of each edge, chained along every vertex's neighbor list, with the marked vertices as selectors.

Equations

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

Realization of the degenerate-case guards

The vertices of the interpreted graph

theorem DescriptiveComplexity.dom_gadget {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) (w : Fin 2 → A) : (hamInterp.domFormula t).Realize w ↔ HEdge (w 0) (w 1)

The domain formula of a gadget tag says the tuple is an edge.

theorem DescriptiveComplexity.dom_sel {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (w : Fin 2 → A) : (hamInterp.domFormula HTag.sel).Realize w ↔ w 0 = w 1 ∧ MGMarked (w 0)

The adjacency of the interpreted graph

def DescriptiveComplexity.IAdjRaw {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (p q : HTag × (Fin 2 → A)) : Prop

The intended (symmetric) adjacency of the interpreted graph, on raw tagged tuples: the ten horizontal gadget edges, the four cross edges, the two chain edges, the selector–entrance and selector–exit edges, the selector clique and the hub self-loop. This is exactly what DescriptiveComplexity.hamInterp realizes (DescriptiveComplexity.dgArc_iff).

Equations

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

theorem DescriptiveComplexity.dgEdge_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (p q : hamInterp.MapRel A) : DGEdge p q ↔ IAdjRaw ↑p ↑q

DGArc on the interpreted graph is symmetric, so the symmetric reading DescriptiveComplexity.DGEdge used by HAMILTON CIRCUIT coincides with it.

The vertices, as named constructors

def DescriptiveComplexity.gPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) {a b : A} (h : HEdge a b) : hamInterp.MapRel A

A gadget vertex ⟨t, (a, b)⟩ for a gadget tag t over an edge (a, b).

Equations

• DescriptiveComplexity.gPt t ht h = ⟨(t, ![a, b]), ⋯⟩

def DescriptiveComplexity.selPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (h : MGMarked m) : hamInterp.MapRel A

A selector vertex, one per marked input vertex.

Equations

• DescriptiveComplexity.selPt h = ⟨(DescriptiveComplexity.HTag.sel, ![m, m]), ⋯⟩

@[simp]

theorem DescriptiveComplexity.gPt_tag {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) {a b : A} (h : HEdge a b) : (↑(gPt t ht h)).1 = t

@[simp]

theorem DescriptiveComplexity.gPt_fst {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) {a b : A} (h : HEdge a b) : (↑(gPt t ht h)).2 0 = a

@[simp]

theorem DescriptiveComplexity.gPt_snd {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) {a b : A} (h : HEdge a b) : (↑(gPt t ht h)).2 1 = b

@[simp]

theorem DescriptiveComplexity.selPt_tag {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (h : MGMarked m) : (↑(selPt h)).1 = HTag.sel

@[simp]

theorem DescriptiveComplexity.selPt_fst {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (h : MGMarked m) : (↑(selPt h)).2 0 = m