%ten.tex:
%%a Plain TeX file by S.B. Ekhad, Vince Vatter, and Doron Zeilberger (6 pages)
%begin macros
\def\L{{\cal L}}
\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\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
{
A Proof of the Loehr-Warrington
Amazing TEN to the Power n Conjecture
}
\rm
\bigskip
\centerline{ {\it
Shalosh B. EKHAD${}^1$, Vince VATTER${}^1$, and 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 [ekhad, vatter, zeilberg] at math dot rutgers dot edu} ,
\hfill \break
{\eighttt http://www.math.rutgers.edu/\~{}[zeilberg/ekhad.html,
vatter, zeilberg]} .
First version: Sept. 14, 2005.
Accompanied by Maple package {\eighttt TEN}
downloadable from Zeilberger's website.
Supported in part by the NSF.
}
}
{\bf Theorem:}
There are $10^n$ words in the alphabet $\{3,-2\}$ of length
$5n$, sum $0$, and such that
every factor that sums to $0$ and that starts with a $3$ may not
be immediately followed by a $-2$.
{\bf Proof:}
{\bf 1.} Download Maple package {\tt TEN} from
{\eighttt http://www.math.rutgers.edu/\~{}zeilberg/tokhniot/TEN}.
Save it as {\tt TEN}.
{\bf 2.} Go into Maple, and type: {\tt read TEN:}.
{\bf 3.} Let your computer rediscover a (linear) grammar
for these words, by typing
{\tt G:=DiscoverGrammar(3,2,3):}
(if you actually want to see it replace the : by ; ).
{\bf 4.} To prove (rigorously!) that the conjectured grammar $G$ indeed
describes
(unambiguously!) our language, type:
{\tt ProveGrammar32(G,3); } and get the output {\tt true}.
{\bf 5.} To get the weight-enumerator for the language (where the
weight of a word $w$ is $x^{length(w)}$), type
{\tt GFgrammar(G,x); }
and get the output $1/(1-10x^5)$. \halmos\ ({\bf endproof})
\halmos\ ({\bf endpaper})
{\bf Appendix: TEN Remarks for Human Readers}
{\bf 1.} The Theorem was conjectured by Nick Loehr and Greg Warrington,
in a more general setting,
where $3$ and $-2$ are replaced by general relatively-prime positive
and negative integers, $a$ and $-b$, $5n$ is replaced by $(a+b)n$,
and $10^n$ is replaced by ${{a+b} \choose {a}}^n$. The general
case is still open. Greatly inspired by our proof,
Loehr and Warrington, together with Bruce Sagan,
found a computer-free proof of our theorem. They then extended
their approach to prove it for $b=2$ and all odd $a$.
This will appear in their forthcoming paper
{\it ``A Human Proof for a Generalization of Shalosh B. Ekhad's $10^n$
Lattice Paths Theorem.''}
We wish to acknowledge stimulating discussions with these three humans,
and of course we thank Nick and Greg for conjecturing such a beautiful
result in the first place, and Bruce for telling
Vince, who told Doron, who told Shalosh.
{\bf 2.} The Maple package {\tt TEN} that
(automatically!!)~discovered the grammar, and then
(automatically!!!)~proved its correctness, and then
(automatically!)~computed the weight-enumerator, was
written by VV and DZ. It was executed by SBE.
{\bf 3.} For a blow-by-blow description of how the
grammar was {\it discovered}, type
{\tt G:=DiscoverGrammarVerbose(3,2,3):} .
(The output file may be viewed/downloaded at
{\eighttt http://www.math.rutgers.edu/\~{}zeilberg/tokhniot/oTENdgv}.)
{\bf 4.} People with no access to Maple may view the output
at \hfill\break
{\eighttt http://www.math.rutgers.edu/\~{}zeilberg/tokhniot/oTEN32t}, \hfill\break
{\eighttt http://www.math.rutgers.edu/\~{}zeilberg/tokhniot/oTEN32v}, \hfill\break
and {\eighttt http://www.math.rutgers.edu/\~{}zeilberg/tokhniot/oTEN32vv}
for the terse, verbose, and very verbose versions.
{\bf 5.} The best way to understand the {\it heuristics} behind the
{\bf act of discovery}
(of the linear grammar for the language of the theorem)
and the {\it logic} behind the {\bf act of verification} (proving
rigorously
that the empirically-conjectured grammar is indeed correct) is to
carefully read the
{\bf Maple source-code}, generously made available by the authors, free
of charge,
even though the same {\bf methodology} is very likely to solve other
problems.
There are ample comments, and readers are encouraged to experiment with
{\tt TEN}
themselves. A nice exercise would be to type {\tt
DiscoverGrammar(1,1,3);}
for the grammar of the language of zero-sum words in $\{-1,1\}$ that
avoid
factors of the form $1[-1](-1)$, where $[-1]$ denotes a word that sums
up to $-1$.
Then prove its validity by human means.
{\bf 6.} What if you don't know Maple well enough to follow someone
else's code?
Then go and learn Maple! It would be time much better spent than reading
esoteric papers like this one.
{\bf 7.} Having said that, as a concession to Maple-illiterate people,
let us briefly describe the methodology of {\bf discovery}, to be
followed by a description of the methodology of {\bf proof}.
Procedure {\tt Corpus} first generates all the words of our language
up to
a specified length. For any language $L$ in the alphabet $\{a,-b\}$,
and any
pair of words in that alphabet (not necessarily in $L$),
$[w_1,w_2]$, let $L(w_1,w_2)$ be the subset of $L$ consisting
of those words of the form $w_1uw_2$ for some word $u$.
We want to construct a binary {\it family tree}, rooted at
$L=L(\phi,\phi)$,
whose vertices are
pairs $[w_1,w_2]$ that stand for $L(w_1,w_2)$.
It may happen that $L(w_1,w_2)$ is {\bf empty}, i.e.~$L$ has
no words of the form $w_1uw_2$.
It may also happen that such an $L(w_1,w_2)$ is a {\bf clone} of
another $L(w'_1,w'_2)$ , i.e.
$$
\{ v \, \vert \, w_1 v w_2 \in L \}=\{ v \, \vert \, w'_1 v w'_2 \in L
\} \quad ,
$$
where $length(w'_1)+length(w'_2) 0$;\cr
\quad & \quad \cr
\displaystyle\bigcup_{i=1}^{b} \,\, [-i+b](-b)[A+i],
& if $A<0$.\cr}
\eqno(WordRecurrence)
$$
Indeed any word that sums to $A>0$ must have its {\bf shortest} prefix
whose
sum is positive, the last letter of that prefix being, necessarily, $a$
(or else it wouldn't be the shortest), and the sum of that prefix
(by `continuity'!) must be between $1$ and $a$
(inclusive). Analogously, for $A<0$.
By iterating these recurrences it is easily seen
that each word $[A]$ can be written as one of several {\it
factorizations}
featuring the letters $a$ and $-b$ and the {\bf fundamental factors}
$[0],[1], \dots, [b-1]$.
We can even apply $(WordRecurrence)$ to these, but then we'll
get `self-referential' expressions, i.e.~ways of expressing them in
terms of
themselves (and the actual letters $a$ and $-b$) as a kind of
`Chomskian' grammar.
Whenever we have to prove emptyness or cloneship, we have to prove
that a certain set of words doesn't exist. Like in 4CT or any
{\it reducto} proof (all the way back to $\sqrt{2} \not \in Q$), if the
set
was not empty, there would be a {\bf minimal counterexample}.
So it suffices to prove that minimal counterexamples do not exist.
Note that a minimal counterexample (in our business) can never have
a {\it proper} zero-factor (removing a zero-factor from a good word
obviously results in another good word).
So if we are in the lookout for minimal
counterexamples, we can considerably reduce the many options that an
$[A]$ word can
have, by discarding those factorizations in the
enlarged (`meta-') alphabet $\{a,-b,[1],[2], \dots, [b-1]\}$ that
contain a zero-sum proper factor.
Of course we also kick out any such meta-word that contains a mishap,
i.e.~a factor of the form $a[-a](-b)$.
If there are any survivors left after the first purge, we can replace
$[1], \dots, [b-1]$ by their self-referential expressions
getting longer `meta-words', and once again
discard all those that contain mishaps and all those that
contain a zero-sum proper factor. If all goes well, nothing
will be left after finitely many purges.
For the $\{3,-2\}$ case three purges sufficed to prove every
instance of emptyness or cloneship.
Let's explicate the above for our case of interest, $a=3$, $b=2$.
There is only one `meta-letter', [1], and we have, according to {\tt
TEN}
(but this is so simple that even you can do it!)
$$
[1]=\{[3, -2], [-2, 3], [-2, [1], 3, [1], -2]\} \quad,
$$
which means that every word in the alphabet $\{3, -2\}$
with no zero-sum-factors and no mishaps and whose sum is $1$,
is either the two-letter word $(3)(-2)$ or the two-letter
word $(-2)3$ or else can be written as
$(-2)w_13w_2(-2)$, where $w_1,w_2$ are zero-sum-free and mishap-free
words
whose sum is $1$ on their own right.
We also have:
$$
[-1]=\{[-2, [1]], [[1], -2]\} \quad,
$$
stating that any mishap-free and zero-factor-free
word in $\{3,-2\}$ that sums up to $-1$ may be written
as $(-2)w_1$ or $w_1(-2)$ where $w_1$ is a such a good word
that adds up to $1$.
You are welcome to decipher the following lemmas that
Shalosh discovered and proved.
$$
[-2]=\{[-2], [[1], -2, -2, [1]]\} \quad ,
$$
$$
[2]=\{[3, -2, [1]], [3, [1], -2], [-2, 3, [1]], [-2, [1], 3], [[1], -2,
3]\} \quad ,
$$
$$
[3]=\{[3], [-2, [1], 3, [1]], [[1], -2, 3, [1]], [-2, 3, 3, -2, [1]],
[-2, 3, 3, [1], -2], [-2, 3, -2, 3, [1]]\} \quad .
$$
{\bf 9.} The grammar is especially simple for the case $b=1$.
If $A_a(n)$ is the set of good words in $\{a,-1\}$ we have
(here $\1$ stands for $-1$)
$$
A_a(n)=A_a(n-1) \, a\, \1^a \,\, \cup \,\,
\1\,A_a(n-1)\, a\, \1^{a-1} \, \cup \,
\1\,\1A_a(n-1)a\,\1^{a-2} \, \cup \, \dots \, \cup \,
\1^a\,A_a(n-1)\,a \quad ,
$$
immediately implying that $\vert A_a(n) \vert =(a+1)^n$.
{\bf 10.} ``{\bf Mr. Watson, come here. I want you!}''
While grammatically correct, this sentence is not quite Shakespeare.
Its great significance is the {\bf way} it was uttered, via
the telephone, by Alexander Graham Bell. Analogously, while our proof
is definitely closer to Gauss than Bell's sentence is to Shakespeare,
its main significance, if we do say so ourselves, is in the
{\bf way} that it was discovered, and especially the {\bf way} that
it was {\bf proved}, all by computer! The role of the humans (VV and DZ)
is no longer that of {\it athlete}, but that of {\it coach}, no longer
{\it prover} but {\it programmer}, or if you wish, {\it meta-prover}.
We believe that this will be {\bf the way to go} sooner than you
think! Amen.
\end