Automatic CounTilings

Doron ZEILBERGER^{1}

An “Almost” Automatic Proof of Kasteleyn’s Formula

In the very special case of two dimer tiles (1 × 2 and 2 × 1), Kasteleyn and Fisher&Temperley ([K][FT], see [AS] for a beautiful recent survey) gave their deservedly celebrated beautiful formula for the weight-enumerator of an m × n rectangle for arbitrary (i.e. symbolic) m and n. To wit, if m and n are both even positive integers, and z and z′ the variables for the horizontal and vertical dimers respectively (what we called H and V above), then

Z_{m,n}(z, z′) = 2^{mn/2} ∏_{r=1}^{m/2} ∏_{s=1}^{n/2} [z^{2} cos^{2} \frac{rπ}{m + 1} + z^{′2} cos^{2} \frac{sπ}{n + 1}] ,  (K)

with a similar formula when n is odd. At this time of writing, computers can’t prove this formula in general. But for any specific m (but general(!) n), it is now a routine verification, thanks to our Maple package TILINGS. Of course, in practice, it can only be done for small values of m (m ≤ 10 on our computer), but with bigger and future computers, one would be able to go further. The proof is a beautiful example of (rigorous!) generalization from finitely many cases, combined with ‘general-nonsense’ linear algebra handwaving, that is nevertheless fully rigorous.

Let’s call the right side of (K) W_{m,n}(z, z′). We have to prove, for our given m, that W_{m,n}(z, z′) = Z_{m,n}(z, z′) for all n. For a fixed even m it is readily seen that W_{m,n}(z, z′) is expressible as a product of m/2 different dilations of U_{n}(z), the Tchebycheff polynomials of the second kind. It is well-known (and easily seen) that U_{n}(z) satisfies a (homogeneous) linear recurrence equation with constant (i.e. not depending on n) coefficients of order 2, and hence do does any of its dilation U_{m}(βz), and the product of m/2 of these creatures consequently satisfies a linear recurrence equation with constant coefficients of order 2^{m/2}. Hence its generating function, in t, is rational function whose denominator has degree 2^{m/2} and numerator degree < 2^{m/2}. We have to prove that this generating function coincides with the ‘real thing’, the rational function outputted by procedure GFtH of TILINGS, that also turns out to have the same degrees. But to prove that two rational functions whose numerator degrees is p and denominator degree is q are identical, we only have to check, by elementary linear algebra, that the first p + q + 2 terms in their Maclaurin series coincide, and this is a routine check, done in our package TILINGS by typing ProveKasteleyn(m);, for the general case (with z and z′), and ProveKasteleyn1(m);, for the straight-enumeration case ( z = z′ = 1).

By hindsight, Kasteleyn and Fisher&Temperley were extremely lucky, since in the very special case of the two dimer tiles, they were able to use graph theory and Pfaffians. The general case seems, at present, out of reach. Even the monomer-dimer problem is still wide open, let alone an “explicit” expression for the weight-enumerators for tilings of an m×n rectangle using other sets of tiles. Our Maple package TILINGS is a research tool that can automatically discover and rigorously prove results for specific m but general n. Let’s hope that the human can use it to discover new ansatzes by which to conjecture and hopefully prove some “explicit” form for the monomer-dimer and more general sets of tiles, where both m and n are symbolic. From this, one should be able to extract, at least, an “explicit” expression for the so-called thermodynamic limit, or at the very least, determine rigorously the critical exponents.

1 Department of Mathematics, Rutgers University (New Brunswick), Hill Center-Busch Campus, 110 Frelinghuysen

Rd., Piscataway, NJ 08854-8019, USA. zeilberg at math dot rutgers dot edu , http://www.math.rutgers.edu/~zeilberg . First version: Jan. 20, 2006. Accompanied by Maple packages TILINGS and RecTILINGS downloadable from Zeilberger’s website. Supported in part by the NSF.

I hope to explore these speculations in a subsequent article.