Attaching a gadget to a matrix

A gadget attached to a matrix M₀ on V is a matrix D on its own nodes X, with in-edges from rows of V to columns of X and out-edges from rows of X to columns of V (DescriptiveComplexity.attach). The permanent of the result expands, by the Laplace expansion along the rows of the gadget, into a sum over the patterns – which in-ports are entered, which out-ports are left – of the permanent of the corresponding minor of the gadget times the permanent of the corresponding minor of M₀.

This file states that expansion for the gadget shape of Valiant's XOR gadget: two in-ports xin, xin' reached from two base rows u, u', and two out-ports o, o' leaving to two base columns v, v' (DescriptiveComplexity.pdel_attachXor). It is stated on minors, so that it can be applied to one gadget at a time when several are attached.

def DescriptiveComplexity.attach {R V X : Type} (M₀ : V → V → R) (D : X → X → R) (ins : V → X → R) (outs : X → V → R) : V ⊕ X → V ⊕ X → R

A gadget attached to a matrix: the base matrix M₀ on V, the gadget D on X, the in-edges ins from V to X and the out-edges outs from X to V.

Equations

• DescriptiveComplexity.attach M₀ D ins outs (Sum.inl a) (Sum.inl b) = M₀ a b
• DescriptiveComplexity.attach M₀ D ins outs (Sum.inl a) (Sum.inr x_2) = ins a x_2
• DescriptiveComplexity.attach M₀ D ins outs (Sum.inr x_2) (Sum.inl b) = outs x_2 b
• DescriptiveComplexity.attach M₀ D ins outs (Sum.inr x_2) (Sum.inr y) = D x_2 y

def DescriptiveComplexity.inEdge {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] (u : V) (x : X) : V → X → R

The indicator of one in-edge, from u to x.

Equations

• DescriptiveComplexity.inEdge u x a y = if a = u ∧ y = x then 1 else 0

def DescriptiveComplexity.outEdge {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] (x : X) (v : V) : X → V → R

The indicator of one out-edge, from x to v.

Equations

• DescriptiveComplexity.outEdge x v y b = if y = x ∧ b = v then 1 else 0

def DescriptiveComplexity.withGadget {V X : Type} [Fintype X] [DecidableEq V] [DecidableEq X] (A : Finset V) : Finset (V ⊕ X)

The rows of the gadget are deleted together with those in A.

Equations

• DescriptiveComplexity.withGadget A = Finset.map Function.Embedding.inl A ∪ Finset.map Function.Embedding.inr Finset.univ

theorem DescriptiveComplexity.mem_withGadget {V X : Type} [Fintype X] [DecidableEq V] [DecidableEq X] (A : Finset V) (w : V ⊕ X) : w ∈ withGadget A ↔ (∃ a ∈ A, w = Sum.inl a) ∨ ∃ (x : X), w = Sum.inr x

Local blocks and the base part of an expansion

def DescriptiveComplexity.gadgetRows {V X : Type} [Fintype X] [DecidableEq X] (O : Finset X) : Finset (V ⊕ X)

The gadget rows outside O, as a set of rows of the attached matrix.

Equations

• DescriptiveComplexity.gadgetRows O = Finset.map Function.Embedding.inr {x : X | x ∉ O}

theorem DescriptiveComplexity.mem_gadgetRows {V X : Type} [Fintype X] [DecidableEq X] (O : Finset X) (w : V ⊕ X) : w ∈ gadgetRows O ↔ ∃ (x : X), w = Sum.inr x ∧ x ∉ O

theorem DescriptiveComplexity.card_gadgetRows {V X : Type} [Fintype X] [DecidableEq X] (O : Finset X) : (gadgetRows O).card = {x : X | x ∉ O}.card

theorem DescriptiveComplexity.notMem_map_inl_of_inr {V X : Type} (A : Finset V) (x : X) : Sum.inr x ∉ Finset.map Function.Embedding.inl A

theorem DescriptiveComplexity.gadgetRows_subset {V X : Type} [Fintype X] [DecidableEq X] (O : Finset X) : gadgetRows O ⊆ gadgetRows ∅

The expansion of Valiant's gadget shape

@[reducible, inline]

abbrev DescriptiveComplexity.attachXor {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] (M₀ : V → V → R) (D : X → X → R) (u u' v v' : V) (xin xin' o o' : X) : V ⊕ X → V ⊕ X → R

The XOR gadget shape: two in-edges, from u to xin and from u' to xin', and two out-edges, from o to v and from o' to v'.

Equations

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

theorem DescriptiveComplexity.attachXor_inl_inl {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (a b : V) : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl a) (Sum.inl b) = M₀ a b

theorem DescriptiveComplexity.attachXor_inr_inr {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (x y : X) : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inr x) (Sum.inr y) = D x y

theorem DescriptiveComplexity.attachXor_inr_inl {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (x : X) (b : V) : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inr x) (Sum.inl b) = (if x = o ∧ b = v then 1 else 0) + if x = o' ∧ b = v' then 1 else 0

theorem DescriptiveComplexity.attachXor_inl_inr {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (a : V) (x : X) : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl a) (Sum.inr x) = (if a = u ∧ x = xin then 1 else 0) + if a = u' ∧ x = xin' then 1 else 0

theorem DescriptiveComplexity.attachXor_inl_inr_xin {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (hxx' : xin ≠ xin') {a : V} (ha : a ≠ u) : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl a) (Sum.inr xin) = 0

theorem DescriptiveComplexity.attachXor_inl_inr_xin' {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (hxx' : xin ≠ xin') {a : V} (ha : a ≠ u') : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl a) (Sum.inr xin') = 0

theorem DescriptiveComplexity.attachXor_u_xin {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (hxx' : xin ≠ xin') : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl u) (Sum.inr xin) = 1

theorem DescriptiveComplexity.attachXor_u'_xin' {R : Type} [CommSemiring R] {V X : Type} [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (hxx' : xin ≠ xin') : attachXor M₀ D u u' v v' xin xin' o o' (Sum.inl u') (Sum.inr xin') = 1

theorem DescriptiveComplexity.card_gadgetRows_singleton {V X : Type} [Fintype X] [DecidableEq X] (x : X) : (gadgetRows {x}).card = Fintype.card X - 1

theorem DescriptiveComplexity.card_gadgetRows_pair {V X : Type} [Fintype X] [DecidableEq X] {x y : X} (hxy : x ≠ y) : (gadgetRows {x, y}).card = Fintype.card X - 2

theorem DescriptiveComplexity.card_gadgetRows_empty {V X : Type} [Fintype X] [DecidableEq X] : (gadgetRows ∅).card = Fintype.card X

theorem DescriptiveComplexity.mem_insert_inl_inl_union_gadgetRows {V X : Type} [Fintype X] [DecidableEq V] [DecidableEq X] (A : Finset V) (a a' : V) (o₀ o₁ : X) (w : V ⊕ X) : w ∈ insert (Sum.inl a') (insert (Sum.inl a) (insert (Sum.inr o₀) (insert (Sum.inr o₁) (Finset.map Function.Embedding.inl A)) ∪ gadgetRows {o₀, o₁})) ↔ (∃ a'' ∈ insert a (insert a' A), w = Sum.inl a'') ∨ ∃ (x : X), w = Sum.inr x

theorem DescriptiveComplexity.mem_insert_inr_inr_union_gadgetRows {V X : Type} [Fintype X] [DecidableEq V] [DecidableEq X] (B : Finset V) (x x' : X) (w : V ⊕ X) : w ∈ insert (Sum.inr x') (insert (Sum.inr x) (Finset.map Function.Embedding.inl B ∪ gadgetRows {x, x'})) ↔ (∃ b ∈ B, w = Sum.inl b) ∨ ∃ (y : X), w = Sum.inr y

theorem DescriptiveComplexity.insert_inl_map {V X : Type} [DecidableEq V] [DecidableEq X] (a : V) (A : Finset V) : insert (Sum.inl a) (Finset.map Function.Embedding.inl A) = Finset.map Function.Embedding.inl (insert a A)

theorem DescriptiveComplexity.pdel_attachXor {R : Type} [CommSemiring R] {V X : Type} [Fintype V] [Fintype X] [DecidableEq V] [DecidableEq X] {M₀ : V → V → R} {D : X → X → R} {u u' v v' : V} {xin xin' o o' : X} (hxx' : xin ≠ xin') (A B : Finset V) (hoo' : o ≠ o') (huu' : u ≠ u') (hvv' : v ≠ v') (hv : v ∉ B) (hv' : v' ∉ B) : pdel (attachXor M₀ D u u' v v' xin xin' o o') (Finset.map Function.Embedding.inl A) (Finset.map Function.Embedding.inl B) = ((((pdel D ∅ ∅ * pdel M₀ A B + pdel D {o} {xin} * if u ∈ A then 0 else pdel M₀ (insert u A) (insert v B)) + pdel D {o} {xin'} * if u' ∈ A then 0 else pdel M₀ (insert u' A) (insert v B)) + pdel D {o'} {xin} * if u ∈ A then 0 else pdel M₀ (insert u A) (insert v' B)) + pdel D {o'} {xin'} * if u' ∈ A then 0 else pdel M₀ (insert u' A) (insert v' B)) + pdel D {o, o'} {xin, xin'} * if u ∈ A ∨ u' ∈ A then 0 else pdel M₀ (insert u (insert u' A)) (insert v (insert v' B))

The expansion of the XOR gadget shape. The permanent of the matrix with the gadget is the sum, over the patterns of use of its ports, of the permanent of the gadget minor of the pattern times the permanent of the base minor with the rows entering and the columns left: no port used; the first in-port entered from u and the first out-port left to v, or the second out-port left to v'; the second in-port entered from u' likewise; both in-ports entered and both out-ports left.