Vertex Cover reduces to Hamilton Circuit

Assembles the relativized ordered first-order reduction DescriptiveComplexity.vertexCover_rel_ordered_fo_reduction_hamCircuit out of the gadget interpretation DescriptiveComplexity.hamInterp of Gadget, from which the umbrella DescriptiveComplexity.Problems.Hamilton derives the NP-hardness of HAMILTON CIRCUIT (hence, through the existing reduction to the directed problem, of DIRECTED HAMILTON CIRCUIT).

The interpretation carries a domain formula (it is a DescriptiveComplexity.RelFOInterpretation), so it is the first reduction of the catalog targeting a spanning problem, where a yes-witness must visit every universe element. The reduction's extra obligation dom_nonempty – a definable domain can be empty on a nonempty input – is discharged here: a marked vertex yields a selector, an edge yields a gadget vertex, and the degenerate input with neither yields the hub.

The correctness of the interpretation (DescriptiveComplexity.hasSmallVertexCover_iff_hamCircuit_mapRel) splits into the two classical directions, proved in Forward and Reverse and linked here.

theorem DescriptiveComplexity.hamInterp_dom_nonempty (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ∃ (t : HTag) (w : Fin 2 → A), (hamInterp.domFormula t).Realize w

The definable domain is inhabited. A marked vertex gives a selector, an edge gives a gadget vertex, and the degenerate input with no marks and no edges gives the hub, at the minimum.

theorem DescriptiveComplexity.cover_to_tour (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hcov : CoverOn MGAdj MGMarked) : TourOn DGEdge

Forward direction: a vertex cover of size at most the marked set yields a Hamilton circuit of the gadget graph. When there is a marked vertex it is the explicit cycle of DescriptiveComplexity.blockCycle_tourOn – selectors threaded with the cover vertices' chains; otherwise (no marks, hence no edges) it is the single self-looped hub (DescriptiveComplexity.degenerate_tourOn).

theorem DescriptiveComplexity.tour_to_cover (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] (htour : TourOn DGEdge) : CoverOn MGAdj MGMarked

Reverse direction: a Hamilton circuit of the gadget graph yields a vertex cover at most as large as the marked set. The local gadget analysis forces each edge's gadget to be traversed through the u-side, the v-side or both (never neither), and the number of active chains is at most the number of selectors.

The counting injection DescriptiveComplexity.active_ncard_le bounds the active set by the marked set; the cover property DescriptiveComplexity.cover_property (the local traversal analysis) shows every edge has an active endpoint.

theorem DescriptiveComplexity.hasSmallVertexCover_iff_hamCircuit_mapRel (A : Type) [FirstOrder.Language.markedGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : HasSmallVertexCover A ↔ HasHamCircuit (hamInterp.MapRel A)

Correctness of the gadget interpretation: a marked graph has a vertex cover at most as large as its marked set iff its gadget graph has a Hamilton circuit. The finiteness of the target universe is mapRel_finite; the two directions are DescriptiveComplexity.cover_to_tour and DescriptiveComplexity.tour_to_cover.

noncomputable def DescriptiveComplexity.vertexCover_rel_ordered_fo_reduction_hamCircuit : RelOrderedFOReduction VertexCover HamCircuit

Vertex Cover relativized-ordered-FO-reduces to Hamilton Circuit: the twelve-vertex cover-testing gadget of each edge, chained along every vertex's neighbour list, with the marked vertices as selectors and a degenerate-case hub. The domain formula cuts the target universe down to the real gadget, selector and hub vertices – Immerman's definable-subset reduction, needed because HAMILTON CIRCUIT is a spanning problem.

Equations

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