Term Coding: An Entropic Framework for Extremal Combinatorics and the Guessing--Number Sandwich Theorem

Abstract

Classical existence problems in extremal combinatorics ask whether finite operations can satisfy prescribed identities universally. Term Coding replaces this yes-or-no question by a graded one: for a finite system $\Gamma$, the maximum code size $S_n(\Gamma )$ is the largest number of satisfying assignments attainable on an $n$-element alphabet. We prove that normalisation and diversification associate $\Gamma$ with a labelled guessing game of guessing number $\alpha$ and give finite-alphabet sandwich bounds. Consequently, ${\log }_n{S}_n(\Gamma )=\alpha +o(1)$. Entropy and polymatroid inequalities provide systematic upper bounds. Examples include a five-cycle with exponent $5/2$, self-orthogonal Latin squares, and presentation-dependent exponents for universally equivalent identity systems. All theorems, lemmas and propositions in this paper have been machine-checked in the Lean 4 proof assistant; the development is available at https://github.com/SR123/term-coding-lean.