Automatic partition identities

We encode certain sets of partitions by regular languages of boundary words, so that their generating functions become rational series in the quantum plane $RU=qUR$. An equality between two partition counts is certified by writing the difference of their series as $(1-U)a+b(1-R)$, with $a,b$ converging $q$-adically. We show that $a,b$ may be chosen as solutions of finite holonomic systems of $q$-difference equations computed from the automata, and describe finite certificates of their convergence, together with bounded searches for such certificates; the searches need not succeed, but a false identity is always detected. As an application, we prove the three-row, level-two case of Primc's conjecture, which equates counts of coloured partitions subject to local multiplicity conditions with counts of coloured partitions whose parts lie in prescribed residue classes modulo eight.