Alternating sign matrices and Robbins numbers

DefinitionRobbins numbers#✓fully proved

For \(n \in \mathbb{N}\), the Robbins number \(A_n\) is the natural number obtained by dividing \(\prod_{k=0}^{n-1} (3k+1)!\) by \(\prod_{k=0}^{n-1} (n+k)!\), where the division is division of natural numbers rounded down.

def robbinsNumber (n : ℕ) : ℕ :=
  (∏ k ∈ Finset.range n, (3 * k + 1).factorial) /
    (∏ k ∈ Finset.range n, (n + k).factorial)

Sources

• Paul Barry, "From Fibonacci to Robbins: Series Reversion and Hankel Transforms," Journal of Integer Sequences 24 (2021).

Used by 1

Used bySigned Robbins numbers

DefinitionSigned Robbins numbers#✓fully proved

For \(n \in \mathbb{N}\), the signed Robbins number is the integer \((-1)^{\binom{n+1}{2}} A_{n+1}\), where \(A_{n+1}\) is the Robbins number.

def signedRobbinsNumber (n : ℕ) : ℤ :=
  (-1) ^ Nat.choose (n + 1) 2 * (robbinsNumber (n + 1) : ℤ)

Uses 1

Statement usesRobbins numbers

DefinitionRow partial sums of a matrix#✓fully proved

For an \(n \times n\) integer matrix \(A\) and indices \(i, k \in \{0, \dots, n-1\}\), the row partial sum of \(A\) at \((i, k)\) is the sum of the entries of row \(i\) in columns \(0\) through \(k\), that is, \(\sum_{j \le k} A_{ij}\).

def rowPartialSum {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (i k : Fin n) : ℤ :=
  Finset.sum (Finset.univ.filter (fun j : Fin n => j ≤ k)) (fun j => A i j)

Used by 1

Used byAlternating sign matrices

DefinitionColumn partial sums of a matrix#✓fully proved

For an \(n \times n\) integer matrix \(A\) and indices \(j, k \in \{0, \dots, n-1\}\), the column partial sum of \(A\) at \((j, k)\) is the sum of the entries of column \(j\) in rows \(0\) through \(k\), that is, \(\sum_{i \le k} A_{ij}\).

def colPartialSum {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (j k : Fin n) : ℤ :=
  Finset.sum (Finset.univ.filter (fun i : Fin n => i ≤ k)) (fun i => A i j)

Used by 1

Used byAlternating sign matrices

DefinitionIntegers equal to zero or one#✓fully proved

An integer \(a\) is zero or one when \(a = 0\) or \(a = 1\). These are the values allowed for the partial sums of an alternating sign matrix.

def IsZeroOrOne (a : ℤ) : Prop := a = 0 ∨ a = 1

Used by 1

Used byAlternating sign matrices

DefinitionAlternating sign matrices#✓fully proved

An \(n \times n\) integer matrix \(A\) is an alternating sign matrix when every entry of \(A\) is \(-1\), \(0\) or \(1\); for all indices \(i, k\) the row partial sum \(\sum_{j \le k} A_{ij}\) is \(0\) or \(1\); for all indices \(j, k\) the column partial sum \(\sum_{i \le k} A_{ij}\) is \(0\) or \(1\); every row of \(A\) sums to \(1\); and every column of \(A\) sums to \(1\).

def IsAlternatingSignMatrix {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Prop :=
  (∀ i j, A i j = -1 ∨ A i j = 0 ∨ A i j = 1) ∧
  (∀ i k, IsZeroOrOne (rowPartialSum A i k)) ∧
  (∀ j k, IsZeroOrOne (colPartialSum A j k)) ∧
  (∀ i, ∑ j, A i j = 1) ∧
  (∀ j, ∑ i, A i j = 1)

Uses 3 · Used by 1

Statement usesIntegers equal to zero or one · Column partial sums of a matrix · Row partial sums of a matrix

Used byAlternating sign matrices of size \(n\)

AbbreviationAlternating sign matrices of size \(n\)#✓fully proved

For a natural number \(n\), this is the collection of all \(n \times n\) integer matrices that are alternating sign matrices.

abbrev ASMatrix (n : ℕ) :=
  { A : Matrix (Fin n) (Fin n) ℤ // IsAlternatingSignMatrix A }

Uses 1 · Used by 1

Statement usesAlternating sign matrices

Used byAlternating sign matrix theorem

DefinitionThe Robbins product#✓fully proved

For a natural number \(n\), the Robbins product is the rational number

\[\prod_{k=0}^{n-1} \frac{(3k+1)!}{(n+k)!},\]

an empty product, equal to \(1\), when \(n = 0\).

def robbinsProduct (n : ℕ) : ℚ :=
  Finset.prod (Finset.range n)
    (fun k => (Nat.factorial (3 * k + 1) : ℚ) / (Nat.factorial (n + k) : ℚ))

Used by 1

Used byAlternating sign matrix theorem

TheoremAlternating sign matrix theorem#●ready to prove

For every natural number \(n\), the number of \(n \times n\) alternating sign matrices equals the Robbins product \(\prod_{k=0}^{n-1} \frac{(3k+1)!}{(n+k)!}\).

public theorem_wanted alternating_sign_matrix_count (n : ℕ) :
    (Nat.card (ASMatrix n) : ℚ) = robbinsProduct n

Sources

• D. Zeilberger (1996); G. Kuperberg (1996). Knill, §168. Problem alternating_sign_matrix_count of the lean-eval benchmark.

Uses 2

Statement usesAlternating sign matrices of size \(n\) · The Robbins product

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.