Expanding a weighted graph into a 0-1 graph: ladders

A matrix of natural numbers is the adjacency matrix of a digraph with parallel edges, and its permanent counts its cycle covers, an edge of weight k counting k times. The ladder expansion (DescriptiveComplexity.ladder) replaces every edge a → b by a ladder: a sequence of levels ℓ : Λ, a finite linear order with a least and a greatest level, with wd a b ℓ rungs at level ℓ; a reaches every rung of the least level, every rung reaches every rung of the next level, every rung of the greatest level reaches b, and every rung loops on itself. The result is a 0-1 matrix, and its permanent is the permanent of the matrix of the products ∏ ℓ, wd a b ℓ (DescriptiveComplexity.bperm_ladder): a cycle cover of the ladder graph is a cycle cover of the weighted graph together with a choice of one rung at each level of each edge it uses, the other rungs looping.

Series and parallel composition at once, which is what a reduction needs: an edge of weight 2 ^ n costs n levels of two rungs, an edge of weight 3 a single level of three rungs.

def DescriptiveComplexity.Rung {V Λ : Type} (K : ℕ) (wd : V → V → Λ → ℕ) : Type

The rungs of the ladders: the copy j of the level ℓ of the ladder from a to b, for j < wd a b ℓ.

Equations

• DescriptiveComplexity.Rung K wd = { q : V × V × Λ × Fin K // ↑q.2.2.2 < wd q.1 q.2.1 q.2.2.1 }

@[instance_reducible]

instance DescriptiveComplexity.Rung.instFintype {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} [Fintype V] [Fintype Λ] : Fintype (Rung K wd)

Equations

• DescriptiveComplexity.Rung.instFintype = Subtype.fintype fun (q : V × V × Λ × Fin K) => ↑q.2.2.2 < wd q.1 q.2.1 q.2.2.1

instance DescriptiveComplexity.Rung.instFinite {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} [Finite V] [Finite Λ] : Finite (Rung K wd)

@[instance_reducible]

instance DescriptiveComplexity.Rung.instDecidableEq {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} [DecidableEq V] [DecidableEq Λ] : DecidableEq (Rung K wd)

Equations

• DescriptiveComplexity.Rung.instDecidableEq = Subtype.instDecidableEq

@[reducible, inline]

abbrev DescriptiveComplexity.Rung.src {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) : V

The source of the ladder a rung belongs to.

Equations

• q.src = (↑q).1

@[reducible, inline]

abbrev DescriptiveComplexity.Rung.tgt {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) : V

The target of the ladder a rung belongs to.

Equations

• q.tgt = (↑q).2.1

@[reducible, inline]

abbrev DescriptiveComplexity.Rung.lvl {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) : Λ

The level of a rung.

Equations

• q.lvl = (↑q).2.2.1

@[reducible, inline]

abbrev DescriptiveComplexity.Rung.idx {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) : Fin K

The index of a rung at its level.

Equations

• q.idx = (↑q).2.2.2

theorem DescriptiveComplexity.Rung.ext {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} {q q' : Rung K wd} (ha : q.src = q'.src) (hb : q.tgt = q'.tgt) (hℓ : q.lvl = q'.lvl) (hj : q.idx = q'.idx) : q = q'

inductive DescriptiveComplexity.LadderEdge {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] (K : ℕ) (wd : V → V → Λ → ℕ) : V ⊕ Rung K wd → V ⊕ Rung K wd → Prop

The edges of the ladder graph.

• enter {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) (h : q.lvl = ⊥) : LadderEdge K wd (Sum.inl q.src) (Sum.inr q)

  The source reaches every rung of the least level.

• loop {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) : LadderEdge K wd (Sum.inr q) (Sum.inr q)

  Every rung loops.

• step {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} (q q' : Rung K wd) (ha : q.src = q'.src) (hb : q.tgt = q'.tgt) (hℓ : q.lvl ⋖ q'.lvl) : LadderEdge K wd (Sum.inr q) (Sum.inr q')

  Every rung reaches every rung of the next level.

• leave {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} (q : Rung K wd) (h : q.lvl = ⊤) : LadderEdge K wd (Sum.inr q) (Sum.inl q.tgt)

  Every rung of the greatest level reaches the target.

noncomputable def DescriptiveComplexity.ladder {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] (K : ℕ) (wd : V → V → Λ → ℕ) (n n' : V ⊕ Rung K wd) : ℕ

The ladder expansion of a weighted matrix: the 0-1 adjacency matrix of the ladder graph.

Equations

• DescriptiveComplexity.ladder K wd n n' = if DescriptiveComplexity.LadderEdge K wd n n' then 1 else 0

Levels

Choices

@[reducible, inline]

abbrev DescriptiveComplexity.Choice {V Λ : Type} (wd : V → V → Λ → ℕ) : Type

A choice: a cycle cover of the weighted graph with one rung chosen at each level of each edge it uses.

Equations

• DescriptiveComplexity.Choice wd = ((σ : V ≃ V) × ((a : V) → (ℓ : Λ) → Fin (wd a (σ a) ℓ)))

Every cover comes from a choice

def DescriptiveComplexity.Act {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) (q : Rung K wd) : Prop

A rung is active in a cover when it does not loop.

Equations

• DescriptiveComplexity.Act e q = (e (Sum.inr q) ≠ Sum.inr q)

theorem DescriptiveComplexity.act_of_eq_inl {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) {a : V} {q : Rung K wd} (h : e (Sum.inl a) = Sum.inr q) : Act e q

theorem DescriptiveComplexity.act_of_eq_inr {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) {q' q : Rung K wd} (h : e (Sum.inr q') = Sum.inr q) (hne : q' ≠ q) : Act e q

theorem DescriptiveComplexity.act_top {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) (he : ∀ (n : V ⊕ Rung K wd), LadderEdge K wd n (e n)) {q : Rung K wd} (h : Act e q) (ht : q.lvl = ⊤) : e (Sum.inr q) = Sum.inl q.tgt

def DescriptiveComplexity.tgt {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) (a : V) : V

The target of the edge leaving a: where the cover sends a.

Equations

• DescriptiveComplexity.tgt e a = Sum.elim (fun (x : V) => a) DescriptiveComplexity.Rung.tgt (e (Sum.inl a))

theorem DescriptiveComplexity.tgt_eq {V Λ : Type} {K : ℕ} {wd : V → V → Λ → ℕ} (e : V ⊕ Rung K wd ≃ V ⊕ Rung K wd) {a : V} {q : Rung K wd} (h : e (Sum.inl a) = Sum.inr q) : tgt e a = q.tgt

theorem DescriptiveComplexity.bperm_ladder {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] {K : ℕ} {wd : V → V → Λ → ℕ} [Fintype V] [DecidableEq V] [Fintype Λ] (hK : ∀ (a b : V) (ℓ : Λ), wd a b ℓ ≤ K) : bperm (ladder K wd) = bperm fun (a b : V) => ∏ ℓ : Λ, wd a b ℓ

The permanent of the ladder expansion is the permanent of the matrix of the products of the widths.