#Hamilton Circuit is parsimoniously #P-complete

DescriptiveComplexity.sharpHamCircuit_sharpP_parsimoniousComplete, by a reduction from the directed problem (DescriptiveComplexity.sharpDirHamCircuit_parsimonious_sharpHamCircuit), order-free and without a domain formula.

The reduction of the library in the other direction, doubling each edge, is not parsimonious for edge sets: an undirected circuit becomes its two orientations. The classical reduction in this direction is. Each vertex x is split into a path (i, x) – (m, x) – (o, x), and an arc x → y becomes the edge (o, x) – (i, y) (DescriptiveComplexity.Split.SArc).

The middle vertex has its two path neighbours and nothing else, so a circuit passes through it, in one direction or the other. Entering a vertex by i and leaving it by o forces the same at the next vertex – were it entered by o, its i would be reached twice – and so, by induction along the circuit (DescriptiveComplexity.IsCircuit.induction), at every vertex (DescriptiveComplexity.Split.forward_all). An undirected circuit of the split graph thus has an orientation in which every vertex is traversed i, m, o, and that orientation is a directed circuit of the graph, read on the edges (o, x) – (i, y). Directed circuits and edge sets correspond bijectively (DescriptiveComplexity.Split.splitEquiv).

Both directions of the correspondence build a circuit from a potential (DescriptiveComplexity.isCircuit_of_potential): the position of the vertex in the other circuit.

inductive DescriptiveComplexity.Split.T3 : Type

The three copies of a vertex.

• i : T3

  The entry copy.

• m : T3

  The middle copy.

• o : T3

  The exit copy.

@[instance_reducible]

instance DescriptiveComplexity.Split.instDecidableEqT3 : DecidableEq T3

Equations

• DescriptiveComplexity.Split.instDecidableEqT3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.Split.instFintypeT3 : Fintype T3

Equations

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

instance DescriptiveComplexity.Split.instNonemptyT3 : Nonempty T3

def DescriptiveComplexity.Split.SArc {A : Type} (R : A → A → Prop) : T3 × A → T3 × A → Prop

The arcs of the split graph of a relation: the path of each vertex, and one arc from exit to entry per arc of the relation.

Equations

• DescriptiveComplexity.Split.SArc R (DescriptiveComplexity.Split.T3.i, x_2) (DescriptiveComplexity.Split.T3.m, y) = (x_2 = y)
• DescriptiveComplexity.Split.SArc R (DescriptiveComplexity.Split.T3.m, x_2) (DescriptiveComplexity.Split.T3.o, y) = (x_2 = y)
• DescriptiveComplexity.Split.SArc R (DescriptiveComplexity.Split.T3.o, x_2) (DescriptiveComplexity.Split.T3.i, y) = R x_2 y
• DescriptiveComplexity.Split.SArc R x✝¹ x✝ = False

def DescriptiveComplexity.Split.SEdge {A : Type} (R : A → A → Prop) (p q : T3 × A) : Prop

The edges of the split graph.

Equations

• DescriptiveComplexity.Split.SEdge R p q = (DescriptiveComplexity.Split.SArc R p q ∨ DescriptiveComplexity.Split.SArc R q p)

theorem DescriptiveComplexity.Split.sedge_symm {A : Type} {R : A → A → Prop} {p q : T3 × A} (h : SEdge R p q) : SEdge R q p

From a directed circuit to a circuit of the split graph

theorem DescriptiveComplexity.Split.isCircuit_sarc {A : Type} [Finite A] [Nonempty A] {R Nxt : A → A → Prop} (h : IsCircuit R Nxt) : IsCircuit (SEdge R) (SArc Nxt)

A directed circuit, split, is a circuit of the split graph.

From a circuit of the split graph to a directed circuit

theorem DescriptiveComplexity.Split.through_m {A : Type} [Finite A] {R : A → A → Prop} {N : T3 × A → T3 × A → Prop} (hN : IsCircuit (SEdge R) N) (x : A) : N (T3.i, x) (T3.m, x) ∧ N (T3.m, x) (T3.o, x) ∨ N (T3.o, x) (T3.m, x) ∧ N (T3.m, x) (T3.i, x)

The circuit passes through the middle copy of a vertex, one way or the other.

theorem DescriptiveComplexity.Split.forward_all {A : Type} [Finite A] {R : A → A → Prop} {N : T3 × A → T3 × A → Prop} (hN : IsCircuit (SEdge R) N) {x₀ : A} (h₀ : N (T3.i, x₀) (T3.m, x₀)) (x : A) : N (T3.i, x) (T3.m, x)

If one vertex is traversed forward, all are.

theorem DescriptiveComplexity.Split.exists_circuit_of_forward {A : Type} [Finite A] {R : A → A → Prop} {N : T3 × A → T3 × A → Prop} [Nonempty A] (hN : IsCircuit (SEdge R) N) (hfwd : ∀ (x : A), N (T3.i, x) (T3.m, x)) : (IsCircuit R fun (x y : A) => N (T3.o, x) (T3.i, y)) ∧ ∀ (p q : T3 × A), N p q ↔ SArc (fun (x y : A) => N (T3.o, x) (T3.i, y)) p q

A forward circuit of the split graph is a split directed circuit.

The correspondence

theorem DescriptiveComplexity.Split.sarc_sym_iff {A : Type} {Nxt : A → A → Prop} (x y : A) : SArc Nxt (T3.o, x) (T3.i, y) ∨ SArc Nxt (T3.i, y) (T3.o, x) ↔ Nxt x y

A split relation is read back on its exit-to-entry arcs.

noncomputable def DescriptiveComplexity.Split.splitEquiv {A : Type} [Finite A] [Nonempty A] (R : A → A → Prop) : { Nxt : A → A → Prop // IsCircuit R Nxt } ≃ { E : T3 × A → T3 × A → Prop // IsUCircuit (SEdge R) E }

The undirected circuits of the split graph are the directed circuits of the graph, bijectively.

Equations

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

The interpretation

def DescriptiveComplexity.Split.splitF : T3 → T3 → FirstOrder.Language.digraph.Formula (Fin 2 × Fin 1)

The arc formulas of the split graph, by tags.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Split.splitF DescriptiveComplexity.Split.T3.i DescriptiveComplexity.Split.T3.m = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 0))
• DescriptiveComplexity.Split.splitF DescriptiveComplexity.Split.T3.m DescriptiveComplexity.Split.T3.o = (FirstOrder.Language.var (0, 0)).equal (FirstOrder.Language.var (1, 0))
• DescriptiveComplexity.Split.splitF x✝¹ x✝ = ⊥

def DescriptiveComplexity.Split.splitInterp : FOInterpretation FirstOrder.Language.digraph FirstOrder.Language.digraph T3 1

The interpretation splitting each vertex of a digraph in three.

Equations

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

def DescriptiveComplexity.Split.splitPts (A : Type) : splitInterp.Map A ≃ T3 × A

The interpreted universe is three copies of the input.

Equations

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

theorem DescriptiveComplexity.Split.sharpHamCircuit_split (A : Type) [FirstOrder.Language.digraph.Structure A] [Finite A] [Nonempty A] : SharpHamCircuit.Count (splitInterp.Map A) = SharpDirHamCircuit.Count A

Correctness of the interpretation, for counting.

def DescriptiveComplexity.sharpDirHamCircuit_parsimonious_sharpHamCircuit : ParsimoniousReduction SharpDirHamCircuit SharpHamCircuit

#Directed Hamilton Circuit reduces parsimoniously to #Hamilton Circuit, by splitting each vertex in three; no order and no domain formula are needed.

Equations

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

theorem DescriptiveComplexity.sharpHamCircuit_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpHamCircuit

#Hamilton Circuit is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpHamCircuit_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpHamCircuit

#Hamilton Circuit is parsimoniously #P-complete: counting the Hamilton circuits of an undirected graph, as sets of edges. Registered in the Lax archive as Lax280166.HamCircuitComplete.sharpHamCircuit_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpHamCircuit_sharpP_complete : SharpP.Complete SharpHamCircuit

SharpHamCircuit is #P-complete: parsimoniously, hence under subtractive reductions.