#Directed Hamilton Circuit: counting the circuits

The counting version of DescriptiveComplexity.DirHamCircuit: the number of Hamilton circuits of a digraph.

What is counted

The decision problem reads a circuit as a linear order of the universe (DescriptiveComplexity.TourOn), the circuit cut open at one place. A count of those orders is not a count of circuits: a circuit through n vertices can be cut at n places. What is counted here is the circuit itself, as the relation “y comes next after x” (DescriptiveComplexity.IsCircuit): the cyclic successor relation of some linear order (DescriptiveComplexity.CycSucc), following the arcs. Its support is the decision problem (DescriptiveComplexity.sharpDirHamCircuit_support_iff).

Membership

A circuit has no first-order certificate of its own, so the counting kernel (DescriptiveComplexity.sharpDirHamKernel) still guesses an order – but the one that starts at the least element of the instance: every circuit has exactly one (DescriptiveComplexity.exists_rooted_order, DescriptiveComplexity.linOrd_eq_of_cycSucc). Hence DescriptiveComplexity.sharpDirHamCircuit_mem_sharpP. Parsimonious hardness is in DescriptiveComplexity.Problems.Hamilton.CountingHardness.

Circuits

def DescriptiveComplexity.CycSucc {A : Type} (Le : A → A → Prop) (x y : A) : Prop

y comes next after x on the circuit a linear order is a cut of: it is the immediate successor of x, or x is the last element and y the first.

Equations

• DescriptiveComplexity.CycSucc Le x y = (DescriptiveComplexity.SuccOf Le x y ∨ (∀ (z : A), Le z x) ∧ ∀ (z : A), Le y z)

def DescriptiveComplexity.IsCircuit {A : Type} (R Nxt : A → A → Prop) : Prop

The relation Nxt is a Hamilton circuit of R: the cyclic successor relation of a linear order of the universe, included in R.

Equations

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

theorem DescriptiveComplexity.IsCircuit.of_equiv {A B : Type} (u : A ≃ B) {RA : A → A → Prop} {RB : B → B → Prop} (hR : ∀ (a a' : A), RA a a' ↔ RB (u a) (u a')) {Nxt : A → A → Prop} (h : IsCircuit RA Nxt) : IsCircuit RB fun (b b' : B) => Nxt (u.symm b) (u.symm b')

Circuits transport along an equivalence commuting with the relations.

def DescriptiveComplexity.circuitEquiv {A B : Type} (u : A ≃ B) {RA : A → A → Prop} {RB : B → B → Prop} (hR : ∀ (a a' : A), RA a a' ↔ RB (u a) (u a')) : { Nxt : A → A → Prop // Finite A ∧ IsCircuit RA Nxt } ≃ { Nxt : B → B → Prop // Finite B ∧ IsCircuit RB Nxt }

The circuits of two relations an equivalence exchanges are in bijection.

Equations

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

One order per circuit

theorem DescriptiveComplexity.linOrd_eq_of_cycSucc {A : Type} [Finite A] {Le Le' : A → A → Prop} (h : IsLinOrd Le) (h' : IsLinOrd Le') {a₀ : A} (hmin : ∀ (y : A), Le a₀ y) (hmin' : ∀ (y : A), Le' a₀ y) (hc : ∀ (x y : A), CycSucc Le x y ↔ CycSucc Le' x y) : Le = Le'

Two cuts of the same circuit at the same place are the same order.

theorem DescriptiveComplexity.exists_rooted_order {A : Type} [Finite A] {Le₀ : A → A → Prop} (h₀ : IsLinOrd Le₀) (a₀ : A) : ∃ (Le : A → A → Prop), IsLinOrd Le ∧ (∀ (y : A), Le a₀ y) ∧ ∀ (x y : A), CycSucc Le x y ↔ CycSucc Le₀ x y

A circuit can be cut anywhere: every order has a rotation starting at a given element, with the same cyclic successor.

theorem DescriptiveComplexity.card_rootedTour_eq {A : Type} [Finite A] [LinearOrder A] [Nonempty A] (R : A → A → Prop) : Nat.card { Le : A → A → Prop // IsLinOrd Le ∧ (∀ (x y : A), SuccOf Le x y → R x y) ∧ (∀ (x y : A), (∀ (z : A), Le x z) → (∀ (z : A), Le z y) → R y x) ∧ ∀ (x : A), IsBot x → ∀ (y : A), Le x y } = Nat.card { Nxt : A → A → Prop // IsCircuit R Nxt }

Circuits are the orders that start at a given element, bijectively: the tours of a relation whose least element is the least element of a linear order of the universe are as many as its circuits.

The counting problem

def DescriptiveComplexity.DirCircuit (A : Type) [FirstOrder.Language.digraph.Structure A] (Nxt : A → A → Prop) : Prop

The relation Nxt is a Hamilton circuit of a finite digraph.

Equations

• DescriptiveComplexity.DirCircuit A Nxt = (Finite A ∧ DescriptiveComplexity.IsCircuit (fun (x y : A) => DescriptiveComplexity.DGArc x y) Nxt)

noncomputable def DescriptiveComplexity.SharpDirHamCircuit : CountingProblem FirstOrder.Language.digraph

#Directed Hamilton Circuit: the number of Hamilton circuits of a digraph, a circuit being its “comes next” relation.

Equations

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

theorem DescriptiveComplexity.sharpDirHamCircuit_support_iff (A : Type) [FirstOrder.Language.digraph.Structure A] [Finite A] : SharpDirHamCircuit.support.Holds A ↔ DirHamCircuit.Holds A

The support of #Directed Hamilton Circuit is Directed Hamilton Circuit. Registered in the Lax archive as Lax280166.DirHamCircuitComplete.sharpDirHamCircuit_support_iff.

Membership

@[reducible, inline]

abbrev DescriptiveComplexity.dhcLang : FirstOrder.Language

The vocabulary of the counting kernel: the ordered digraph, expanded by the guessed order.

Equations

• DescriptiveComplexity.dhcLang = (FirstOrder.Language.digraph.sum FirstOrder.Language.order).sum DescriptiveComplexity.hamGuessBlock.lang

@[reducible, inline]

abbrev DescriptiveComplexity.dhcVarSym : dhcLang.Relations 2

The guessed order, over the vocabulary of the counting kernel.

Equations

• DescriptiveComplexity.dhcVarSym = Sum.inr DescriptiveComplexity.hLeRel

@[reducible, inline]

abbrev DescriptiveComplexity.dhcOrdSym : dhcLang.Relations 2

The order of the instance, over the vocabulary of the counting kernel.

Equations

• DescriptiveComplexity.dhcOrdSym = Sum.inl (Sum.inr FirstOrder.Language.leSymb)

def DescriptiveComplexity.hamAssignEquiv (A : Type) : hamGuessBlock.Assignment A ≃ (A → A → Prop)

A binary relation, as an assignment of the block guessing the order.

Equations

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

theorem DescriptiveComplexity.sharpDirHamCircuit_mem_sharpP : SharpP.Mem SharpDirHamCircuit

#Directed Hamilton Circuit is in #P: a circuit has exactly one cut at the least element of the instance.