Term Coding: An Entropic Framework for Extremal Combinatorics and the Guessing–Number Sandwich Theorem
Søren Riis
cs.IT
Jan 23, 2026 · v2
TL;DR
All theorems, lemmas, propositions and worked examples are machine-checked in Lean 4 with Mathlib, with a public repository and Zenodo archive.
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 $Γ$, 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.
Problem
Classical extremal combinatorics asks whether finite operations can satisfy universal identities everywhere. Term Coding replaces this yes-or-no question with a graded one: the maximum number S_n(Γ) of satisfying assignments attainable on an n-element alphabet.
Approach
Normalisation adds auxiliary variables, and diversification reduces a term system to a labelled guessing game on a dependency digraph. This gives finite-alphabet sandwich bounds relating S_n(Γ) to the guessing-game winning counts. Entropy and polymatroid inequalities supply systematic upper bounds. The whole development is formalised in Lean 4.26.0 with Mathlib, and every declaration depends only on Lean's standard axioms.
Results
The sandwich theorem yields log_n S_n(Γ) = α + o(1), where α is the guessing number. Case studies include a five-cycle instance with exponent 5/2, self-orthogonal Latin squares, and presentation-dependent exponents for universally equivalent identity systems.
