The gadgets attached at every site, flattened

DescriptiveComplexity.Site.attachAll attaches Valiant's gadget at the sites of a list, one sum type ⊕ Fin 4 at a time; the reductions draw the same matrix on the flat node type V ⊕ (S × Fin 4), the gadget nodes indexed by the sites themselves (DescriptiveComplexity.Site.flatAttach). The two have the same permanent (DescriptiveComplexity.Site.bperm_flatAttach): the nested type and the flat one are in bijection, entry by entry.

def DescriptiveComplexity.Site.flatAttach {V S : Type} [DecidableEq V] [DecidableEq S] (M₀ : V → V → ℤ) (site : S → Site V) : V ⊕ S × Fin 4 → V ⊕ S × Fin 4 → ℤ

The gadgets attached at every site, on the flat node type: the base matrix on V, and four gadget nodes per site. The first edge of a site enters its gadget at node 0 and leaves from node 3, the second enters at 3 and leaves from 0, as in DescriptiveComplexity.attachValiant.

Equations

• DescriptiveComplexity.Site.flatAttach M₀ site (Sum.inl a) (Sum.inl b) = M₀ a b
• DescriptiveComplexity.Site.flatAttach M₀ site (Sum.inl a) (Sum.inr (s, x_2)) = (if a = (site s).u ∧ x_2 = 0 then 1 else 0) + if a = (site s).u' ∧ x_2 = 3 then 1 else 0
• DescriptiveComplexity.Site.flatAttach M₀ site (Sum.inr (s, x_2)) (Sum.inl b) = (if x_2 = 3 ∧ b = (site s).v then 1 else 0) + if x_2 = 0 ∧ b = (site s).v' then 1 else 0
• DescriptiveComplexity.Site.flatAttach M₀ site (Sum.inr (s, x_2)) (Sum.inr (s', y)) = if s = s' then DescriptiveComplexity.xorGadget x_2 y else 0

The nested node type, flattened

def DescriptiveComplexity.Site.toFlat {V S : Type} (site : S → Site V) (l : List S) : AttachType V (List.map site l) → V ⊕ { s : S // s ∈ l } × Fin 4

The nested node type of the attachments along a list, read on the flat node type.

Equations

• DescriptiveComplexity.Site.toFlat site [] a = Sum.inl a
• DescriptiveComplexity.Site.toFlat site (s₀ :: l) (Sum.inl n) = Sum.map id (Prod.map (fun (s : { s : S // s ∈ l }) => ⟨↑s, ⋯⟩) id) (DescriptiveComplexity.Site.toFlat site l n)
• DescriptiveComplexity.Site.toFlat site (head :: tail) (Sum.inr x_2) = Sum.inr (⟨head, ⋯⟩, x_2)

def DescriptiveComplexity.Site.ofFlat {V S : Type} [DecidableEq S] (site : S → Site V) (l : List S) : V ⊕ { s : S // s ∈ l } × Fin 4 → AttachType V (List.map site l)

The flat node type, read on the nested one.

Equations

• DescriptiveComplexity.Site.ofFlat site [] (Sum.inl a) = a
• DescriptiveComplexity.Site.ofFlat site [] (Sum.inr (s, snd)) = absurd ⋯ ⋯
• DescriptiveComplexity.Site.ofFlat site (head :: l) (Sum.inl a) = Sum.inl (DescriptiveComplexity.Site.ofFlat site l (Sum.inl a))
• DescriptiveComplexity.Site.ofFlat site (s₀ :: l) (Sum.inr (s, x_2)) = if h : ↑s = s₀ then Sum.inr x_2 else Sum.inl (DescriptiveComplexity.Site.ofFlat site l (Sum.inr (⟨↑s, ⋯⟩, x_2)))

theorem DescriptiveComplexity.Site.toFlat_base {V S : Type} (site : S → Site V) (l : List S) (a : V) : toFlat site l (base (List.map site l) a) = Sum.inl a

theorem DescriptiveComplexity.Site.ofFlat_inl {V S : Type} [DecidableEq S] (site : S → Site V) (l : List S) (a : V) : ofFlat site l (Sum.inl a) = base (List.map site l) a

theorem DescriptiveComplexity.Site.ofFlat_toFlat {V S : Type} [DecidableEq S] (site : S → Site V) (l : List S) : l.Nodup → ∀ (n : AttachType V (List.map site l)), ofFlat site l (toFlat site l n) = n

theorem DescriptiveComplexity.Site.toFlat_ofFlat {V S : Type} [DecidableEq S] (site : S → Site V) (l : List S) (n : V ⊕ { s : S // s ∈ l } × Fin 4) : toFlat site l (ofFlat site l n) = n

theorem DescriptiveComplexity.Site.toFlat_injective {V S : Type} (site : S → Site V) (l : List S) (hl : l.Nodup) : Function.Injective (toFlat site l)

theorem DescriptiveComplexity.Site.toFlat_eq_inl_iff {V S : Type} (site : S → Site V) (l : List S) (hl : l.Nodup) (n : AttachType V (List.map site l)) (a : V) : toFlat site l n = Sum.inl a ↔ n = base (List.map site l) a

theorem DescriptiveComplexity.Site.bperm_flatAttach {V S : Type} [Fintype V] [DecidableEq V] [DecidableEq S] (site : S → Site V) [Fintype S] (M₀ : V → V → ℤ) : bperm (flatAttach M₀ site) = bperm (attachAll M₀ (List.map site Finset.univ.toList))

The permanent of the flat attachment is that of the nested one, the sites enumerated in any order.