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 $Γ$, the maximum code size $S_n(Γ)$ is the largest number of satisfying assignments attainable on an $n$-element alphabet. We prove that normalisation and diversification associate $Γ$ with a labelled guessing game of guessing number $α$ and give finite-alphabet sandwich bounds. Consequently, $\log_n S_n(Γ)=α+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.

翻译：暂无翻译