Hamilton Circuit reduces to Directed Hamilton Circuit

The undirected problem is the directed one on the symmetrized instance, so the reduction between them is a one-dimensional, single-tag interpretation that replaces each edge by its two arcs (DescriptiveComplexity.hamCircuit_fo_reduction_dirHamCircuit). It is what carries the hardness of HAMILTON CIRCUIT over to DIRECTED HAMILTON CIRCUIT, which is why the gadget work (from Vertex Cover) only has to be done once, on the undirected side.

def DescriptiveComplexity.HamRed.symInterp : FOInterpretation FirstOrder.Language.digraph FirstOrder.Language.digraph Unit 1

The interpretation of a digraph in a graph: the universe is unchanged and each edge becomes a pair of opposite arcs.

Equations

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

def DescriptiveComplexity.HamRed.sPt {A : Type} (a : A) : symInterp.Map A

The point of the interpreted structure over a.

Equations

• DescriptiveComplexity.HamRed.sPt a = ((), fun (x : Fin 1) => a)

def DescriptiveComplexity.HamRed.sEquiv {A : Type} : A ≃ symInterp.Map A

The interpreted universe is a copy of the original one.

Equations

• DescriptiveComplexity.HamRed.sEquiv = (DescriptiveComplexity.HamRed.symInterp.mapEquivSelf A).symm

@[simp]

theorem DescriptiveComplexity.HamRed.sEquiv_apply {A : Type} (a : A) : sEquiv a = sPt a

theorem DescriptiveComplexity.HamRed.sPt_surj {A : Type} (q : symInterp.Map A) : q = sPt (q.2 0)

@[simp]

theorem DescriptiveComplexity.HamRed.sArc_iff {A : Type} [FirstOrder.Language.digraph.Structure A] (a b : A) : DGArc (sPt a) (sPt b) ↔ DGEdge a b

The arcs of the interpreted structure are the edges of the original one.

theorem DescriptiveComplexity.HamRed.hasHamCircuit_iff (A : Type) [FirstOrder.Language.digraph.Structure A] : HasHamCircuit A ↔ HasDirHamCircuit (symInterp.Map A)

Correctness: a graph has a Hamilton circuit exactly when its symmetrization has a directed one.

def DescriptiveComplexity.hamCircuit_fo_reduction_dirHamCircuit : FOReduction HamCircuit DirHamCircuit

HAMILTON CIRCUIT FO-reduces to DIRECTED HAMILTON CIRCUIT: replace each edge by its two arcs, the universe unchanged.

Equations

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