Papers With

← All papers
First page of Embedding Finite Functions into Low-Degree Polynomial Functions over Commutative Rings

Embedding Finite Functions into Low-Degree Polynomial Functions over Commutative Rings

Roman Bacik

math.CO Jun 8, 2026 · v1
formalization combinatorics algebra
Read PDF arXiv abstract Code
TL;DR
Proves three embedding results for finite functions, all verified in Lean 4 with Mathlib.
Abstract
A function $f \colon X^k \to X$ on a finite set embeds into a polynomial of total degree $d$ over a commutative ring $R$ if there is an injection $j \colon X \to R$ and a polynomial $g$ of total degree at most $d$ with $j \circ f = g \circ j^k$, where $j^k$ applies $j$ in each coordinate. These are the transition functions of $k$-neighbour cellular automata, and the injection $j$ is an enlargement of the alphabet that preserves the transitions. We prove three results, all verified in Lean~4 with Mathlib~\cite{bacik2026finbin}. Every unary function $f \colon X \to X$ embeds into a polynomial of total degree $1$. Every binary Kronecker delta embeds into a polynomial of total degree $4$. For every $d$ there is a binary function that does not embed into any polynomial of total degree $d$.
Problem

Representing finite functions as low-degree polynomials over commutative rings is relevant for algebraic modeling of cellular automata, but tight degree bounds for such embeddings were unknown, especially for binary functions.

Approach

The authors prove three results about polynomial embeddings of finite functions, all verified in Lean 4 with Mathlib. They show every unary function embeds in degree 1 via a Chinese Remainder Theorem construction, every binary Kronecker delta embeds in degree 4 via explicit modular-arithmetic constructions with degree-preserving reductions, and for every degree d there exists a binary function (the inversion indicator on Z/p) that cannot embed in any polynomial of degree d over any commutative ring.

Results

Every unary function on a finite set embeds into a linear polynomial. Every binary Kronecker delta embeds in degree 4. For every d, a binary function exists that requires degree greater than d. All three results are machine-checked in Lean 4.