Aztec dragon tilings

AbbreviationCells of the Aztec diamond#✓fully proved

For \(m \in \mathbb{N}\), the cells of the Aztec diamond region of order \(m\) are the pairs of integers \((i, j)\) with \(|2i + 1| + |2j + 1| \le 2m\). The pair \((i, j)\) stands for the unit square with lower-left corner \((i, j)\) and center \((i + \frac12, j + \frac12)\), so the condition says that this center satisfies \(|i + \frac12| + |j + \frac12| \le m\).

The Aztec diamond graph \(AD_m\) has these \(2m(m + 1)\) cells as vertices and joins two cells when they share a side.

abbrev AztecCell (m : ℕ) : Type :=
  {c : ℤ × ℤ // |2 * c.1 + 1| + |2 * c.2 + 1| ≤ 2 * (m : ℤ)}
Used by 2
Used byPropp's Aztec dragon count · The Aztec dragon graph

DefinitionCiucu's weight matrix for the Aztec dragon#✓fully proved

Ciucu's periodic weight matrix of Section 7 (the display before (7.1)) is the \(4 \times 4\) matrix with natural number entries, rows and columns indexed by \(0, 1, 2, 3\),

\[A = \begin{pmatrix}1 & 1 & 1 & 1\\1 & 0 & 1 & 1\\0 & 1 & 1 & 1\\1 & 1 & 1 & 1\end{pmatrix}.\]

Its two zero entries, in positions \((1, 1)\) and \((2, 0)\), delete edges of the Aztec diamond graph.

def ciucuMatrix : Matrix (Fin 4) (Fin 4) ℕ :=
  !![1, 1, 1, 1; 1, 0, 1, 1; 0, 1, 1, 1; 1, 1, 1, 1]
Used by 1
Used byCiucu's periodic weight

DefinitionRow index of an edge of the Aztec diamond#✓fully proved

For \(m \in \mathbb{N}\) and pairs of integers \(c = (c_1, c_2)\) and \(d = (d_1, d_2)\), put \(X = c_1 + d_1 + 1\) and \(Y = c_2 + d_2 + 1\), the doubled coordinates of the center of the edge joining \(c\) and \(d\). The row index of this edge is \(\lfloor (X + Y + 2m - 1) / 2 \rfloor\), so the rows of the \(2m \times 2m\) array of edge centers of the Aztec diamond graph \(AD_m\) are the diagonals \(X + Y = \mathrm{const}\), numbered \(0, \dots, 2m - 1\).

def edgeRow (m : ℕ) (c d : ℤ × ℤ) : ℤ :=
  ((c.1 + d.1 + 1) + (c.2 + d.2 + 1) + 2 * m - 1) / 2
Used by 1
Used byCiucu's periodic weight

DefinitionColumn index of an edge of the Aztec diamond#✓fully proved

For \(m \in \mathbb{N}\) and pairs of integers \(c = (c_1, c_2)\) and \(d = (d_1, d_2)\), put \(X = c_1 + d_1 + 1\) and \(Y = c_2 + d_2 + 1\), the doubled coordinates of the center of the edge joining \(c\) and \(d\). The column index of this edge is \(\lfloor (X - Y + 2m - 1) / 2 \rfloor\), so the columns of the array of edge centers of the Aztec diamond graph \(AD_m\) are the diagonals \(X - Y = \mathrm{const}\), numbered \(0, \dots, 2m - 1\).

def edgeCol (m : ℕ) (c d : ℤ × ℤ) : ℤ :=
  ((c.1 + d.1 + 1) - (c.2 + d.2 + 1) + 2 * m - 1) / 2
Used by 1
Used byCiucu's periodic weight

DefinitionCiucu's periodic weight#✓fully proved

For \(m \in \mathbb{N}\) and pairs of integers \(c\) and \(d\), let \(r\) and \(s\) be the row and column indices of the pair \((c, d)\) in the array of edge centers of the Aztec diamond graph \(AD_m\). The weight \(\mathrm{wt}_A(c, d)\) is the entry of Ciucu's matrix \(A\) in row \(r \bmod 4\) and column \(s \bmod 4\); that is, \(A\) is placed in a corner of the array and repeated with period \(4\) in both directions (Ciucu's Definition 3.3).

def ciucuWeight (m : ℕ) (c d : ℤ × ℤ) : ℕ :=
  ciucuMatrix ⟨(edgeRow m c d % 4).toNat % 4, Nat.mod_lt _ (Nat.succ_pos 3)⟩
    ⟨(edgeCol m c d % 4).toNat % 4, Nat.mod_lt _ (Nat.succ_pos 3)⟩
Uses 3 · Used by 1
Statement usesCiucu's weight matrix for the Aztec dragon · Column index of an edge of the Aztec diamond · Row index of an edge of the Aztec diamond
Used byThe Aztec dragon graph

DefinitionThe Aztec dragon graph#✓fully proved

For \(n \in \mathbb{N}\), the dragon graph of order \(n\) is the graph on the cells of the Aztec diamond of order \(2n\) in which two cells \(c\) and \(d\) are adjacent when they share a side (their coordinates differ by \(1\) in exactly one place) and the edge joining them has weight \(\mathrm{wt}_A(c, d) = 1\) under Ciucu's periodic weight. It is the spanning subgraph of the Aztec diamond graph \(AD_{2n}\) obtained by deleting the edges of weight \(0\); Ciucu's (7.1) shows that its perfect matchings are equinumerous with the tilings of the Aztec dragon \(R_n\).

def dragonGraph (n : ℕ) : SimpleGraph (AztecCell (2 * n)) :=
  SimpleGraph.fromRel fun c d =>
    |c.1.1 - d.1.1| + |c.1.2 - d.1.2| = 1 ∧ ciucuWeight (2 * n) c.1 d.1 = 1
Uses 2 · Used by 1
Statement usesCells of the Aztec diamond · Ciucu's periodic weight
Used byPropp's Aztec dragon count

DefinitionPropp's Aztec dragon count#✓fully proved

The statement that for every natural number \(n\) the dragon graph of order \(n\) (the spanning subgraph of the Aztec diamond graph \(AD_{2n}\) that keeps exactly the edges of weight \(1\) under Ciucu's periodic weight \(\mathrm{wt}_A\)) has exactly \(2^{n(n+1)}\) perfect matchings. This is Propp's Problem 15 in the form of Ciucu's (7.1) and Theorem 7.1 at \(a = 1\).

def aztecDragonCount : Prop :=
  ∀ n : ℕ, Nat.card {M : (dragonGraph n).Subgraph // M.IsPerfectMatching} = 2 ^ (n * (n + 1))
Uses 2 · Used by 1
Statement usesCells of the Aztec diamond · The Aztec dragon graph
Used byPerfect matchings of the Aztec dragon graph (Ciucu, Wieland)

TheoremPerfect matchings of the Aztec dragon graph (Ciucu, Wieland)#●ready to prove

For every natural number \(n\), the dragon graph of order \(n\) (the spanning subgraph of the Aztec diamond graph \(AD_{2n}\) that keeps exactly the edges of weight \(1\) under Ciucu's periodic weight \(\mathrm{wt}_A\)) has exactly \(2^{n(n+1)}\) perfect matchings.

Ciucu proves that the number of perfect matchings of \(AD_{2n}\) with the periodic weight \(\mathrm{wt}_A\) is \(2^{n(n+1)}\) (Theorem 7.1 at \(a = 1\)) and, by his identification (7.1) of these matchings with the tilings of the Aztec dragon \(R_n\), that \(R_n\) has \(2^{n(n+1)}\) tilings (Corollary 7.2), as Propp's Problem 15 asks.

public theorem_wanted aztecDragonCount_holds : aztecDragonCount
Sources
  • J. Propp, Twenty open problems in enumeration of matchings (1998), arXiv:math/9801060, Problem 15; resolution: M. Ciucu, Perfect matchings and perfect powers, J. Algebraic Combin. 17 (2003), 335-375, arXiv:math/0501521, Section 7 (The Aztec dragon): (7.1) M(R_n) = M(AD_2n; wt_A) for the displayed 4 × 4 matrix A; Theorem 7.1, M(AD_2n; wt_B) = (1 + a²)^(n(n+1)), where B at a = 1 is A; Corollary 7.2, T(R_n) = 2^(n(n+1)); Ciucu calls it an ex-conjecture of Propp first proved by B. Wieland (unpublished; Propp's progress report arXiv:math/9904150, Problem 15: 'Ben Wieland solved this problem'), https://arxiv.org/abs/math/0501521.
Uses 1
Statement usesPropp's Aztec dragon count
7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.