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