Term coding / paper & proof
PDF ↗

Interactive edition · 12 September 2026

One Unit Separates Polynomial Time
from Undecidability in Term Coding

Søren Riis

How this paper developed

Author’s note · Søren Riis

The ideas behind this paper took shape during my research visit to the Institut Henri Poincaré in Paris in early 2016, during the programme Nexus of Information and Computation Theories. I began to see how term coding could bring several mathematical questions into a common framework. One possibility particularly appealed to me: a seemingly small change in a decision problem might produce a dramatic jump from polynomial-time decidability to undecidability.

These ideas developed into the outline of my omnibus paper. But the undecidability argument for what I called the square-matrix decision problem remained troublesome. For a long time, I thought a reduction from a known undecidable problem should settle it. Repeatedly, however, I reached a step I could not justify. The undecidability claim in the earlier omnibus version ultimately had to be withdrawn.

I came to regard the problem as considerably harder than I had first imagined. I subsequently explored it through extended work with AI assistants, first Sol Pro in Codex and then Astra Pro in Codex, without resolving the central difficulty.

The decisive conceptual changes came from me. I proposed reformulating the problem by allowing explicit disequality constraints. I also recognised that we needed to consider a family of values of k, rather than concentrating solely on k = 2. These were crucial human contributions: both the modified formulation and the recognition that the parameter needed to vary originated in my own thinking. The subsequent mathematical development proceeded interactively with AI assistance.

These changes led to a closely related problem for which the dramatic complexity gap could be proved. They recovered the mathematical phenomenon I had hoped to capture, while leaving the original square problem open.

For me, the appeal of the result is partly aesthetic: a minute change in the threshold separates polynomial-time decidability from undecidability. Its history also matters to me. The finished proof conceals years of uncertainty, unsuccessful approaches, and the eventual decision to ask a slightly different question.

Paris visit: programme · contemporary report (p. 23).

Read the paper. Open any paragraph to follow the argument.
Continue into the exact Lean statement, proof steps and foundations.

Download paperDownload Claude’s Lean sourceVerification recordBuild & audit evidence
Contents · all eight sections

Abstract

Term coding provides a common algebraic framework for network coding, index coding and problems in extremal combinatorics. We exhibit a decision problem in which lowering an output threshold by just one changes the complexity from polynomial time to undecidability: no algorithm then halts with the correct answer on every input. The problem concerns dispersion, the maximum number of distinct output tuples obtainable by interpreting the function symbols in a tuple of terms on a finite alphabet. We restrict inputs by inequalities between terms and ask whether a given instance meets a prescribed output threshold for some alphabet size at least two. Both thresholds are considered on the same class of instances. A machine-checked Lean development and an interactive presentation of the paper accompany this work (GitHub: https://github.com/SR123/term-coding-disequality-lean; DOI: 10.5281/zenodo.22727895); Section 8 specifies its external input and verification limits.

1. Two decision problems with adjacent thresholds

An expression such as f(g(x),y)f(g(x),y) becomes a function of x,yx,y once a set AA and functions g:A→Ag:A\to A and f:A2→Af:A^2\to A are chosen. We call such expressions terms, and the choice of functions an interpretation. Every occurrence of a symbol uses the same function: for example, g(g(x))g(g(x)) means that this function is applied twice. A tuple of terms in variables x1,…,xmx_1,\ldots,x_m defines a map from AmA^m to ArA^r, where rr is the number of terms in the tuple. We restrict its domain by requiring finitely many inequalities u≠vu\ne v between terms. Such inequalities are also called disequalities or tests.
An instance Γ\Gamma specifies the variables, function symbols and their arities, output terms, and tests. For each n≥1n\ge1, let DΓ(n)D_\Gamma(n) be the maximum number of distinct output tuples obtained from inputs satisfying all tests, as the interpreting functions on [n]={0,…,n−1}[n]=\{0,\ldots,n-1\} vary. This maximum is called the dispersion. It counts output tuples, not satisfying input tuples: different inputs can give the same output. The finite set on which the functions act is also called the alphabet. The instance specifies neither its size nor any of the interpreting functions. Section 2 gives the formal definitions.
Let C\mathcal C consist of all instances with a finite set XX of variables containing distinct variables x,yx,y, output tuple (x,y,t3,…,tr),r≥2, (x,y,t_3,\ldots,t_r),\qquad r\ge2, and a finite list of tests that includes x≠yx\ne y. The remaining output terms may use any variables in XX and may repeat. All variables, symbols, terms and tests are explicitly listed in the input. The class C\mathcal C does not depend on the integer kk used below; in particular, the numbers of variables and outputs need not equal kk.
For k≥2k\ge2, put bk(n)=nk−nk−1=nk−1(n−1). b_k(n)=n^k-n^{k-1}=n^{k-1}(n-1). This is the number of kk-tuples in [n]k[n]^k whose first two coordinates differ. We compare two questions about an input Γ∈C\Gamma\in\mathcal C: does DΓ(n)≥bk(n)D_\Gamma(n)\ge b_k(n) hold for some n≥2n\ge2, and does DΓ(n)≥bk(n)+1D_\Gamma(n)\ge b_k(n)+1 hold for some n≥2n\ge2? Both quantify over the same possible sizes of the finite set. The second question asks for just one more output tuple, but admits a polynomial-time algorithm, whereas the first is undecidable.
The algorithm uses a graph determined by the terms. Its vertices are the distinct subterms, together with all declared variables; an edge runs from an immediate argument to the term containing it. This is a directed acyclic graph. A term cut is a set of vertices meeting every directed path from a variable to an output term. Paths of length zero are included, and a cut may contain variables or output terms. Let ρΓ\rho_\Gamma be the minimum size of such a cut. Every cut for an instance in C\mathcal C contains x,yx,y, since each is both a variable and an output. Thus ρΓ≥2\rho_\Gamma\ge2.
Theorem 1.1. The one-unit difference in complexity. For every fixed integer k≥2k\ge2, the following decision problems on C\mathcal C have the indicated complexities: input: Γ∈C∃n≥2: DΓ(n)≥bk(n)undecidable,input: Γ∈C∃n≥2: DΓ(n)≥bk(n)+1polynomial time. \begin{array}{lll} \text{input: }\Gamma\in\mathcal C& \exists n\ge2:\ D_\Gamma(n)\ge b_k(n)&\text{undecidable},\\[2pt] \text{input: }\Gamma\in\mathcal C& \exists n\ge2:\ D_\Gamma(n)\ge b_k(n)+1&\text{polynomial time}. \end{array} The second answer is yes if and only if no test has syntactically identical sides and ρΓ≥k+1\rho_\Gamma\ge k+1. This criterion can also be decided in polynomial time when k≥2k\ge2 is part of the input, written in binary. If it holds, and ss is the number of distinct subterms in the outputs and tests together with all declared variables, then DΓ(n)≥⌊n/s⌋k+1(n≥s). D_\Gamma(n)\ge\lfloor n/s\rfloor^{k+1}\quad(n\ge s). In particular, whenever the criterion holds, the strict threshold is attained at the alphabet size n0=sk+1n_0=s^{k+1}. For every fixed kk, the first problem remains undecidable on the subclass with ρΓ=k\rho_\Gamma=k, where DΓ(n)≤bk(n)D_\Gamma(n)\le b_k(n) for all n≥2n\ge2. There is no total computable function BB such that every positive instance in this subclass, of input length NN, has a size nn with 2≤n≤B(N)2\le n\le B(N) and DΓ(n)=bk(n)D_\Gamma(n)=b_k(n).
We call the two inequalities in the theorem the non-strict and strict thresholds, respectively: since DΓ(n)D_\Gamma(n) is an integer, the second is equivalent to DΓ(n)>bk(n)D_\Gamma(n)>b_k(n). For fixed kk, the sufficient size sk+1s^{k+1} is polynomial in ss. When kk varies, its value need not be polynomial, but its binary representation is still short. On a positive strict instance, k+1≤ρΓ≤sk+1\le\rho_\Gamma\le s, so it has at most s(⌊log⁡2s⌋+1)s(\lfloor\log_2 s\rfloor+1) bits. This bounds the length of the integer specifying a sufficient alphabet size; it does not assert that all entries of functions of arbitrary arity can be listed in polynomial time.
Why all output pairs force identities. For outputs (x,y)(x,y), the test x≠yx\ne y allows at most n(n−1)n(n-1) outputs. Achieving this number means that every pair (a,b)(a,b) with a≠ba\ne b satisfies every test. In particular, if a further test is F(x)≠yF(x)\ne y, then F(a)=aF(a)=a for every aa: otherwise the pair (a,F(a))(a,F(a)) would fail. We refer to equality with this upper bound as saturation. Applying this observation to terms expressing inverse and relator laws forces them to hold on the whole finite set. Section 5 uses it to encode the following undecidable problem for one fixed finitely presented group: given a word, does it have nonidentity image in some finite quotient? The external group-theoretic result is [1, Theorem 2.1]. Only the term representing the input word varies; the unary symbols and the number of tests are fixed. Adding k−2k-2 new variables as further outputs, with no tests involving them, multiplies the image size by nk−2n^{k-2} and proves the other degrees.
The cut bound and earlier routing work. Riis and Gadouleau [6] proved that ordinary dispersion, without tests, has growth exponent equal to the minimum term cut. Their lower bound transmits independent values along disjoint paths in the term graph. Each transmitted value is accompanied by a label identifying its subterm, so that different uses of a symbol can be handled by one function. This construction is called routing. Section 3 shows that the same labels satisfy every test whose sides are syntactically different. It also proves the sharper upper bound DΓ(n)≤nρΓ−nρΓ−1(Γ∈C), D_\Gamma(n)\le n^{\rho_\Gamma}-n^{\rho_\Gamma-1} \qquad(\Gamma\in\mathcal C), because every cut contains the output variables x,yx,y, whose values must differ. These two bounds give the strict decision criterion. The reduction uses the new identity-forcing argument above; it does not follow from the earlier asymptotic theorem.
Approaching the upper bound by explicit functions. For the two-variable instance associated to a fixed presentation GG and a word ww, write DG,w(n)D_{G,w}(n) for the dispersion. For every nonempty word ww, Section 7 constructs functions satisfying n(n−1)−Mn≤DG,w(n)≤n(n−1)(n>∣w∣), n(n-1)-Mn\le D_{G,w}(n)\le n(n-1)\qquad(n>|w|), where ∣w∣|w| counts the letters as written and MM depends only on the presentation. Given ww and a positive rational ε\varepsilon, the construction computes an integer n≥2n\ge2 and unary functions for which the allowed output image contains at least (1−ε)n(n−1)(1-\varepsilon)n(n-1) pairs. It works even for words for which equality with n(n−1)n(n-1) is impossible at every size. Thus arbitrarily accurate proportions of this upper bound, with computable witnesses, do not decide whether the bound can be reached. The reason is concrete: each failed identity at a point excludes at most one further second coordinate. At most MnMn pairs are lost, a vanishing proportion of n(n−1)n(n-1), whereas losing no pair forces every identity to hold everywhere. The approximate constructions need not satisfy the group laws.
Example 1.2. Both answers occur at every degree. Fix k≥2k\ge2, variables x1,…,xk+1x_1,\ldots,x_{k+1}, and only the test x1≠x2x_1\ne x_2. The output tuple (x1,…,xk+1)(x_1,\ldots,x_{k+1}) has bk+1(n)b_{k+1}(n) distinct outputs and exceeds bk(n)+1b_k(n)+1 already at n=2n=2. With the same variables, test and number of output coordinates, the tuple (x1,…,xk,x1)(x_1,\ldots,x_k,x_1) instead has exactly bk(n)b_k(n) outputs. It gives a no answer to the strict question and a yes answer to the non-strict question. Adding the deliberately impossible test x1≠x1x_1\ne x_1 excludes every assignment and gives DΓ(n)=0D_\Gamma(n)=0, so both questions have answer “no”. For k=2k=2, the first two examples are (x,y,z)(x,y,z) with D(n)=n2(n−1)D(n)=n^2(n-1) and (x,y,x)(x,y,x) with D(n)=n(n−1)D(n)=n(n-1).
The strict positive instances form a subset of the non-strict positive instances; there is no contradiction in the subset being easier to recognise. Also bk(n)+1<bk+1(n)b_k(n)+1<b_{k+1}(n) for every n≥2n\ge2. As kk increases, the undecidable thresholds therefore alternate with the polynomial-time thresholds. The input class remains C\mathcal C throughout.
Correction to the earlier omnibus. This paper is intended to replace Term Coding for Extremal Combinatorics: Dispersion and Complexity Dichotomies, arXiv:2504.16265 [3]. That work has been divided into focused papers. The entropic framework and guessing-number sandwich theorem are developed in [4]; ordinary dispersion and its exact and asymptotic decision problems are studied in [5]. Versions 1–3 of the earlier omnibus asserted undecidability of finite square term bijectivity, the existence of an interpretation making a tuple of kk terms in kk variables a bijection on AkA^k for some finite AA with ∣A∣≥2|A|\ge2. The proposed Horn-clause reduction in Appendix A of v1 did not establish the required forcing properties, and the machine-simulation sketches in Section 7.1 of v2 and v3 did not establish the required reduction. The undecidability assertion and the unconditional pure-equation complexity conclusions depending on it are therefore withdrawn. Finite square term bijectivity remains open. The present reduction applies to the stated class with disequality tests and does not establish that earlier assertion.

2. Terms, interpretations, and the output image

Fix a finite nonempty set XX of variables, also called source variables, and a finite signature Σ\Sigma: a set of function symbols with a specified nonnegative integer arity for each symbol. Terms are finite rooted expressions over XX and Σ\Sigma, with ordered arguments. A symbol of arity zero is a constant symbol. Syntactic equality means literal equality of expressions using the same symbol and variable names; no algebraic identities or cancellation rules are imposed. An interpretation II on a nonempty set AA assigns one function If:Aarity⁡(f)→AI_f:A^{\operatorname{arity}(f)}\to A to each f∈Σf\in\Sigma. Every such function is defined on its entire domain, with no prescribed values. For an assignment a:X→Aa:X\to A, the value uI(a)u^I(a) of a term is defined recursively. All occurrences of ff use the same IfI_f.
Definition 2.1. An instance Γ\Gamma consists of variables X={x1,…,xm}X=\{x_1,\ldots,x_m\}, a finite signature Σ\Sigma, an output tuple t=(t1,…,tr)\mathbf t=(t_1,\ldots,t_r), and a finite list Δ\Delta of tests u≠vu\ne v between terms over XX and Σ\Sigma. For an interpretation II on a finite nonempty set AA, define CI={a∈Am:uI(a)≠vI(a) for every (u≠v)∈Δ}. C_I=\{a\in A^m:u^I(a)\ne v^I(a) \text{ for every }(u\ne v)\in\Delta\}. The output map is tI(a)=(t1I(a),…,trI(a))\mathbf t^I(a)=(t_1^I(a),\ldots,t_r^I(a)). Its image on the allowed inputs is tI(CI)⊆Ar\mathbf t^I(C_I)\subseteq A^r. For n≥1n\ge1, the dispersion is DΓ(n)=Dn(t,Δ)=max⁡I on [n]∣tI(CI)∣. D_\Gamma(n)=\DD_n(\mathbf t,\Delta) =\max_{I\text{ on }[n]}|\mathbf t^I(C_I)|. The notation Dn(t,Δ)\DD_n(\mathbf t,\Delta) leaves XX and Σ\Sigma implicit.
A bijection between two finite sets transports interpretations and assignments, preserving the number of outputs. Thus only ∣A∣|A| matters. There are finitely many functions of each specified arity on [n][n], so the maximum exists. In particular, DΓ(n)≥hD_\Gamma(n)\ge h means that some interpretation on [n][n] has at least hh distinct outputs.
For outputs (x,y)(x,y) and only the test x≠yx\ne y, the output map is the identity on pairs and has n(n−1)n(n-1) outputs. Input and output counts can differ when other variables are present. For example, with variables x,y,zx,y,z, outputs (x,y,x)(x,y,x) and only the test x≠yx\ne y, there are n2(n−1)n^2(n-1) allowed inputs, but only n(n−1)n(n-1) different outputs: changing zz does not change the output.
Writing nested terms as acyclic equations. One may introduce a new variable for each distinct nonvariable subterm and an equation recording its computation. For example, the output f(g(x),y)f(g(x),y) can be written using z=g(x)z=g(x) and v=f(z,y)v=f(z,y), with output vv. Every assignment to the original variables has a unique extension to the new ones. Replacing terms in outputs and tests by their names therefore preserves the output image. Equal subterms receive the same name, and every use of a symbol still has the same interpretation. These equations merely record evaluation; they add no further equality condition on the original variables. This rewriting is often called flattening.
Finite input descriptions. For the complexity statements, names, arities, variables, output and test lists, and ordered argument lists are explicitly encoded in binary. Integers have canonical self-delimiting encodings, and every list includes its length and all entries. Let NN be the bit length of this description. Terms may be represented by syntax trees or by an acyclic graph listed in topological order, with arguments referring to earlier nodes. In the latter representation, different nodes can still represent the same expression. We identify them by syntax, processing child terms first, without expanding the graph into a potentially exponential tree. Validation and this identification take polynomial time in either representation.
The algorithm rejects invalid references, wrong argument counts, noncanonical integer encodings and trailing data. A declared list length or arity does not justify a long search for absent entries: a parser stops and rejects when the supplied data end. Thus validation is polynomial in the actual input length even for malformed descriptions. For the uniform problem, kk is a separate binary integer and inputs with k<2k<2 are rejected.

3. Image bounds from cuts in the term graph

Let SS contain all distinct subterms of the outputs and tests, together with every declared variable, and put s=∣S∣≥1s=|S|\ge1. On SS, draw an edge from each immediate argument to its parent term. Vertices represent expressions, not separate occurrences of those expressions. Let ρ\rho be the minimum size of a set meeting all directed paths from variables to outputs, including paths of length zero. Repeated output terms designate the same vertex.
Terms occurring only in tests do not change ρ\rho: all ancestors of an output already occur among its subterms. Constant symbols have no incoming edges and start no path from a variable. Unused variables and terms occurring only in tests can enlarge SS without increasing ρ\rho. For example, the outputs (x,y,f(z),g(f(z)))(x,y,f(z),g(f(z))) have ρ=3\rho=3, since the last two terms share f(z)f(z). The cut {x,y,f(z)}\{x,y,f(z)\} has size three; the paths consisting of xx alone, yy alone, and the edge from zz to f(z)f(z) show that no smaller cut is possible.
Theorem 3.1. The term-cut bounds with disequalities. If a test in Δ\Delta has syntactically identical sides, then Dn(t,Δ)=0\DD_n(\mathbf t,\Delta)=0 for every n≥1n\ge1. Otherwise, for every n≥sn\ge s, ⌊n/s⌋ρ≤Dn(t,Δ)≤nρ. \lfloor n/s\rfloor^\rho\le \DD_n(\mathbf t,\Delta)\le n^\rho. For each fixed instance without such a test, Dn=Θ(nρ),lim⁡n→∞log⁡Dnlog⁡n=ρ. \DD_n=\Theta(n^\rho),\qquad \lim_{n\to\infty}\frac{\log\DD_n}{\log n}=\rho. One can check for identical sides and compute ρ\rho in polynomial time in the explicit input length.
Proof. A test u≠uu\ne u cannot be satisfied. For the upper bound, fix an interpretation and a cut KK. The values of its terms determine every output value. Indeed, evaluate an output recursively, stopping whenever a vertex of KK is reached and using its given value. Any other leaf must be a constant: reaching a variable without meeting KK would give a path missed by the cut. Consequently two assignments with the same values at KK have the same output tuple. There are at most n∣K∣n^{|K|} possible tuples of values at KK, and restricting the allowed inputs cannot increase this bound. Take a minimum cut.
For the lower bound, Menger's theorem gives ρ\rho vertex-disjoint paths from variables to outputs. Choose a set BB of size m≥1m\ge1 and use the finite set A=S×BA=S\times B. An element (u,b)(u,b) has a label u∈Su\in S and a value b∈Bb\in B. We construct the functions so that every subterm evaluates with its own label and the values at the chosen path starts are copied along their paths.
For a symbol ff of arity dd, consider arguments ((u1,b1),…,(ud,bd))((u_1,b_1),\ldots,(u_d,b_d)). If v=f(u1,…,ud)v=f(u_1,\ldots,u_d) belongs to SS, let the result have label vv. If a chosen path enters vv through uju_j, set its value to bjb_j; otherwise use a fixed element of BB. Vertex-disjointness makes the chosen predecessor unique. If the predecessor term occurs in several argument positions, select any one of those positions. On the assignments used below they have equal values. For a constant symbol belonging to SS, use the same default value and its own label. All remaining function values may be chosen arbitrarily. These instructions define one function for each symbol: the symbol and the ordered input labels determine the term vv, so different subterms cannot impose conflicting instructions.
Give each source variable its own label. Allow the values at the ρ\rho path starts to vary independently in BB, and fix all other source values. Induction on terms shows that each subterm has its own label. Every test with different sides is therefore satisfied. Along each selected path its starting value is copied to the output, giving mρm^\rho distinct output tuples. Hence Dsm≥mρ\DD_{sm}\ge m^\rho. For a larger set, extend each function arbitrarily while preserving its values on (S×B)d(S\times B)^d. Taking m=⌊n/s⌋m=\lfloor n/s\rfloor proves the lower bound for every n≥sn\ge s.
For n≥2sn\ge2s, ⌊n/s⌋≥n/(2s)\lfloor n/s\rfloor\ge n/(2s), giving the growth and logarithmic limits, also when ρ=0\rho=0. To compute the cut, split each vertex into an entrance and exit joined by an edge of capacity one. Replace each original edge by an edge from the corresponding exit to entrance, of capacity s+1s+1. Attach a new source to all variable entrances and all output exits to a new sink, again with capacity s+1s+1. Cutting all unit edges costs ss, so a minimum cut uses only unit edges. Integral max-flow/min-cut gives both ρ\rho and the vertex-disjoint paths in polynomial time. This is the directed vertex form of Menger's theorem [2].□
Proposition 3.2. The sharper bound when x,yx,y are outputs. For every Γ∈C\Gamma\in\mathcal C and n≥2n\ge2, DΓ(n)≤bρΓ(n)=nρΓ−nρΓ−1. D_\Gamma(n)\le b_{\rho_\Gamma}(n) =n^{\rho_\Gamma}-n^{\rho_\Gamma-1}. For every j≥2j\ge2 the bound is sharp: the tuple of jj distinct variables, with only the test x≠yx\ne y on its first two coordinates, has ρΓ=j\rho_\Gamma=j and DΓ(n)=bj(n)D_\Gamma(n)=b_j(n).
Proof. Every cut KK contains x,yx,y because of their paths of length zero. For a fixed interpretation, the values at KK determine the output tuple, as in Theorem 3.1. On allowed inputs the values at x,yx,y differ, so there are at most n(n−1)n∣K∣−2=b∣K∣(n) n(n-1)n^{|K|-2}=b_{|K|}(n) possible tuples of values at the cut. Choose a minimum cut and maximise over interpretations. In the stated example, every allowed input is a different output, and every one of the jj variables is an output. Thus the cut has size jj and the image has size bj(n)b_j(n).□
Corollary 3.3. Thresholds for all sufficiently large sets. Fix an integer d≥0d\ge0 and a function hdh_d such that nd<hd(n)n^d<h_d(n) for all sufficiently large nn, and hd(n)=o(nd+1)h_d(n)=o(n^{d+1}). Given an instance, one can decide in polynomial time whether Dn≥hd(n)\DD_n\ge h_d(n) for all sufficiently large nn. The answer is yes exactly when no test has syntactically identical sides and ρ≥d+1\rho\ge d+1.
Proof. An identical-side test makes every image empty. Otherwise the lower bound is at least a positive constant, depending on the instance, times nρn^\rho for all sufficiently large nn. If ρ≥d+1\rho\ge d+1, this eventually exceeds hd(n)h_d(n). If ρ≤d\rho\le d, the upper bound Dn≤nd<hd(n)\DD_n\le n^d<h_d(n) gives the converse.□
How the labels handle repeated symbols. For terms f(x,y)f(x,y) and f(y,x)f(y,x) using the same binary symbol, the ordered input labels are (x,y)(x,y) and (y,x)(y,x). They are different, so one function can give each result its required label. Two occurrences of the same term f(x,y)f(x,y) instead use the same rule. For f(u,u)f(u,u), either argument position can be used to copy the value of uu. The rules depend on terms, never on occurrences independently.
This is the routing method of Riis and Gadouleau [6], with the additional observation that the labels satisfy all disequalities at once. For example, u≠vu\ne v, v≠wv\ne w, and w≠uw\ne u hold simultaneously when u,v,wu,v,w are distinct terms and each receives its own label. Small finite sets can still be too small for the tests. The theorem controls growth as nn increases; it does not decide whether the sharp upper bound is ever reached at a finite size.

4. Forcing identities from all distinct pairs

Lemma 4.1. An inequality characterises the identity function. For any set AA and function F:A→AF:A\to A, [∀a,b∈A (a≠b⇒F(a)≠b)]⟺F=id⁡A. [\forall a,b\in A\ (a\ne b\Rightarrow F(a)\ne b)] \quad\Longleftrightarrow\quad F=\id_A.
Proof. If F(a)≠aF(a)\ne a, take b=F(a)b=F(a) to contradict the stated condition. Conversely, if F=id⁡AF=\id_A, the condition is just a≠b⇒a≠ba\ne b\Rightarrow a\ne b.□
For functions F1,…,FM,W:A→AF_1,\ldots,F_M,W:A\to A, define the set of allowed pairs C(F,W)={(a,b)∈A2:a≠b, Fj(a)≠b (1≤j≤M), W(a)≠a}. C(F,W)=\{(a,b)\in A^2:a\ne b,\ F_j(a)\ne b\ (1\le j\le M),\ W(a)\ne a\}. When (x,y)(x,y) are the only variables and are also the outputs, this set is itself the output image. Its size is at most n(n−1)n(n-1) for ∣A∣=n|A|=n. The next proposition characterises equality, called saturation above.
Proposition 4.2. Equality with the pair bound. If ∣A∣=n≥2|A|=n\ge2, then ∣C(F,W)∣=n(n−1)⟺[Fj=id⁡A for all j] and [W has no fixed point]. |C(F,W)|=n(n-1) \quad\Longleftrightarrow\quad [F_j=\id_A\text{ for all }j]\ \text{and}\ [W\text{ has no fixed point}].
Proof. The set C(F,W)C(F,W) is contained in the set of all n(n−1)n(n-1) pairs with different coordinates. Equality of their sizes means that every such pair is allowed. Lemma 4.1 then gives Fj=id⁡AF_j=\id_A for each jj. For any a∈Aa\in A, choose b≠ab\ne a; the test on WW gives W(a)≠aW(a)\ne a. Conversely, these identities and the absence of fixed points make every pair with different coordinates satisfy every test.□
We can also count exactly how many pairs are excluded. For each a∈Aa\in A, put Ba={a,F1(a),…,FM(a)}B_a=\{a,F_1(a),\ldots,F_M(a)\}, and put Z={a∈A:W(a)=a}Z=\{a\in A:W(a)=a\}. If a∈Za\in Z, no pair with first coordinate aa is allowed. Otherwise the allowed second coordinates are precisely A∖BaA\setminus B_a. Hence ∣C(F,W)∣=∑a∉Z(n−∣Ba∣),(1) |C(F,W)|=\sum_{a\notin Z}(n-|B_a|),\tag{1}n(n−1)−∣C(F,W)∣=(n−1)∣Z∣+∑a∉Z(∣Ba∣−1).(2) n(n-1)-|C(F,W)|=(n-1)|Z|+ \sum_{a\notin Z}(|B_a|-1).\tag{2} If WW has no fixed point, then ZZ is empty and ∣Ba∣−1≤M|B_a|-1\le M, so n(n−1)−Mn≤∣C(F,W)∣≤n(n−1).(3)\tag{3} n(n-1)-Mn\le |C(F,W)|\le n(n-1). The lower bound is an ordinary integer inequality and remains valid when n(n−1)−Mnn(n-1)-Mn is negative.
Example 4.3. A failed identity can exclude just one pair. Take A={0,1,2}A=\{0,1,2\}, outputs (x,y)(x,y), and tests x≠yx\ne y, F(x)≠yF(x)\ne y. If F(0)=1F(0)=1, F(1)=1F(1)=1, and F(2)=2F(2)=2, exactly five of the six pairs with different coordinates are allowed: only (0,1)(0,1) is excluded. Admitting all six pairs requires F(0)=0F(0)=0 as well. If we also require F(x)≠xF(x)\ne x, all six can never be admitted. More generally, on any nn-element set with n≥2n\ge2, these three tests have maximum output image size n(n−2)n(n-2). A point moved by FF allows n−2n-2 second coordinates, while a fixed point allows none. A cyclic permutation of all nn elements attains n(n−2)n(n-2). Thus the proportion n(n−2)/[n(n−1)]n(n-2)/[n(n-1)] tends to one, although the image always falls short of n(n−1)n(n-1) by at least nn.

5. Reduction from a fixed finitely presented group

The external undecidability theorem. A finite quotient of a group GG means a finite group QQ together with a surjective homomorphism G→QG\to Q. A word is separated in such a quotient if its image is not the identity. Bridson and Wilton [1, Theorem 2.1], deriving a consequence of Slobodskoi's construction [7], prove that there is a fixed finitely presented group GG for which the set {w:w has nonidentity image in some finite quotient of G} \{w:\text{$w$ has nonidentity image in some finite quotient of $G$}\} is recursively enumerable and undecidable. Thus an algorithm can eventually find a separating finite quotient whenever one exists, but no algorithm decides for every input word whether one exists. The presentation is fixed; the input consists only of the word. We first describe our reduction for an arbitrary finite presentation.
Fix G=⟨a1,…,ad∣r1,…,rq⟩. G=\langle a_1,\ldots,a_d\mid r_1,\ldots,r_q\rangle. For each generator introduce two unary symbols pi,mip_i,m_i. The notation suggests a generator and its inverse, but their interpretations are initially independent functions. For a signed word v=ℓ1⋯ℓLv=\ell_1\cdots\ell_L, whose letters belong to {a1±1,…,ad±1}\{a_1^{\pm1},\ldots,a_d^{\pm1}\}, define τv(x)=fℓ1(fℓ2(⋯fℓL(x)⋯ )),τε(x)=x, \tau_v(x)=f_{\ell_1}(f_{\ell_2}(\cdots f_{\ell_L}(x)\cdots)), \qquad \tau_\varepsilon(x)=x, where fai=pif_{a_i}=p_i, fai−1=mif_{a_i^{-1}}=m_i, and ε\varepsilon is the empty word. Let LG\mathcal L_G be the list of M=2d+qM=2d+q terms pi(mi(x)), mi(pi(x))(1≤i≤d),τrj(x)(1≤j≤q). p_i(m_i(x)),\ m_i(p_i(x))\quad(1\le i\le d), \qquad \tau_{r_j}(x)\quad(1\le j\le q). We call these the law terms, since requiring each to equal xx would impose inverse and relator identities. Repetitions are retained; an empty relator contributes the term xx. Our convention for multiplying permutations is composition with the rightmost function applied first, agreeing with the displayed nesting.
Given the input word ww, construct an instance with just the variables x,yx,y, output tuple (x,y)(x,y), and tests x≠y,L(x)≠y(L∈LG),τw(x)≠x.(4)\tag{4} x\ne y,\qquad L(x)\ne y\quad(L\in\mathcal L_G),\qquad \tau_w(x)\ne x. Here L(x)L(x) denotes the law term LL, with its indicated variable xx. Write DG,w(n)D_{G,w}(n) for this instance's dispersion. For each interpretation its output image is C(F,W)C(F,W) above, where F1,…,FMF_1,\ldots,F_M interpret the law terms and WW interprets τw\tau_w.
Theorem 5.1. The reduction. For every finite presentation GG and signed word ww, ∃n≥2: DG,w(n)=n(n−1)⟺w has nonidentity image in some finite quotient of G. \begin{gathered} \exists n\ge2:\ D_{G,w}(n)=n(n-1)\\ \Longleftrightarrow\\ \text{$w$ has nonidentity image in some finite quotient of $G$}. \end{gathered} The construction has linear output length in the explicit presentation and word lengths, and is computable in polynomial time.
Proof. Suppose DG,w(n)=n(n−1)D_{G,w}(n)=n(n-1), and choose an interpretation attaining this maximum on a set AA of size nn. Write pi,mip_i,m_i also for its unary functions. Proposition 4.2 gives pi∘mi=id⁡A=mi∘pip_i\circ m_i=\id_A=m_i\circ p_i, so the pip_i are permutations and mi=pi−1m_i=p_i^{-1}. It also gives τrj=id⁡A\tau_{r_j}=\id_A for every relator. The universal property of the presentation therefore gives a homomorphism ϕ:G→Sym⁡(A)\phi:G\to\Sym(A). The interpreted τw=ϕ(w)\tau_w=\phi(w) has no fixed point, hence is not the identity. The finite group ϕ(G)\phi(G), with the surjection G→ϕ(G)G\to\phi(G), is the required quotient. The identities hold at every point of AA, as required to define this homomorphism.
Conversely, suppose ϕ:G→Q\phi:G\to Q is a finite quotient with ϕ(w)≠1\phi(w)\ne1. On A=QA=Q, interpret pip_i as left multiplication by ϕ(ai)\phi(a_i) and mim_i as left multiplication by its inverse. Each law term is the identity function. The term τw\tau_w acts by left multiplication by ϕ(w)\phi(w), which has no fixed point: ϕ(w)b=b\phi(w)b=b would imply ϕ(w)=1\phi(w)=1. Proposition 4.2 gives DG,w(∣Q∣)=∣Q∣(∣Q∣−1)D_{G,w}(|Q|)=|Q|(|Q|-1), and ∣Q∣≥2|Q|\ge2. The construction of the instance only lists the inverse-law terms, copies the relators, and writes the nested term for ww, giving the stated size and time bounds.□
Theorem 5.2. Undecidability with fixed unary symbols and tests. There is a fixed finite presentation GG such that, given a signed word ww, deciding whether DG,w(n)=n(n−1)D_{G,w}(n)=n(n-1) for some n≥2n\ge2 is undecidable. The associated instances use a fixed finite unary signature, a fixed number of tests, and just two variables and two outputs. Their positive instances are recursively enumerable but not decidable, and their complement is not recursively enumerable.
Proof. Fix the presentation provided by the external theorem above and apply Theorem 5.1. Only τw\tau_w varies with the input. For enumerability, try n=2,3,…n=2,3,\ldots in order, and for each nn enumerate all interpretations on [n][n]. There are finitely many at each size, and each output image is computable by finite enumeration. This procedure finds an image of size n(n−1)n(n-1) whenever one exists. If the negative instances also had such a semidecision procedure, running both procedures in parallel would decide every instance, contradicting the reduction.□
Bridson–Wilton state their theorem for freely reduced words, meaning words with no adjacent inverse pair aiai−1a_i a_i^{-1} or ai−1aia_i^{-1}a_i. Such a word is already a valid signed input word here. Conversely, removing adjacent inverse pairs is computable and preserves evaluation in every group, hence preserves separation in finite quotients. The reduction theorem therefore gives the same exact decision problem for arbitrary signed words. This does not license cancellation in the terms under arbitrary interpretations: pip_i and mim_i need not be inverse functions. Cancellation preserves their evaluation only after the required inverse laws hold, as they do when the pair bound is attained.
The empty word yields the impossible test x≠xx\ne x and is a decidable negative case. Restricting to nonempty freely reduced words consequently leaves the problem undecidable. Recursively enumerable completeness is not asserted; it does not follow from enumerability and undecidability alone.

6. Proof of the one-unit theorem

Proof of Theorem 1.1. Fix k≥2k\ge2. Start with the instance associated to G,wG,w in Theorem 5.1. Add k−2k-2 new variables as further output coordinates, with no tests involving them. This operation is called padding. For each interpretation the new image is exactly the Cartesian product of the old pair image with [n]k−2[n]^{k-2}: the new variables can be chosen independently of every test and of the old outputs. Maximising over the same interpretations therefore gives DG,w(k)(n)=nk−2DG,w(n), D_{G,w}^{(k)}(n)=n^{k-2}D_{G,w}(n), where the superscript denotes the padded instance. All kk variables are outputs, so every cut contains them and they also form a cut. Thus ρ=k\rho=k. Since DG,w(n)≤n(n−1)D_{G,w}(n)\le n(n-1), for n≥2n\ge2 the inequality DG,w(k)(n)≥bk(n)D_{G,w}^{(k)}(n)\ge b_k(n) holds exactly when DG,w(n)=n(n−1)D_{G,w}(n)=n(n-1). For fixed kk, adding the variables and outputs takes constant extra space; the signature and tests are unchanged. Theorem 5.2 proves the claimed undecidability.
For the strict problem, a test with identical sides makes the answer no. Otherwise compute ρ=ρΓ\rho=\rho_\Gamma. If ρ≤k\rho\le k, then Proposition 3.2 gives, for every n≥2n\ge2, DΓ(n)≤bρ(n)≤bk(n), D_\Gamma(n)\le b_\rho(n)\le b_k(n), so again the answer is no. If ρ≥k+1\rho\ge k+1, Theorem 3.1 gives DΓ(n)≥⌊n/s⌋ρ≥⌊n/s⌋k+1(n≥s). D_\Gamma(n)\ge\lfloor n/s\rfloor^\rho \ge\lfloor n/s\rfloor^{k+1}\qquad(n\ge s). For n=sk+1n=s^{k+1} the last expression is (sk)k+1=nk≥nk−nk−1+1=bk(n)+1. (s^k)^{k+1}=n^k\ge n^k-n^{k-1}+1=b_k(n)+1. Here s≥2s\ge2 because x,yx,y are distinct, so n≥2n\ge2. This proves the criterion and the explicit sufficient size. Checking syntax and computing a minimum vertex cut are polynomial-time operations, as detailed below. Comparing ρ\rho with the binary integer k+1k+1 is polynomial too. The decision algorithm need not construct nn or any interpreting functions.
Finally, suppose a total computable bound B(N)B(N) as in the theorem existed for some fixed kk. On an input from the padded family, compute its bit length NN and enumerate 2≤n≤B(N)2\le n\le B(N). For each size enumerate all interpretations and all assignments, form the set of distinct outputs satisfying the tests, and compare its size with bk(n)b_k(n). The search is finite and, by the assumed bound, would answer yes exactly on the positive instances. This would decide the undecidable problem. The contradiction needs no time bound on this exhaustive search.□
The polynomial-time algorithm. First validate the input as described in Section 2. Process terms in topological order. Assign an identifier to each source and identify compound terms by the record (f,i1,…,id)(f,i_1,\ldots,i_d) of their symbol and ordered child identifiers. Equal records receive the same identifier. Thus syntactically equal expressions are identified even when the input supplied different node names for them. Reject any test whose two resulting identifiers agree. Build the term graph on these identifiers, compute its minimum cut by the network in Theorem 3.1, and answer yes exactly when ρΓ≥k+1\rho_\Gamma\ge k+1.
For a term description of NN bits, at most NN nodes and argument entries are supplied. Pairwise comparison of the records can be done in O(N3)O(N^3) bit operations. The split network has O(N)O(N) vertices and edges and integer capacities at most N+1N+1. An augmenting-path flow algorithm needs at most s≤Ns\le N augmentations, since each increases the integer flow by at least one, while the cut of all unit edges bounds it by ss. Path searches and updates involve only polynomially many entries. Indices, capacities and flow values have O(log⁡N)O(\log N) bits, so even sequential scans for lookups give polynomial bit cost. Together with validation and the binary comparison with k+1k+1, this proves the uniform polynomial-time bound. No loop of length kk is needed when kk is large.
Which degree can give an undecidable question. For an instance in C\mathcal C without an identical-side test, DΓ(n)=Θ(nρ)D_\Gamma(n)=\Theta(n^\rho). If k<ρk<\rho, the strict threshold is exceeded for all sufficiently large nn. If k>ρk>\rho, the sharp upper bound is smaller than bk(n)b_k(n) for every n≥2n\ge2, so even the non-strict answer is no. When k=ρk=\rho, the non-strict question asks whether the upper bound bρ(n)b_\rho(n) is attained for some nn; this is the subclass on which the reduction proves undecidability. It also follows that the existential strict question is equivalent to requiring DΓ(n)≥bk(n)+1D_\Gamma(n)\ge b_k(n)+1 for all sufficiently large nn, and to requiring DΓ(n)≥nk+1/2D_\Gamma(n)\ge n^{k+1/2} for all sufficiently large nn. These are consequences; both questions in Theorem 1.1 itself use the existential quantifier.
Three outputs. For outputs (x,y,t)(x,y,t) in C\mathcal C, first reject a test with identical sides. Then ρ=2\rho=2 if tt contains no variable other than x,yx,y, including when it contains no variables at all. If another variable occurs in tt, a path from it to tt cannot pass through xx or yy, since variable vertices have no incoming edges. Together with the paths of length zero at x,yx,y, this gives three disjoint paths. The three outputs form a cut, so ρ=3\rho=3. For k=2k=2, the strict algorithm thus only has to check whether tt contains another variable. In the positive case s3s^3 is a sufficient size and DΓ(n)=Θ(n3)D_\Gamma(n)=\Theta(n^3). The lower bound is n3/(8s3)n^3/(8s^3) for n≥2sn\ge2s, hence at least n5/2n^{5/2} for n≥64s6n\ge64s^6.
Requiring x,yx,y to be outputs is essential to this criterion. For example, with four distinct variables x,y,z,wx,y,z,w, outputs (z,w)(z,w), and only the test x≠yx\ne y, every pair (z,w)(z,w) is an output for n≥2n\ge2. Thus D(n)=n2≥b2(n)+1D(n)=n^2\ge b_2(n)+1 although the cut size is two. This instance lies outside C\mathcal C: the two variables constrained to differ are not output coordinates.

7. Functions approaching the pair bound

Theorem 7.1. An explicit approximation to the pair bound. Fix a finite presentation GG and its M=2d+qM=2d+q law terms. For every nonempty signed word ww of length LL and every integer n>Ln>L, n(n−1)−Mn≤DG,w(n)≤n(n−1). n(n-1)-Mn\le D_{G,w}(n)\le n(n-1). An interpretation giving the lower bound is explicitly computable and uses only cyclic shifts. In particular, for each such word, lim⁡n→∞DG,w(n)n(n−1)=1,DG,w(n)=n2−OG(n). \lim_{n\to\infty}\frac{D_{G,w}(n)}{n(n-1)}=1, \qquad D_{G,w}(n)=n^2-O_G(n). The constant in the error bound depends only on the presentation, while the condition n>Ln>L also depends on the word.
Proof. On A=Z/nZA=\mathbb Z/n\mathbb Z, interpret every pip_i and every mim_i as z↦z+1z\mapsto z+1. A word of length ℓ\ell as written then acts by z↦z+ℓz\mapsto z+\ell, regardless of the signs of its letters. Because 0<L<n0<L<n, the function interpreting τw\tau_w has no fixed point. For each first coordinate aa, the tests exclude at most M+1M+1 second coordinates: aa itself and the MM law values. The lower bound follows from (3). Dividing by n(n−1)n(n-1) gives a proportion between 1−M/(n−1)1-M/(n-1) and 11, proving the limit and the error estimate. The inequality is valid even if its lower bound is nonpositive.
The formal inverse symbols receive the same shift as the positive symbols. This is permitted because an interpretation consists of arbitrary functions. Inverse laws are forced only when every pair with different coordinates is admitted.□
For this interpretation the exact count is ∣C∣=n(n−1−∣Rn∣),Rn={∣v∣ mod n:τv∈LG}∖{0}. |C|=n(n-1-|R_n|),\qquad R_n=\{|v|\bmod n:\tau_v\in\mathcal L_G\}\setminus\{0\}. Each inverse-law term is here regarded as its two-letter word, and ∣v∣|v| always counts the letters without cancellation. Distinct nonzero residues give distinct additional forbidden second coordinates for each first coordinate; the zero residue forbids nothing beyond aa.
Given a nonempty word ww and a positive rational ε\varepsilon, choose, for example, n=1+max⁡{L,⌈1+M/ε⌉}. n=1+\max\{L,\lceil1+M/\varepsilon\rceil\}. This integer satisfies n>Ln>L and M/(n−1)≤εM/(n-1)\le\varepsilon. Return nn and the unary functions z↦z+1(modn)z\mapsto z+1\pmod n. Under this interpretation the instance has at least (1−ε)n(n−1)(1-\varepsilon)n(n-1) distinct output pairs. The functions have finite explicit tables; writing those tables takes time polynomial in nn and the input length, with nn measured by its value rather than its binary length. Here density refers exactly to the ratio of the image size to n(n−1)n(n-1).
This gives more information than the quadratic growth exponent: for any prescribed rational error an algorithm produces functions with the required proportion of outputs. Nonetheless it cannot decide whether some interpretation admits all n(n−1)n(n-1) pairs. A nonzero loss of at most MnMn pairs becomes arbitrarily small after division by n(n−1)n(n-1), while zero loss imposes every group identity on all of AA. The approximate interpretations are not required to be group actions.
The distinction between an empty word and a word representing the identity matters. The empty word gives x≠xx\ne x and zero dispersion. A nonempty word can represent the identity in GG, or even cancel freely to the empty word, while retaining positive length as an input expression. Its shift interpretation still gives the bound above. There is no conflict with the reduction theorem: cancellation preserves group evaluation, but need not preserve evaluation by these arbitrary unary functions. For such an identity word, the exact answer is no even though the proportions tend to one.
For the padded instances of degree k≥2k\ge2, the exact product identity gives, for n>Ln>L, bk(n)−Mnk−1≤DG,w(k)(n)≤bk(n),lim⁡n→∞DG,w(k)(n)bk(n)=1. b_k(n)-Mn^{k-1}\le D_{G,w}^{(k)}(n)\le b_k(n), \qquad \lim_{n\to\infty}\frac{D_{G,w}^{(k)}(n)}{b_k(n)}=1. The lower bound again uses ordinary integer subtraction. For every n≥2n\ge2 the ratio equals the original pair ratio. Thus the same algorithm gives a proportion at least 1−ε1-\varepsilon of bk(n)b_k(n) by adding the independent output variables, although deciding whether bk(n)b_k(n) is attained at any size remains undecidable.

8. Scope and the problem without tests

The decision problems use one finite set for all variables and function values. For each fixed k≥2k\ge2, undecidability already holds with kk variables, all retained as outputs, a fixed finite unary signature and a fixed number of tests. Only the nested expression for the input word varies. The tests compare computed expressions as well as variables. Writing a computed term as a new variable with a defining equation does not make it an independent source variable: its value is determined by the original inputs. The reduction therefore proves no undecidability result for the narrower language in which tests may compare only source variables.
The open bijectivity problem. Without disequality tests, finite square term bijectivity asks the following: given kk terms in kk variables, does some interpretation on a finite set AA, with ∣A∣≥2|A|\ge2, make the resulting map Ak→AkA^k\to A^k bijective? This problem remains open in general. The analysis of ordinary dispersion in [5] identifies an image of size ∣A∣k|A|^k for such a map with bijectivity, and gives padding reductions from the case k=3k=3 to the problem of attaining the full output set at every fixed output dimension at least three. Those reductions do not prove undecidability and are not used here. An unconditional polynomial-time/undecidable separation for dispersion without disequality tests remains open. The present bounds also concern a different quantity from the number of solutions of an arbitrary equation system or the entropy and guessing number of a graph; they do not imply that those quantities are integer-valued or efficiently computable.
Machine verification. The development, archived release and interactive paper are available at:
GitHub:
https://github.com/SR123/term-coding-disequality-lean
DOI: 10.5281/zenodo.22727895
Interactive paper:
https://sr123.github.io/term-coding-disequality-lean/
The accompanying Lean 4.26 development has 71 mathematical and algorithmic modules. It checks the output-image definition, the sharp cut bound when x,yx,y are outputs, finite directed Menger and max-flow results, the routing construction, and the strict criterion for every degree with its explicit sufficient size. It also checks the argument forcing identities, the equivalence with finite-quotient separation, the exact product under padding, finite search, enumerability, and the absence of a computable bound on alphabet size, as well as the approximation, asymptotic and flattening results. The undecidability theorems assume explicitly the fixed-presentation finite-group noncomputability result. The classical theorem of Slobodskoi in the form used by Bridson–Wilton is an external input, not a theorem formalised in this project. The axiom audits use only the standard axioms of Lean's classical foundations, with no admissions. The build and audit records accompany the source.
For the strict decision algorithm, the development proves correctness of parsing, rejection of malformed bit strings, and the decision by max-flow. It also certifies one fixed deterministic random-access machine program under a logarithmic cost criterion. For every input bit string bb, including malformed inputs, this program halts with the specified decision result. Fixed constants C≥1C\ge1 and cc bound both its number of instructions executed and its total logarithmic cost by C(∣b∣+1)cC(|b|+1)^c. The binary degree is part of the input; the program does not loop to its value. The main formal statements are program_polynomial and program_accepts_iff in MMain.lean. The standard polynomial simulation from this RAM model to a multitape Turing machine is not formalised here. The ordinary bit-complexity argument appears in Section 6.
The interactive edition links the text of this paper to explanations, exact formal statements and proofs, including the hypotheses used at each stage. The reader can inspect Lean's recorded proof states and follow formal dependencies into library proofs and the underlying logical rules. External mathematical input and the limits of machine verification are identified explicitly. This correspondence helps a reader check that the formal statements express the claims made in the paper; kernel checking of a Lean proof alone does not establish that correspondence.

References

  1. Martin R. Bridson and Henry Wilton. The triviality problem for profinite completions. Inventiones Mathematicae, 202:839–874, 2015. arXiv:1401.2273; Theorem 2.1.
  2. Karl Menger. Zur allgemeinen kurventheorie. Fundamenta Mathematicae, 10:96–115, 1927.
  3. Søren Riis. Term coding for extremal combinatorics: Dispersion and complexity dichotomies. arXiv:2504.16265v3, 2025. Earlier omnibus; its square-bijectivity undecidability claim is withdrawn in the present replacement.
  4. Søren Riis. Term coding: An entropic framework for extremal combinatorics and the guessing–number sandwich theorem. arXiv:2601.16614v2, 2026. Revised 30 August 2026.
  5. Søren Riis. Term coding and dispersion: Exact and asymptotic decision problems. arXiv:2602.08110v2, 2026. Revised 1 September 2026.
  6. Søren Riis and Maximilien Gadouleau. Max-flow min-cut theorems on dispersion and entropy measures for communication networks. Information and Computation, 267:49–73, 2019. Preprint: arXiv:1012.5224.
  7. A. M. Slobodskoi. Undecidability of the universal theory of finite groups. Algebra i Logika, 20(2):207–230, 1981. In Russian; English translation in Algebra and Logic 20 (1981), 139–156.