The Quasi-Holonomic Ansatz and Restricted Lattice Walks

TL;DR

This paper introduces a novel, elegant proof technique for restricted lattice walks that simplifies previous complex proofs, using a quasi-holonomic approach supported by computer algebra, resulting in a concise, conceptually one-line proof.

Contribution

The paper presents a new quasi-holonomic ansatz and proof method for enumerating restricted lattice walks, offering a simpler and more elegant alternative to existing proofs.

Findings

A new quasi-holonomic approach to lattice walk enumeration

An elegant, conceptually one-line proof of a known enumeration fact

Computer-assisted derivation of a large recurrence relation

Abstract

The great enumerator Germain Kreweras empirically discovered this intriguing fact, and then needed lots of pages[K], and lots of human ingenuity, to prove it. Other great enumerators, for example, Heinrich Niederhausen[N], Ira Gessel[G1], and Mireille Bousquet-M\'elou[B], found other ingenious, ``simpler'' proofs. Yet none of them is as simple as ours! Our proof (with the generous help of our faithful computers) is ``ugly'' in the traditional sense, since it would be painful for a lowly human to follow all the steps. But according to our humble aesthetic taste, this proof is much more elegant, since it is (conceptually) one-line. So what if that line is rather long (a huge partial-recurrence equation satisfied by the general counting function), it occupies less storage than a very low-resolution photograph.