
%tilings.tex:
%%a Plain TeX file by Doron Zeilberger (x pages)

%begin macros
\def\L{{\cal L}}
\def\A{{\cal A}}
\def\B{{\cal B}}
\baselineskip=14pt
\parskip=10pt
\def\halmos{\hbox{\vrule height0.15cm width0.01cm\vbox{\hrule height
  0.01cm width0.2cm \vskip0.15cm \hrule height 0.01cm width0.2cm}\vrule
  height0.15cm width 0.01cm}}
\font\eightrm=cmr8 \font\sixrm=cmr6
\font\eighttt=cmtt8
\magnification=\magstephalf
\def\P{{\cal P}}
\def\Q{{\cal Q}}
\def\1{{\overline{1}}}
\def\2{{\overline{2}}}
\parindent=0pt
\overfullrule=0in
\def\Tilde{\char126\relax}
\def\frac#1#2{{#1 \over #2}}
%\headline={\rm  \ifodd\pageno  \RightHead  \else  \LeftHead  \fi}
%\def\RightHead{\centerline{
%Title
%}}
%\def\LeftHead{ \centerline{Doron Zeilberger}}
%end macros
\bf
\centerline
{
Automatic CounTilings
}
\rm
\bigskip
\centerline{ {\it
Doron 
ZEILBERGER}\footnote{$^1$}
{\eightrm  \raggedright
Department of Mathematics, Rutgers University (New Brunswick),
Hill Center-Busch Campus, 110 Frelinghuysen Rd., Piscataway,
NJ 08854-8019, USA.
%\break
{\eighttt zeilberg  at math dot rutgers dot edu} ,
\hfill \break
{\eighttt http://www.math.rutgers.edu/\~{}zeilberg} .
First version: Jan. 20, 2006.
Accompanied by Maple packages {\eighttt TILINGS} and
{\eighttt RecTILINGS}
downloadable from Zeilberger's website.
Supported in part by the NSF.
}
}


{\bf An ``Almost'' Automatic Proof of Kasteleyn's Formula}

In the very special case of two dimer tiles ($1 \times 2$ and $2 \times 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 \times n$ rectangle for
{\it 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} \prod_{r=1}^{m/2}\prod_{s=1}^{n/2}
\left [ z^2 \cos^2 { {r\pi} \over {m+1}}+
z'^2 \cos^2 { {s\pi} \over {n+1}} \right ] \quad,
\eqno(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 {\it specific} $m$ (but general(!) $n$), it is now a routine verification, thanks to our Maple
package {\tt TILINGS}. Of course, in practice, it can only be done for small values
of $m$ ($m \leq 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 {\it 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 {\it 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) {\it 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(\beta 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 {\tt GFtH} of {\tt 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
{\tt TILINGS} by typing {\tt ProveKasteleyn(m);}, for the general case (with $z$ and $z'$),
and {\tt 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 \times n$ rectangle using other sets of
tiles. Our Maple package {\tt TILINGS} is a {\it research tool} that can automatically
discover and rigorously prove results for {\bf specific} $m$ but general $n$.
Let's hope that the human can use it to discover new {\bf ansatzes} by which
to conjecture and hopefully prove some ``explicit'' form for the
monomer-dimer and more general sets of tiles, where {\it both} 
$m$ and $n$ are {\bf symbolic}.
From this, one should be able to extract, at least, an ``explicit'' expression
for the so-called {\it thermodynamic limit}, or at the very least, determine
rigorously the {\it critical exponents}.

I hope to explore these speculations in a subsequent article.

\end


