A Hamilton circuit presented as a cyclic list

The forward direction of the Vertex Cover → Hamilton Circuit reduction builds its circuit as an explicit sequence of vertices – selectors interleaved with the chains of the cover vertices – so it is convenient to introduce a tour from a list: a duplicate-free list containing every vertex, along which consecutive elements are adjacent and whose last element is adjacent to its first, is a tour (DescriptiveComplexity.tourOn_of_cycleList).

theorem DescriptiveComplexity.tourOn_of_cycleList {H : Type} {R : H → H → Prop} [Finite H] (l : List H) (hne : l ≠ []) (nd : l.Nodup) (hcov : ∀ (x : H), x ∈ l) (hchain : List.IsChain R l) (hwrap : R (l.getLast hne) (l.head hne)) : TourOn R

A cyclic list is a tour. A duplicate-free list containing every element, along which consecutive elements are R-related and whose last element is R-related to its first, presents a tour of R.

The traversal of a single gadget (the snake)

@[reducible, inline]

abbrev DescriptiveComplexity.gv {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) {a b : A} (h : HEdge a b) : hamInterp.MapRel A

The gadget vertex of index i over the ordered edge (a, b) (owner a).

Equations

• DescriptiveComplexity.gv i hi h = DescriptiveComplexity.gPt i hi h

@[reducible, inline]

abbrev DescriptiveComplexity.gv0 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 0 (a side's entrance).

Equations

• DescriptiveComplexity.gv0 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g0 DescriptiveComplexity.gv0._proof_3 h

@[reducible, inline]

abbrev DescriptiveComplexity.gv1 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 1.

Equations

• DescriptiveComplexity.gv1 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g1 DescriptiveComplexity.gv1._proof_3 h

@[reducible, inline]

abbrev DescriptiveComplexity.gv2 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 2.

Equations

• DescriptiveComplexity.gv2 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g2 DescriptiveComplexity.gv2._proof_3 h

@[reducible, inline]

abbrev DescriptiveComplexity.gv3 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 3.

Equations

• DescriptiveComplexity.gv3 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g3 DescriptiveComplexity.gv3._proof_3 h

@[reducible, inline]

abbrev DescriptiveComplexity.gv4 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 4.

Equations

• DescriptiveComplexity.gv4 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g4 DescriptiveComplexity.gv4._proof_3 h

@[reducible, inline]

abbrev DescriptiveComplexity.gv5 {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : hamInterp.MapRel A

Gadget vertex 5 (a side's exit).

Equations

• DescriptiveComplexity.gv5 h = DescriptiveComplexity.gPt DescriptiveComplexity.HTag.g5 DescriptiveComplexity.gv5._proof_3 h

def DescriptiveComplexity.snakeBoth {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : List (hamInterp.MapRel A)

The traversal of gadget {a, b} when b is also in the cover: only the a-side is walked, a straight horizontal path 0-1-2-3-4-5.

Equations

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

def DescriptiveComplexity.snakeThrough {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : List (hamInterp.MapRel A)

The traversal of gadget {a, b} when b is not in the cover: the a-through path visiting all twelve vertices, dipping into the b-side.

Equations

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

@[simp]

theorem DescriptiveComplexity.snakeBoth_head? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : (snakeBoth h).head? = some (gv0 h)

@[simp]

theorem DescriptiveComplexity.snakeThrough_head? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : (snakeThrough h).head? = some (gv0 h)

@[simp]

theorem DescriptiveComplexity.snakeBoth_getLast? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : (snakeBoth h).getLast? = some (gv5 h)

@[simp]

theorem DescriptiveComplexity.snakeThrough_getLast? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : (snakeThrough h).getLast? = some (gv5 h)

Distinctness of gadget vertices

Which vertices a snake contains (for covering)

The sorted neighbor list of a vertex

noncomputable def DescriptiveComplexity.nbrList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (a : A) : List A

The neighbors of a in the input, listed in increasing order.

Equations

• DescriptiveComplexity.nbrList a = {b : A | DescriptiveComplexity.HEdge a b}.sort fun (x1 x2 : A) => x1 ≤ x2

A cover vertex's chain

noncomputable def DescriptiveComplexity.snakeOf {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] (C : A → Prop) (a b : A) : List (hamInterp.MapRel A)

The snake of gadget {a, b} in a chain of a: the a-side-only path if b is in the cover C, the through-path otherwise (empty if a, b is not an edge, which never happens on the neighbor list).

Equations

• DescriptiveComplexity.snakeOf C a b = if h : DescriptiveComplexity.HEdge a b then if C b then DescriptiveComplexity.snakeBoth h else DescriptiveComplexity.snakeThrough h else []

theorem DescriptiveComplexity.snakeOf_eq {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) : snakeOf C a b = if C b then snakeBoth h else snakeThrough h

theorem DescriptiveComplexity.snakeOf_ne_nil {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) : snakeOf C a b ≠ []

theorem DescriptiveComplexity.snakeOf_isChain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) : List.IsChain DGEdge (snakeOf C a b)

theorem DescriptiveComplexity.snakeOf_head? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) : (snakeOf C a b).head? = some (gv0 h)

theorem DescriptiveComplexity.snakeOf_getLast? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) : (snakeOf C a b).getLast? = some (gv5 h)

noncomputable def DescriptiveComplexity.chain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (C : A → Prop) (a : A) : List (hamInterp.MapRel A)

The chain of the cover vertex a: its gadgets' snakes, concatenated in neighbor order.

Equations

• DescriptiveComplexity.chain C a = List.flatMap (DescriptiveComplexity.snakeOf C a) (DescriptiveComplexity.nbrList a)

Minima and maxima of the neighbor list

Selector edges

Which vertices a chain contains (for covering)

The endpoints of a chain

Chains of distinct cover vertices are disjoint

theorem DescriptiveComplexity.snakeBoth_tuple {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) {p : hamInterp.MapRel A} (hp : p ∈ snakeBoth h) : (↑p).2 0 = a ∧ (↑p).2 1 = b

theorem DescriptiveComplexity.snakeThrough_tuple {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) {p : hamInterp.MapRel A} (hp : p ∈ snakeThrough h) : (↑p).2 0 = a ∧ (↑p).2 1 = b ∨ (↑p).2 0 = b ∧ (↑p).2 1 = a

theorem DescriptiveComplexity.snakeOf_tuple {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {w b : A} (hwb : HEdge w b) {p : hamInterp.MapRel A} (hp : p ∈ snakeOf C w b) : (↑p).2 0 = w ∧ (↑p).2 1 = b ∨ (↑p).2 0 = b ∧ (↑p).2 1 = w

The blocks of the cycle

def DescriptiveComplexity.block {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (hm : MGMarked m) (cp : List (hamInterp.MapRel A)) : List (hamInterp.MapRel A)

A block of the cycle: a selector, optionally followed by a cover vertex's chain. The cp is that chain when the selector is paired with a cover vertex, and [] for a leftover selector.

Equations

• DescriptiveComplexity.block hm cp = DescriptiveComplexity.selPt hm :: cp

theorem DescriptiveComplexity.block_ne_nil {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (hm : MGMarked m) (cp : List (hamInterp.MapRel A)) : block hm cp ≠ []

theorem DescriptiveComplexity.block_head? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (hm : MGMarked m) (cp : List (hamInterp.MapRel A)) : (block hm cp).head? = some (selPt hm)

theorem DescriptiveComplexity.block_isChain_extra {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m : A} (hm : MGMarked m) : List.IsChain DGEdge (block hm [])

The marked and cover lists

noncomputable def DescriptiveComplexity.markedList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] : List A

The marked vertices of the input: the selectors.

Equations

• DescriptiveComplexity.markedList = {m : A | DescriptiveComplexity.MGMarked m}.toList

theorem DescriptiveComplexity.mem_markedList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] {m : A} : m ∈ markedList ↔ MGMarked m

theorem DescriptiveComplexity.markedList_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [Fintype A] : markedList.Nodup

The cycle and its correctness