From an integer matrix to a 0-1 matrix, modulo 2 ^ L + 1

The matrix a gadget argument produces has small integer entries, some of them negative; a 0-1 matrix with the same permanent modulo 2 ^ L + 1 is its ladder expansion (DescriptiveComplexity.ladder) with the widths DescriptiveComplexity.widths: an entry -1 becomes a ladder of L levels of two rungs, i.e., 2 ^ L ≡ -1, and an entry k ≥ 0 a ladder whose least level has k rungs and the others one (DescriptiveComplexity.bperm_ladder_widths_modEq). When the permanent is known to be 4 ^ t * N with 4 ^ t * N ≤ 2 ^ L, the count N is read off the permanent of the 0-1 matrix by a remainder and a quotient (DescriptiveComplexity.bperm_ladder_widths_div): the arithmetic the one-call reduction to #Cycle Cover applies to the answer of its oracle.

def DescriptiveComplexity.widths {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] (M : V → V → ℤ) (a b : V) (ℓ : Λ) : ℕ

The widths of the ladders of an integer matrix: two rungs at every level for an entry -1; for an entry k ≥ 0, k rungs at the least level and one at every other.

Equations

• DescriptiveComplexity.widths M a b ℓ = if M a b = -1 then 2 else if ℓ = ⊥ then (M a b).toNat else 1

theorem DescriptiveComplexity.widths_le {V Λ : Type} [LinearOrder Λ] [BoundedOrder Λ] (M : V → V → ℤ) (hM : ∀ (a b : V), M a b ≤ 3) (a b : V) (ℓ : Λ) : widths M a b ℓ ≤ 3

theorem DescriptiveComplexity.bperm_ladder_widths_modEq {V Λ : Type} [Fintype V] [DecidableEq V] [LinearOrder Λ] [Fintype Λ] [BoundedOrder Λ] (M : V → V → ℤ) (hM : ∀ (a b : V), -1 ≤ M a b ∧ M a b ≤ 3) : ↑(bperm (ladder 3 (widths M))) ≡ bperm M [ZMOD 2 ^ Fintype.card Λ + 1]

The permanent of the 0-1 ladder expansion is congruent to the permanent of the integer matrix modulo 2 ^ L + 1, for entries between -1 and 3.

theorem DescriptiveComplexity.bperm_ladder_widths_div {V Λ : Type} [Fintype V] [DecidableEq V] [LinearOrder Λ] [Fintype Λ] [BoundedOrder Λ] (M : V → V → ℤ) (hM : ∀ (a b : V), -1 ≤ M a b ∧ M a b ≤ 3) (t N : ℕ) (hperm : bperm M = 4 ^ t * ↑N) (hlt : 4 ^ t * N ≤ 2 ^ Fintype.card Λ) : bperm (ladder 3 (widths M)) % (2 ^ Fintype.card Λ + 1) / 4 ^ t = N

The count is read off the permanent of the 0-1 matrix: when the permanent of the integer matrix is 4 ^ t * N with 4 ^ t * N ≤ 2 ^ L, the permanent of the ladder expansion, modulo 2 ^ L + 1 and divided by 4 ^ t, is N.