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 neighbour-order formulas

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 neighbour formulas

@[simp]

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

@[simp]

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

theorem DescriptiveComplexity.realize_minNbrF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {α : Type} (v : α → A) (a b : α) : (DescriptiveComplexity.minNbrF✝ a b).Realize v ↔ ∀ (d : A), HEdge (v a) d → v b ≤ d

theorem DescriptiveComplexity.realize_maxNbrF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {α : Type} (v : α → A) (a b : α) : (DescriptiveComplexity.maxNbrF✝ a b).Realize v ↔ ∀ (d : A), HEdge (v a) d → d ≤ v b

theorem DescriptiveComplexity.realize_succNbrF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {α : Type} (v : α → A) (a b c : α) : (DescriptiveComplexity.succNbrF✝ a b c).Realize v ↔ HEdge (v a) (v c) ∧ v b < v c ∧ ∀ (d : A), HEdge (v a) d → d ≤ v b ∨ v c ≤ d

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

theorem DescriptiveComplexity.realize_noMarksF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (w : Fin 2 → A) : DescriptiveComplexity.noMarksF✝.Realize w ↔ ∀ (y : A), ¬MGMarked y

theorem DescriptiveComplexity.realize_noEdgesF {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (w : Fin 2 → A) : DescriptiveComplexity.noEdgesF✝.Realize w ↔ ∀ (y z : A), ¬HEdge y z

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)

theorem DescriptiveComplexity.dom_hub {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (w : Fin 2 → A) : (hamInterp.domFormula HTag.hub).Realize w ↔ w 0 = w 1 ∧ (∀ (a : A), w 0 ≤ a) ∧ (∀ (y : A), ¬MGMarked y) ∧ ∀ (y z : A), ¬HEdge y z

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.dgArc_iff {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (p q : hamInterp.MapRel A) : DGArc p q ↔ IAdjRaw ↑p ↑q

The adjacency of the interpreted graph: DescriptiveComplexity.hamInterp realizes exactly the intended edges DescriptiveComplexity.IAdjRaw.

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

The intended adjacency is symmetric: every gadget, chain, selector and hub edge appears in both directions.

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]), ⋯⟩

def DescriptiveComplexity.hubPt {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (hmin : ∀ (a : A), m ≤ a) (hnm : ∀ (y : A), ¬MGMarked y) (hne : ∀ (y z : A), ¬HEdge y z) : hamInterp.MapRel A

The degenerate-case hub vertex.

Equations

• DescriptiveComplexity.hubPt hmin hnm hne = ⟨(DescriptiveComplexity.HTag.hub, ![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

theorem DescriptiveComplexity.point_cases {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (p : hamInterp.MapRel A) : (∃ (t : HTag) (ht : t ≠ HTag.sel ∧ t ≠ HTag.hub) (h : HEdge ((↑p).2 0) ((↑p).2 1)), p = gPt t ht h) ∨ (∃ (h : MGMarked ((↑p).2 0)), (↑p).2 0 = (↑p).2 1 ∧ p = selPt h) ∨ (↑p).1 = HTag.hub

Every vertex of the interpreted graph is a gadget vertex, a selector, or the hub.