Attaching Valiant's gadget at every site of a list

A site is a pair of edges u → v, u' → v' of a base matrix (DescriptiveComplexity.Site). Attaching Valiant's gadget at every site of a list l (DescriptiveComplexity.Site.attachAll, on the node type DescriptiveComplexity.Site.AttachType V l that adds four nodes per site) multiplies the permanent by 4 per site and leaves the XOR sum (DescriptiveComplexity.Site.xorSum): the sum, over the choices of one edge per site, of the permanent of the base minor with the rows and columns of the chosen edges deleted, a choice contributing nothing when it deletes a row twice (DescriptiveComplexity.Site.pdel_attachAll). The columns of the sites must be pairwise distinct and the two rows of a site distinct; the rows of different sites may coincide, which is what the vanishing of the repeated choices is for.

The XOR sum is the number of cycle covers of the base graph with the pair edges in place that use exactly one edge of each site, weighted by the base entries (DescriptiveComplexity.Site.xorSum_eq_sum, as a sum over the choice functions).

structure DescriptiveComplexity.Site (V : Type) : Type

A site: the two edges u → v and u' → v' a gadget replaces.

• u : V

  The row of the first edge.

• u' : V

  The row of the second edge.

• v : V

  The column of the first edge.

• v' : V

  The column of the second edge.

def DescriptiveComplexity.instDecidableEqSite.decEq {V✝ : Type} [DecidableEq V✝] (x✝ x✝¹ : Site V✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSite {V✝ : Type} [DecidableEq V✝] : DecidableEq (Site V✝)

Equations

• DescriptiveComplexity.instDecidableEqSite = DescriptiveComplexity.instDecidableEqSite.decEq

@[reducible, inline]

abbrev DescriptiveComplexity.Site.AttachType (V : Type) : List (Site V) → Type

The nodes after attaching a gadget at every site of the list: four more per site.

Equations

• DescriptiveComplexity.Site.AttachType V [] = V
• DescriptiveComplexity.Site.AttachType V (head :: l) = (DescriptiveComplexity.Site.AttachType V l ⊕ Fin 4)

@[instance_reducible]

instance DescriptiveComplexity.Site.instFintypeAttachType {V : Type} [Fintype V] (l : List (Site V)) : Fintype (AttachType V l)

Equations

• DescriptiveComplexity.Site.instFintypeAttachType [] = inst✝
• DescriptiveComplexity.Site.instFintypeAttachType (head :: l) = instFintypeSum (DescriptiveComplexity.Site.AttachType V l) (Fin 4)

@[instance_reducible]

instance DescriptiveComplexity.Site.instDecidableEqAttachType {V : Type} [DecidableEq V] (l : List (Site V)) : DecidableEq (AttachType V l)

Equations

• DescriptiveComplexity.Site.instDecidableEqAttachType [] = inst✝
• DescriptiveComplexity.Site.instDecidableEqAttachType (head :: l) = instDecidableEqSum

def DescriptiveComplexity.Site.base {V : Type} (l : List (Site V)) : V → AttachType V l

The base nodes, among the nodes after the attachments.

Equations

• DescriptiveComplexity.Site.base [] x✝ = x✝
• DescriptiveComplexity.Site.base (head :: l) x✝ = Sum.inl (DescriptiveComplexity.Site.base l x✝)

theorem DescriptiveComplexity.Site.base_injective {V : Type} (l : List (Site V)) : Function.Injective (base l)

def DescriptiveComplexity.Site.baseEmb {V : Type} (l : List (Site V)) : V ↪ AttachType V l

The base nodes, as an embedding.

Equations

• DescriptiveComplexity.Site.baseEmb l = { toFun := DescriptiveComplexity.Site.base l, inj' := ⋯ }

theorem DescriptiveComplexity.Site.map_baseEmb_cons {V : Type} (s : Site V) (l : List (Site V)) (A : Finset V) : Finset.map (baseEmb (s :: l)) A = Finset.map Function.Embedding.inl (Finset.map (baseEmb l) A)

theorem DescriptiveComplexity.Site.map_baseEmb_nil {V : Type} (A : Finset V) : Finset.map (baseEmb []) A = A

def DescriptiveComplexity.Site.attachAll {V : Type} [DecidableEq V] (M₀ : V → V → ℤ) (l : List (Site V)) : AttachType V l → AttachType V l → ℤ

The gadgets attached at every site of the list.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Site.attachAll M₀ [] = M₀

noncomputable def DescriptiveComplexity.Site.xorSum {V : Type} [Fintype V] [DecidableEq V] (M₀ : V → V → ℤ) : List (Site V) → Finset V → Finset V → ℤ

The XOR sum: one edge chosen per site, its row and column deleted, a choice deleting a row twice contributing nothing.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Site.xorSum M₀ [] x✝¹ x✝ = DescriptiveComplexity.pdel M₀ x✝¹ x✝

def DescriptiveComplexity.Site.cols {V : Type} : List (Site V) → List V

The columns of the sites of a list.

Equations

• DescriptiveComplexity.Site.cols [] = []
• DescriptiveComplexity.Site.cols (head :: l) = head.v :: head.v' :: DescriptiveComplexity.Site.cols l

theorem DescriptiveComplexity.Site.mem_cols_v {V : Type} (l : List (Site V)) (t : Site V) (ht : t ∈ l) : t.v ∈ cols l

theorem DescriptiveComplexity.Site.mem_cols_v' {V : Type} (l : List (Site V)) (t : Site V) (ht : t ∈ l) : t.v' ∈ cols l

theorem DescriptiveComplexity.Site.pdel_attachAll {V : Type} [Fintype V] [DecidableEq V] (M₀ : V → V → ℤ) (l : List (Site V)) (A B : Finset V) : (∀ s ∈ l, s.u ≠ s.u') → (cols l).Nodup → (∀ s ∈ l, s.v ∉ B ∧ s.v' ∉ B) → pdel (attachAll M₀ l) (Finset.map (baseEmb l) A) (Finset.map (baseEmb l) B) = 4 ^ l.length * xorSum M₀ l A B

Attaching a gadget at every site multiplies the permanent by 4 per site and leaves the XOR sum.

The XOR sum of self-loop sites, as a sum over the subsets of sites

def DescriptiveComplexity.Site.delRows {V : Type} [DecidableEq V] (l : List (Site V)) (T : Finset (Site V)) : Finset V

The rows deleted by a choice of one edge per site: the first row of the sites in T, the second row of the others.

Equations

• DescriptiveComplexity.Site.delRows l T = Finset.image (fun (s : DescriptiveComplexity.Site V) => if s ∈ T then s.u else s.u') l.toFinset

theorem DescriptiveComplexity.Site.delRows_nil {V : Type} [DecidableEq V] (T : Finset (Site V)) : delRows [] T = ∅

theorem DescriptiveComplexity.Site.delRows_cons {V : Type} [DecidableEq V] (s : Site V) (l : List (Site V)) (T : Finset (Site V)) : delRows (s :: l) T = insert (if s ∈ T then s.u else s.u') (delRows l T)

theorem DescriptiveComplexity.Site.delRows_insert_of_notMem {V : Type} [DecidableEq V] {s : Site V} {l : List (Site V)} (hs : s ∉ l) (T : Finset (Site V)) : delRows l (insert s T) = delRows l T

theorem DescriptiveComplexity.Site.xorSum_eq_sum {V : Type} [Fintype V] [DecidableEq V] (M₀ : V → V → ℤ) (l : List (Site V)) : (cols l).Nodup → (∀ s ∈ l, s.v = s.u ∧ s.v' = s.u') → ∀ (A : Finset V), (∀ s ∈ l, s.u ∉ A ∧ s.u' ∉ A) → xorSum M₀ l A A = ∑ T ∈ l.toFinset.powerset, pdel M₀ (A ∪ delRows l T) (A ∪ delRows l T)

The XOR sum of self-loop sites: when every site pairs two self-loops, the sum is over the subsets T of the sites, the first loop chosen at the sites of T and the second elsewhere, of the principal minor of the base matrix with the chosen rows deleted.