Finite arithmetic kernels and finite output automata

Abstract

Over every finite output alphabet, a sequence has finite arithmetic kernel exactly when a finite DFAO computes it on every least-significant-digit-first representation.

The characterization is Eilenberg’s theorem. Natural indices include zero. A digit word is read least significant digit first; its final digits are the high-order digits.

Definition 1.1 (Value of a digit word).

$$\forall k\in \mathrm{Nat},\forall ds\in \mathrm{List}\left(\mathrm{Fin}\left(k\right)\right),\mathrm{Value}\left(k,ds\right)=\mathrm{foldr}\left(ds,(d:\mathrm{Fin}\left(k\right)\mapsto (v:\mathrm{Nat}\mapsto \mathrm{val}\left(d\right)+k\cdot v)),0\right)$$

Formalization. D5/S0/Automata/FiniteKernelDFAO.baseWordValueLSD (✓ std3).

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

For every natural base k and every finite word ds over Fin k, Value(k,ds) is its least-significant-digit-first value. The right fold starts at zero. Thus the empty word and every all-zero word represent zero; appending high-order zeros preserves value. The notation val(d) denotes the natural value of a digit d.

Definition 1.2 (Correctness on every representation).

$$\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(B\right)]\forall k\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to B),(\mathrm{Machine}\left(k,a\right)⟺2\le k\wedge \left(\exists q\in \mathrm{Nat},0<q\wedge \left(\exists s\in \mathrm{Fin}\left(q\right),\exists t\in (\mathrm{Fin}\left(q\right)\to (\mathrm{Fin}\left(k\right)\to \mathrm{Fin}\left(q\right))),\exists o\in (\mathrm{Fin}\left(q\right)\to B),\forall n\in \mathrm{Nat},\forall ds\in \mathrm{List}\left(\mathrm{Fin}\left(k\right)\right),\mathrm{Value}\left(k,ds\right)=n\Rightarrow o\left(\mathrm{Fold}\left(ds,t,s\right)\right)=a\left(n\right)\right)\right))$$

Formalization. D5/S0/Automata/FiniteKernelDFAO.IsKAutomaticSequence (✓ std3).

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

For a finite output type B, Machine(k,a) requires k at least two and a positive natural state count q, an initial state s, a total transition table t and an output map o. Fold(ds,t,s) is List.foldl: the leftmost, least significant digit is read first. Correctness quantifies over every natural n and every word of value n, including empty and padded representations. Zero-digit transitions are constrained by this output-invariance condition.

Definition 1.3 (Arithmetic kernel).

$$\forall D\in {\mathrm{Type}}^{\ast },\forall k\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to D),\mathrm{Kernel}\left(k,a\right)=\{b:(\mathrm{Nat}\to D)\mid \exists e\in \mathrm{Nat},\exists r\in \mathrm{Nat},r<k^e\wedge b=(n:\mathrm{Nat}\mapsto a\left(k^e\cdot n+r\right))\}$$

Formalization. D5/S0/Automata/FiniteKernelDFAO.kKernel (✓ std3).

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

For any output type D in any universe, Kernel(k,a) consists of the decimations n ↦ a(k^e n+r), with natural exponent e and residue r less than k^e. No finiteness or additive structure on D is needed to define this set.

Definition 1.4 (Finite-kernel automaticity).

$$\forall D\in {\mathrm{Type}}^{\ast },\forall k\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to D),(\mathrm{Automatic}\left(k,a\right)⟺2\le k\wedge \mathrm{Finite}\left(\mathrm{Kernel}\left(k,a\right)\right))$$

Formalization. D5/S0/Automata/FiniteKernelDFAO.IsKAutomatic (✓ std3).

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

Automatic(k,a) is the conjunction of k at least two and finiteness of the type of members of Kernel(k,a). This definition is available for arbitrary output types; the equivalence below holds for finite output types B : Type.

Theorem 1.5 (One-digit kernel closure).

$$\forall D\in {\mathrm{Type}}^{\ast },\forall q\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to D),\forall b\in (\mathrm{Nat}\to D),\forall j\in \mathrm{Nat},b\in \mathrm{Kernel}\left(q,a\right)\Rightarrow \left(j<q\Rightarrow (n:\mathrm{Nat}\mapsto b\left(q\cdot n+j\right))\in \mathrm{Kernel}\left(q,a\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Automata/FiniteKernelDFAO.chr_kernel_lam_mem (✓ std3). ∎

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

Decimating a kernel element b by a digit j less than q gives another member of the same q-kernel. The construction uses exponent e+1 and residue q^e j+R from a representation of b. This closure supplies the transition of the kernel-state machine.

Theorem 1.6 (The original sequence is a kernel state).

$$\forall D\in {\mathrm{Type}}^{\ast },\forall q\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to D),a\in \mathrm{Kernel}\left(q,a\right)$$

Proof. Machine-checked in Lean as D5/S0/Automata/FiniteKernelDFAO.chr_self_mem_kernel (✓ std3). ∎

Citation. ATLAS contributors; Meta Platforms, Inc. and affiliates (2026). Automatic sequences: finite kernels and the Eilenberg bridge. URL: https://github.com/facebookresearch/atlas-lean/blob/8c9ac8ce7d2febf34a232009e1e1b0a350174591/MathlibExt/Combinatorics/Words/Automatic.lean.

Commentary.

The exponent zero and residue zero put every sequence a in its own q-kernel, even for bases zero and one. For the final theorem this state provides the initial state and certifies that the finite state count is positive.

Theorem 1.7 (Eilenberg’s finite-kernel equivalence).

$$\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(B\right)]\forall k\in \mathrm{Nat},\forall a\in (\mathrm{Nat}\to B),(2\le k\wedge \mathrm{Finite}\left(\mathrm{Kernel}\left(k,a\right)\right)⟺2\le k\wedge \left(\exists q\in \mathrm{Nat},0<q\wedge \left(\exists s\in \mathrm{Fin}\left(q\right),\exists t\in (\mathrm{Fin}\left(q\right)\to (\mathrm{Fin}\left(k\right)\to \mathrm{Fin}\left(q\right))),\exists o\in (\mathrm{Fin}\left(q\right)\to B),\forall n\in \mathrm{Nat},\forall ds\in \mathrm{List}\left(\mathrm{Fin}\left(k\right)\right),\mathrm{Value}\left(k,ds\right)=n\Rightarrow o\left(\mathrm{Fold}\left(ds,t,s\right)\right)=a\left(n\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S0/Automata/FiniteKernelDFAO.isKAutomatic_iff_isKAutomaticSequence (✓ std3). ∎

Citation. Boris Adamczewski and Jason P. Bell (2012). On vanishing coefficients of algebraic power series over fields of positive characteristic. URL: https://arxiv.org/abs/1205.4091v1.

Commentary.

For every finite B : Type, every natural k and every sequence a : Nat → B, Automatic(k,a) is equivalent to Machine(k,a). Both sides contain the conjunct 2 ≤ k. In the forward direction the states are exactly the kernel elements, relabeled by an equivalence with Fin q; the initial state is a, a digit acts by decimation, and the output is evaluation at zero. The inductive chr_fold_val invariant identifies the reached state with n ↦ b(k^length(ds) n+Value(k,ds)). In the reverse direction, fix a representing word for each n. A kernel element with exponent e and residue r is realized by the state reached after a representing word for r of length exactly e. Padding by high-order zeros supplies that exact length. Concatenating this word with a representing word for n yields k^e n+r, so all kernel elements lie in the finite image of the q states.

References

• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.IsKAutomatic
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.IsKAutomaticSequence
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.baseWordValueLSD
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.chr_kernel_lam_mem
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.chr_self_mem_kernel
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.isKAutomatic_iff_isKAutomaticSequence
• Truth anchor: D5/S0/Automata/FiniteKernelDFAO.kKernel