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.

theorem DescriptiveComplexity.tourOn_of_blocks {H : Type} {R : H → H → Prop} [Finite H] (bs : List (List H)) (hbne : [] ∉ bs) (hflat : bs.flatten ≠ []) (nd : bs.flatten.Nodup) (hcov : ∀ (x : H), x ∈ bs.flatten) (hchain : ∀ l ∈ bs, List.IsChain R l) (hconn : List.IsChain (fun (l₁ l₂ : List H) => ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y) bs) (hwrap : ∀ x ∈ bs.flatten.getLast?, ∀ y ∈ bs.flatten.head?, R x y) : TourOn R

A cycle of blocks is a tour. A list of nonempty blocks whose flattening is duplicate-free and covers everything, where each block is a chain, consecutive blocks connect (last of one to head of the next), and the whole wraps (last of the flattening to its head), presents a tour. This packages the isChain_flatten step for the forward construction, whose blocks are a selector followed by a cover vertex's chain.

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

theorem DescriptiveComplexity.gv_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b a' b' : A} (i j : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) (hj : j ≠ HTag.sel ∧ j ≠ HTag.hub) (h : HEdge a b) (h' : HEdge a' b') : DGEdge (gPt i hi h) (gPt j hj h') ↔ IAdjRaw (i, ![a, b]) (j, ![a', b'])

Adjacency between two gadget vertices reduces to the intended adjacency of their (tag, tuple) pairs.

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

theorem DescriptiveComplexity.snakeBoth_isChain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : List.IsChain DGEdge (snakeBoth h)

theorem DescriptiveComplexity.snakeThrough_isChain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) : List.IsChain DGEdge (snakeThrough h)

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

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

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

Distinctness of gadget vertices

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

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

Which vertices a snake contains (for covering)

theorem DescriptiveComplexity.mem_snakeBoth_owner {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) : gPt i hi h ∈ snakeBoth h

Every a-side gadget vertex is in the both-sides snake.

theorem DescriptiveComplexity.mem_snakeThrough_near {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (h : HEdge a b) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) : gPt i hi h ∈ snakeThrough h

Every a-side gadget vertex is in the through snake.

theorem DescriptiveComplexity.mem_snakeThrough_far {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b : A} (hba : HEdge b a) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) (hab : HEdge a b) : gPt i hi hab ∈ snakeThrough hba

Every b-side gadget vertex – a gadget vertex owned by the far endpoint – is in the through snake. This is why an uncovered endpoint's vertices are visited by the covered endpoint's chain.

The sorted neighbour list of a vertex

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

The neighbours 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

theorem DescriptiveComplexity.mem_nbrList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a b : A} : b ∈ nbrList a ↔ HEdge a b

theorem DescriptiveComplexity.nbrList_sortedLT {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (a : A) : (nbrList a).SortedLT

The neighbour list is strictly increasing.

theorem DescriptiveComplexity.nbrList_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (a : A) : (nbrList a).Nodup

theorem DescriptiveComplexity.chain_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {a b c : A} (hb : HEdge a b) (hc : HEdge a c) (hbc : b < c) (hbtw : ∀ (d : A), HEdge a d → d ≤ b ∨ c ≤ d) : DGEdge (gv5 hb) (gv0 hc)

The gadget chain edge: the exit ⟨g5,(a,b)⟩ of one gadget is adjacent to the entrance ⟨g0,(a,c)⟩ of the next, given the neighbour-successor conditions (DescriptiveComplexity.IAdjRaw, the .g5,.g0 case). This is what glues consecutive snakes into a vertex's chain.

theorem DescriptiveComplexity.nbrList_isChain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (a : A) : List.IsChain (fun (b c : A) => ∀ (hb : HEdge a b) (hc : HEdge a c), DGEdge (gv5 hb) (gv0 hc)) (nbrList a)

The neighbour list is a connection-chain: consecutive neighbours b, c of a satisfy the gadget chain edge, so the per-neighbour snakes concatenate into a's chain.

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

Equations

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

theorem DescriptiveComplexity.chain_isChain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (C : A → Prop) (a : A) : List.IsChain DGEdge (chain C a)

A chain is a DGEdge-chain: the snakes are chains and consecutive ones connect via DescriptiveComplexity.chain_edge.

Minima and maxima of the neighbour list

theorem DescriptiveComplexity.head_nbrList_le {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (hne : nbrList a ≠ []) {d : A} (hd : HEdge a d) : (nbrList a).head hne ≤ d

The head of the neighbour list is the least neighbour.

theorem DescriptiveComplexity.le_getLast_nbrList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {a : A} (hne : nbrList a ≠ []) {d : A} (hd : HEdge a d) : d ≤ (nbrList a).getLast hne

The last of the neighbour list is the greatest neighbour.

Selector edges

theorem DescriptiveComplexity.sel_entrance_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m a b : A} (hm : MGMarked m) (h : HEdge a b) (hmin : ∀ (d : A), HEdge a d → b ≤ d) : DGEdge (selPt hm) (gv0 h)

A selector is adjacent to a chain entrance ⟨g0,(a,b)⟩ when b is the least neighbour of a.

theorem DescriptiveComplexity.exit_sel_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m a b : A} (hm : MGMarked m) (h : HEdge a b) (hmax : ∀ (d : A), HEdge a d → d ≤ b) : DGEdge (gv5 h) (selPt hm)

A selector is adjacent to a chain exit ⟨g5,(a,b)⟩ when b is the greatest neighbour of a.

theorem DescriptiveComplexity.sel_sel_edge {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m m' : A} (hm : MGMarked m) (hm' : MGMarked m') : DGEdge (selPt hm) (selPt hm')

Selectors are mutually adjacent (a self-looped clique).

Which vertices a chain contains (for covering)

theorem DescriptiveComplexity.mem_snakeOf_owner {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {a b : A} (h : HEdge a b) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) : gPt i hi h ∈ snakeOf C a b

Every a-side gadget vertex is in a's snake for b, whichever snake it is.

theorem DescriptiveComplexity.gadget_mem_chain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {a b : A} (h : HEdge a b) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) : gPt i hi h ∈ chain C a

A gadget vertex is in its owner's chain: ⟨i,(a,b)⟩ is visited by a's chain (for any cover C).

theorem DescriptiveComplexity.gadget_mem_chain_far {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {a b : A} (hab : HEdge a b) (i : HTag) (hi : i ≠ HTag.sel ∧ i ≠ HTag.hub) (hnc : ¬C a) : gPt i hi hab ∈ chain C b

A gadget vertex is in the far endpoint's chain when its owner is uncovered: if a ∉ C, the vertex ⟨i,(a,b)⟩ is visited by b's through-traversal.

The endpoints of a chain

theorem DescriptiveComplexity.chain_head? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (C : A → Prop) (a : A) (hne : nbrList a ≠ []) : ∃ (b : A) (h : HEdge a b), (∀ (d : A), HEdge a d → b ≤ d) ∧ (chain C a).head? = some (gv0 h)

A chain's first vertex is the entrance ⟨g0,(a,b)⟩ of the least-neighbour gadget – which a selector is adjacent to.

theorem DescriptiveComplexity.chain_getLast? {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (C : A → Prop) (a : A) (hne : nbrList a ≠ []) : ∃ (b : A) (h : HEdge a b), (∀ (d : A), HEdge a d → d ≤ b) ∧ (chain C a).getLast? = some (gv5 h)

A chain's last vertex is the exit ⟨g5,(a,b)⟩ of the greatest-neighbour gadget – which a selector is adjacent to.

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.chain_tuple {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w : A} {p : hamInterp.MapRel A} (hp : p ∈ chain C w) : (↑p).2 0 = w ∨ (↑p).2 1 = w ∧ ¬C ((↑p).2 0)

The owner invariant of a chain: a vertex of w's chain is either owned by w (w-side) or owned by an uncovered neighbour of w (the far side of a through-traversal).

theorem DescriptiveComplexity.chain_disjoint {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w w' : A} (hw : C w) (hw' : C w') (hne : w ≠ w') : (chain C w).Disjoint (chain C w')

Chains of distinct cover vertices are disjoint. Their only possible overlap is a far-side vertex, which requires an uncovered owner – but both cover vertices are covered.

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

theorem DescriptiveComplexity.snakeOf_disjoint {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} {w b b' : A} (hwb : HEdge w b) (hwb' : HEdge w b') (hbb : b ≠ b') : (snakeOf C w b).Disjoint (snakeOf C w b')

Snakes of distinct neighbours of w are disjoint.

theorem DescriptiveComplexity.chain_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] (C : A → Prop) (w : A) : (chain C w).Nodup

A single chain is duplicate-free: its snakes are internally nodup and pairwise disjoint (distinct neighbours ⇒ distinct gadgets).

theorem DescriptiveComplexity.chain_tag {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w : A} {p : hamInterp.MapRel A} (hp : p ∈ chain C w) : (↑p).1 ≠ HTag.sel

Chain vertices are gadget vertices, never selectors.

theorem DescriptiveComplexity.selPt_not_mem_chain {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w m : A} (hm : MGMarked m) : selPt hm ∉ chain C w

A selector is never a chain vertex.

The blocks of the cycle

theorem DescriptiveComplexity.chain_ne_nil {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w : A} (hne : nbrList w ≠ []) : chain C w ≠ []

A chain over a nonempty neighbour list is nonempty.

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_paired {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {m w : A} (hm : MGMarked m) (hne : nbrList w ≠ []) : List.IsChain DGEdge (block hm (chain C w))

Every paired block is a DGEdge-chain: the selector connects to the chain's entrance and the chain is a chain.

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

theorem DescriptiveComplexity.block_getLast_paired_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {m m' w : A} (hm : MGMarked m) (hm' : MGMarked m') (hne : nbrList w ≠ []) {x : hamInterp.MapRel A} (hx : x ∈ (block hm (chain C w)).getLast?) : DGEdge x (selPt hm')

The last vertex of a paired block (a chain exit) is adjacent to any selector.

theorem DescriptiveComplexity.block_getLast_extra_adj {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m m' : A} (hm : MGMarked m) (hm' : MGMarked m') {x : hamInterp.MapRel A} (hx : x ∈ (block hm []).getLast?) : DGEdge x (selPt hm')

The last vertex of an extra block (its selector) is adjacent to any selector.

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

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

The non-isolated cover vertices: those whose chain is nonempty.

Equations

• DescriptiveComplexity.coverList C = {w : A | C w ∧ DescriptiveComplexity.nbrList w ≠ []}.toList

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

theorem DescriptiveComplexity.mem_coverList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {w : A} : w ∈ coverList C ↔ C w ∧ nbrList w ≠ []

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

theorem DescriptiveComplexity.coverList_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} : (coverList C).Nodup

theorem DescriptiveComplexity.coverList_length_le {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) : (coverList C).length ≤ markedList.length

There are at most as many cover vertices as selectors, from the vertex-cover threshold.

The cycle and its correctness

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

The blocks of the cycle: the first |coverList| selectors each followed by their paired cover vertex's chain, then the leftover selectors alone.

Equations

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

theorem DescriptiveComplexity.block_of_mem_blockList {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {bl : List (hamInterp.MapRel A)} (hbl : bl ∈ blockList C) : (∃ (m : A) (w : A) (hm : MGMarked m), C w ∧ nbrList w ≠ [] ∧ bl = block hm (chain C w)) ∨ ∃ (m : A) (hm : MGMarked m), bl = block hm []

Every block of the list is a selector followed by a chain, or a lone selector – both nonempty and starting with a selector.

theorem DescriptiveComplexity.blockList_ne_nil_mem {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} : [] ∉ blockList C

No block is empty.

theorem DescriptiveComplexity.blockList_isChain_mem {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {bl : List (hamInterp.MapRel A)} (hbl : bl ∈ blockList C) : List.IsChain DGEdge bl

Every block is a DGEdge-chain.

theorem DescriptiveComplexity.blockList_isChain_conn {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} : List.IsChain (fun (l₁ l₂ : List (hamInterp.MapRel A)) => ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, DGEdge x y) (blockList C)

Consecutive blocks connect – in fact every pair does, since every block starts with a selector and every block's last vertex is adjacent to every selector.

theorem DescriptiveComplexity.block_disjoint {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {m1 m2 : A} (hm1 : MGMarked m1) (hm2 : MGMarked m2) {cp1 cp2 : List (hamInterp.MapRel A)} (hmm : m1 ≠ m2) (hcp : cp1.Disjoint cp2) (h1 : selPt hm1 ∉ cp2) (h2 : selPt hm2 ∉ cp1) : (block hm1 cp1).Disjoint (block hm2 cp2)

Two blocks with distinct selectors and appropriately disjoint chain parts are disjoint.

theorem DescriptiveComplexity.mem_zip_left {α β : Type} {l₁ : List α} {l₂ : List β} (hlen : l₁.length ≤ l₂.length) {x : α} (hx : x ∈ l₁) : ∃ (y : β), (x, y) ∈ l₁.zip l₂

Every element of the first list is paired by zip when it is no longer than the second.

theorem DescriptiveComplexity.mem_zip_right {α β : Type} {l₁ : List α} {l₂ : List β} (hlen : l₂.length ≤ l₁.length) {y : β} (hy : y ∈ l₂) : ∃ (x : α), (x, y) ∈ l₁.zip l₂

Every element of the second list is paired by zip when it is no longer than the first.

theorem DescriptiveComplexity.zip_pairwise_both {α β : Type} {l₁ : List α} {l₂ : List β} (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) : List.Pairwise (fun (p q : α × β) => p.1 ≠ q.1 ∧ p.2 ≠ q.2) (l₁.zip l₂)

Zipping two duplicate-free lists gives a list whose pairs differ in both components.

theorem DescriptiveComplexity.chain_sub_flatten {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) {w : A} (hw : w ∈ coverList C) : chain C w ⊆ (blockList C).flatten

Every cover vertex's chain is in the cycle: a cover vertex is paired with a selector, so its chain sits in a paired block.

theorem DescriptiveComplexity.selPt_mem_flatten {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) {m : A} (hm : MGMarked m) : selPt hm ∈ (blockList C).flatten

Every selector is in the cycle: it heads either a paired block (if among the first |coverList| selectors) or a leftover block.

theorem DescriptiveComplexity.blockList_covers {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) (hcover : ∀ (a b : A), HEdge a b → C a ∨ C b) (hmarks : ∃ (m : A), MGMarked m) (v : hamInterp.MapRel A) : v ∈ (blockList C).flatten

Covering: every vertex of the interpreted graph is in the cycle. A selector heads a block; a gadget vertex sits in a covered endpoint's chain (its owner's if covered, the neighbour's otherwise); the hub cannot occur, since there is a selector.

theorem DescriptiveComplexity.blockList_flatten_ne_nil {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) (hmarks : ∃ (m : A), MGMarked m) : (blockList C).flatten ≠ []

The cycle is nonempty when there is a selector.

theorem DescriptiveComplexity.blockList_block_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} {bl : List (hamInterp.MapRel A)} (hbl : bl ∈ blockList C) : bl.Nodup

Each block is duplicate-free.

theorem DescriptiveComplexity.blockList_pairwise_disjoint {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} : List.Pairwise List.Disjoint (blockList C)

The blocks are pairwise disjoint: distinct selectors, and distinct cover vertices give disjoint chains.

theorem DescriptiveComplexity.blockList_flatten_nodup {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} : (blockList C).flatten.Nodup

The cycle is duplicate-free.

theorem DescriptiveComplexity.blockList_wrap {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Fintype A] {C : A → Prop} (x : hamInterp.MapRel A) : x ∈ (blockList C).flatten.getLast? → ∀ y ∈ (blockList C).flatten.head?, DGEdge x y

The wrap edge: the last vertex of the cycle is adjacent to the first (a selector), since every block's last vertex is adjacent to every selector.

theorem DescriptiveComplexity.blockCycle_tourOn {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] {C : A → Prop} [Finite A] (hcard : {x : A | C x}.ncard ≤ {x : A | MGMarked x}.ncard) (hcover : ∀ (a b : A), HEdge a b → C a ∨ C b) (hmarks : ∃ (m : A), MGMarked m) : TourOn DGEdge

The non-degenerate forward direction: given a cover with at most as many vertices as the marked set, at least one marked vertex, and covering every edge, the gadget graph has a Hamilton circuit – the cycle of selectors and chains.

theorem DescriptiveComplexity.degenerate_tourOn {A : Type} [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hnm : ∀ (y : A), ¬MGMarked y) (hne : ∀ (y z : A), ¬HEdge y z) : TourOn DGEdge

The degenerate forward direction: with no marked vertices and no edges, the interpreted graph is the single self-looped hub, a one-element Hamilton circuit.