No lattice tiling of $\mathbb{Z}^{35}$ or $\mathbb{Z}^{805}$ by Lee balls of radius three

Introduction

For integers $n \ge1$ and $r \ge0$ the Lee ball of radius $r$ in $\mathbb{Z}^n$ is

A tiling of $\mathbb{Z}^n$ by $B^n(r)$ is a set $T \subset\mathbb{Z}^n$ such that the translates $t + B^n(r)$ with $t \in T$ partition $\mathbb{Z}^n$, and it is a lattice tiling if $T$ is a subgroup of $\mathbb{Z}^n$. Such tilings exist when $n \le2$ and when $r = 1.¹$ Golomb and Welch [6] conjectured that these are the only cases.

The conjecture is open, and so is its lattice form, in which only lattice tilings are considered. It holds for $3 \le n \le5$ [7, 8] and for radii that are large compared with the dimension [15, 10]; the lattice form holds for radius two in every dimension [13]. We refer to the survey of Horak and Kim [10] for the history. A lattice tiling is the same thing as a perfect code in a finite abelian group [9], and in this form many further dimensions have been excluded for small radii by the polynomial method and by group-ring equations [11, 19, 21, 16, 20]. Xiao and Zhou [18] recently combined all these criteria with new ones and applied them to every pair $(n, r)$ with $n \ge3$, $r \ge2$ and $|B^n(r)| < 2^{30}$. Of the 1358 such pairs they excluded 1356, and the two that remained are $(n, r) = (35, 3)$ and $(805, 3)$ [18 Theorem 5.1]. We settle both.

2020 Mathematics Subject Classification. Primary 52C22; Secondary 05B45, 94B25, 05C25.

Key words and phrases. Golomb–Welch conjecture, Lee metric, perfect code, lattice tiling, group ring.

Corresponding author: Deep Bhattacharjee.

Proof. This is Theorem 1.1 together with [18 Theorem 5.1]. □

The balls in question have

Neither number is prime, so the theorem of Szegedy [17], which turns the nonexistence of lattice tilings into the nonexistence of all tilings when $|B^n(r)|$ is prime, does not apply, and Theorem 1.1 says nothing about tilings that are not lattice tilings. In the language of the degree–diameter problem [5], Theorem 1.1 says that no abelian group of order 59711 is generated by 35 elements in such a way that each of its elements is a sum of at most three of these generators and their negatives, and likewise for order 696845031 and 805 generators; in other words the abelian Cayley–Moore bound is not attained in degree 70 or in degree 1610 at diameter three (compare [18 Section 1]).²

The method

A lattice tiling of $\mathbb{Z}^n$ by $B^n(3)$ gives a finite abelian group $G$ of order $|B^n(3)|$ and elements $g_1,\ldots,g_n$ such that $a \mapsto\sum_j a_jg_j$ maps $B^n(3)$ bijectively onto $G$ (Lemma 2.2). Summing a character over the ball gives a cubic identity in a group ring (Proposition 2.3), and projecting $G$ onto $\mathbb{Z}/p$ for a prime $p$ dividing $|G|$ turns it into conditions on the images of the $g_j$. This is the setting of [21, 18], and two features of the present cases defeat the projections used so far.

For $n=805$ the conditions modulo $p=29$ leave a very large number of possible distributions of the images, whose examination Xiao and Zhou estimated would take about two months of exhaustive search [18 Example 5.13]. We read off the coefficient of the identity element modulo $29^2$ instead; it excludes all of them by one congruence (Section 5).

For $n=35$ Xiao and Zhou found, for each of the two primes 71 and 29, a distribution of the images that satisfies every condition coming from that prime alone [18 Example 5.14]. We project onto $\mathbb{Z}/71 \times\mathbb{Z}/29$ at once, through a character with values in the dual numbers over the group ring $\mathbb{F}_{71}[\mathbb{Z}/29]$. The first-order part of the identity couples the two distributions and leads to a circulant linear system over $\mathbb{F}_{71}$ whose only solution is zero (Section 6). Figure 1 shows the order of the argument.

Image not extracted

Theorem 1.1, with every step of Sections 2–6, has been formalized in the Lean 4 proof assistant (Section 7).

Perfect codes and the ball identity

All groups in this paper are abelian and written additively, except the groups of units of rings. For $a \in\mathbb{Z}^n$ we write $|a|=|a_1|+\cdots+|a_n|$, and $B^n=B^n(3)$.

Figure 2 shows the ball $B^3(3)$, the tile of the three-dimensional case.

Image not extracted

The next identity is the source of all the conditions used below. Let $f_n$ be the polynomial

Proof. Put $u_j=\chi(z_j)$ and $v_j=\chi(-z_j)$, so that $u_jv_j=1$ and $\chi\left(\sum_j a_jz_j\right)=\prod_j u_j^{a_j}$, where $u_j^{-1}=v_j$. Consider multisets of the letters $u_1,\ldots,u_n$ and $v_1,\ldots,v_n$, and say that a multiset contains a pair if it contains both $u_j$ and $v_j$ for some $j$. A multiset $M$ of size $k$ without a pair corresponds to the point $a\in\mathbb{Z}^n$ with $a_j$ equal to the multiplicity of $u_j$ minus that of $v_j$; this is a bijection onto the points with $|a|=k$, and the product of the elements of $M$ is $\prod_j u_j^{a_j}$.

Let $h_k$ be the sum, over all multisets $M$ of size $k$, of the product of the elements of $M$, and let $p_i=\sum_j(u_j^i+v_j^i)$. The multisets of size 2 with a pair are the $n$ multisets $\{u_j,v_j\}$, each with product 1. A multiset of size 3 with a pair is $\{u_j,v_j,w\}$ for one index $j$ and one letter $w$, these are distinct for distinct $(j,w)$, and the product is $w$. Hence

Newton’s identities give $2h_2=p_1^2+p_2$ and $6h_3=p_1^3+3p_1p_2+2p_3$ in the polynomial ring over $\mathbb{Z}$ in the $2n$ letters, hence in $R$. Six times the right side above is therefore

which is $T_1^3+3T_1T_2+2T_3-6nT_1$ for $T_i=1+p_i$.

With $\Gamma$ trivial, (2.1) reads $6|B^n|=f_n(2n+1)$. For instance $|B^{35}|=f_{35}(71)/6=59711$ and $|B^{805}|=f_{805}(1611)/6=696845031$.

Proof. The argument of $F$ is $\psi(\varphi_g(a))$, and $\varphi_g$ maps $B^n$ bijectively onto $G$, so the left side is $\sum_{x\in G}F(\psi(x))$. Each fibre of $\psi$ has $|G|/|\Gamma|$ elements.

For a commutative ring $k$ and a finite group $\Gamma$ we write $k[\Gamma]$ for the group ring, with basis elements $[\gamma]$, $\gamma\in\Gamma$, multiplied by $[\gamma][\gamma']=[\gamma+\gamma']$. Its unit element is $[0]$, and we write $S_\Gamma=\sum_{\gamma\in\Gamma}[\gamma]$. For $F\in k[\Gamma]$ we write $F(\gamma)$ for the coefficient of $[\gamma]$.

Proof. Apply Proposition 2.3 with $z_j=x_j$ and then Lemma 2.4 with $F=\chi$. Part (2) is the case $R=k[\Gamma]$, $\chi(\gamma)=[\gamma]$.

Proof. Write $G$ as a direct sum of cyclic groups of prime power order. Since $p$ divides $|G|$, one summand is $\mathbb{Z}/p^e$ with $e\ge1$; project onto it and reduce modulo $p$.

Power sums modulo a prime

Throughout this section $g$ is a perfect code in a group $G$ with $|G|=|B^n|$, $p$ is a prime dividing $|G|$, and $\psi:G\to\mathbb{F}_p=\mathbb{Z}/p$ is surjective. We put

with $0^0=1$. For odd $k$ the two terms of each summand cancel, so $P_k=0$. For $F\in\mathbb{F}_p^{\mathbb{F}_p}$ and $k\geq0$ we define the moment $M_k(F)=\sum_{h\in\mathbb{F}_p}F(h)h^k\in\mathbb{F}_p$. Expanding $(h+h')^k$ gives

For $T_i=[0]+\sum_j([ix_j]+[-ix_j])$ we have $M_0(T_i)=2n+1$ and $M_k(T_i)=i^kP_k$ for $k\geq1$.

Proof. Call $F$ flat if $M_k(F)=0$ for $1\leq k<v$. By (4) a product of flat elements is flat, and for flat $F,F'$ we have $M_v(FF')=M_0(F)M_v(F')+M_v(F)M_0(F')$. The $T_i$ are flat by hypothesis, so

Apply $M_v$ to (3) with $k=\Gamma=\mathbb{F}_p$; the left side becomes $6m\sum_h h^v$.

Proof. If $1\leq v<p-1$, a generator $u$ of the cyclic group $\mathbb{F}_p^\times$ has $u^v\ne1$, and $\sum_h h^v=\sum_h(uh)^v=u^v\sum_h h^v$. If $v=p-1$, then $h^v=1$ for $h\ne0$.

Proof. By induction on $k$. For odd $k$ we have seen that $P_k=0$. For even $k<L$, Proposition 3.1 with $v=k$ and Lemma 3.2 give $\kappa_n(k)P_k=0$.

When all power sums below $p-1$ vanish, the distribution of the $x_j$ is almost determined.

Proof. (1) Let $F=T_1-(2n+1)[0]$, so that $F(h)=c(h)+c(-h)-2n\delta_{h,0}$, $M_0(F)=0$ and $M_k(F)=P_k$ for $k\geq1$. Fix $h\in\mathbb{F}_p$. Expanding $(h'-h)^{p-1}$ by the binomial theorem gives

On the other hand $(h'-h)^{p-1}$ is $1$ for $h'\ne h$ and $0$ for $h'=h$, so the left side is $M_0(F)-F(h)=-F(h)$. Thus $F(h)\equiv D$ for every $h$, which is (1).

(2) Every $j$ with $x_j\ne0$ is counted in exactly two of the numbers $c(h)+c(-h)$ with $h\ne0$, so these $p-1$ numbers add up to $2n-2c(0)$. Each of them is a

::: nonnegative integer congruent to $D$ modulo $p$, and $0 \le D < p$, so each is at least $D$. □

The constant term modulo $p$ squared

The identity (3) holds over $\mathbb{Z}$, so it can be read modulo $p^2$. When the pair counts are divisible by $p$, its coefficient at $[0]$ gives one more congruence.

Proof. Work in $(\mathbb{Z}/p^2)[\mathbb{F}_p]$. As $p \ge5$, the numbers $i=1,2,3$ are invertible modulo $p$, and the coefficient of $T_i$ at $h$ is $\delta_{h,0}+c(i^{-1}h)+c(-i^{-1}h)$. At $h=0$ this is $A=1+2c(0)$, and at $h \ne0$ it is divisible by $p$. Hence $T_i=A[0]+pW_i$ with $W_i(0)=0$. Since $p^2=0$,

and the second term has coefficient $0$ at $[0]$. The left side of (2.3) is $6mS_{\mathbb{F}_p}$, whose coefficient at $[0]$ is $6m$. □

Dimension 805

Proof of Theorem 1.1 for $n=805$. Suppose that a lattice tiling exists. Lemma 2.2 gives a perfect code $g$ in a group $G$ of order 696845031, and Lemma 2.6 gives a surjection $\psi:G\to\mathbb{F}_{29}$. We use the notation of § 3 with $p=29$, so $m=|G|/29=24029139=29\cdot828591$.

Step 1: $P_k=0$ for $1\le k\le28$. Modulo 29 we have $n\equiv22$, $2n+1\equiv16$ and $3\equiv2^5$, so with $z=2^v$,

Table 1 lists these values for even $v\le28$; none is zero. Corollary 3.3 with $L=28$ gives $P_k=0$ for $1\le k<28$. Proposition 3.1 with $v=28$ and Lemma 3.2 give $9P_{28}=-6m=0$, since 29 divides $m$. Hence $P_{28}=0$.

Step 2: the counts. Lemma 3.4 applies with $D=0$: 29 divides $c(h)+c(-h)$ for every $h\ne0$, and $2c(0)\equiv2n$, so $c(0)\equiv22\pmod{29}$. Since $0\le c(0)\le805=22+29\cdot27$, we can write $c(0)=22+29k$ with $0\le k\le27$.

Step 3: modulo $29^2$. By Lemma 4.1, $6m\equiv f_{805}(A)\pmod{29^2}$ with $A=1+2c(0)=45+58k$. For integers $a$ and $y$,

Take $a=45$ and $y=58k$; the last two terms are divisible by $29^2$. Here $f_{805}(45)=-120060\equiv29\cdot7$ and $f'_{805}(45)=1517\equiv9\pmod{29}$, so $f_{805}(A)\equiv29(7+18k)\pmod{29^2}$. On the other side $6m=29\cdot4971546$ with $4971546\equiv18\pmod{29}$. Therefore $7 + 18k \equiv18$, that is $18k \equiv11 \pmod{29}$. As $18 \cdot21 \equiv1$, this gives $k \equiv11 \cdot21 \equiv28 \pmod{29}$, which contradicts $0 \le k \le27$. □

Without the bound $c(0) \le n$ the congruence of Step 3 has the solution $c(0) = 834$; it is the size of $G$ relative to $n$, through $c(0) \le n$, that closes the case.

Dimension 35

Suppose that a lattice tiling of $\mathbb{Z}^{35}$ by $B^{35}(3)$ exists. By Lemma 2.2 there is a perfect code $g$ in a group $G$ of order $59711 = 71 \cdot29^2$, and by Lemma 2.6 there are surjections $\psi_1 : G \to\mathbb{F}_{71}$ and $\psi_2 : G \to\mathbb{F}_{29}$. We put

$x_j = \psi_1(g_j) \in\mathbb{F}_{71}, \qquad y_j = \psi_2(g_j) \in\mathbb{F}_{29},$

$c_{71}(h) = \#\{j : x_j = h\}, \qquad c_{29}(t) = \#\{j : y_j = t\}.$

The prime 71

Proof. We apply § 3 with $p = 71$ and $m = 841$. Since $2n + 1 = 71$ and $6n = 210 \equiv-3 \pmod{71}$, we have $\kappa_{35}(v) \equiv2 \cdot3^v + 3 = 3(2 \cdot3^{v-1} + 1)$. If this vanished, then $3^{v-1} \equiv-2^{-1} \equiv-36 = -6^2$. But $3$ is a square modulo $71$, because $\left(\frac{3}{71}\right) = -\left(\frac{71}{3}\right) = -\left(\frac{2}{3}\right) = 1$, while $-1$ is not, because $71 \equiv3 \pmod{4}$. So $\kappa_{35}(v) \ne0$ for every $v \ge1$, and Corollary 3.3 with $L = 70$ gives $P_k = 0$ for $1 \le k < 70$. For $v = 70$ we have $\kappa_{35}(70) \equiv2 + 3 = 5$ by Fermat’s theorem, and $6m = 5046 \equiv5$, so Proposition 3.1 and Lemma 3.2 give $5P_{70} = -5$, that is $P_{70} = -1$ and $D = 1$.

By Lemma 3.4, $2c_{71}(0) \equiv2n + 1 = 71 \equiv0$, and $c_{71}(0) \le35$, so $c_{71}(0) = 0$. Then $(p - 1)D + 2c_{71}(0) = 70 = 2n$, and the equality case of Lemma 3.4 gives $c_{71}(h) + c_{71}(-h) = 1$ for $h \ne0$. If $x_j = \pm x_k$ for some $j \ne k$, then $h = x_j \ne0$ has $c_{71}(h) + c_{71}(-h) \ge2$, since $h \ne-h$. □

The prime 29

Proof. We apply § 3 with $p = 29$ and $m = 2059 = 29 \cdot71$. Modulo $29$ we have $2n + 1 \equiv13$ and $6n \equiv7$, so with $z = 2^v$,

$\kappa_{35}(v) \equiv3 \cdot13^2 + 3 \cdot13(1 + z) + 2z^5 - 7 \equiv2z^5 + 10z + 17 \pmod{29}$.

By Table 1 these values are nonzero for even $v \le26$, so Corollary 3.3 with $L = 28$ gives $P_k = 0$ for $1 \le k < 28$. (The value at $v = 28$ is zero, so $P_{28}$ is not determined.) Let $D$ be as in Lemma 3.4. Then $28D + 2c_{29}(0) \le70$, so $D \le2$, and $2c_{29}(0) \equiv70 + D \pmod{29}$.

$v$	2	4	6	8	10	12	14	16	18	20	22	24	26	28
$\kappa_{805}(v)$ mod 29	24	19	23	23	24	8	25	10	15	11	11	10	26	9
$\kappa_{35}(v)$ mod 29	17	20	27	10	1	3	5	17	14	7	24	4	2	0

If $D = 0$, then $c_{29}(0) \equiv35 \equiv6$ and $c_{29}(0) \le35$, which is (a). If $D = 1$, then $2c_{29}(0) \equiv13$, so $c_{29}(0) \equiv21$, while $2c_{29}(0) \le42$; hence $c_{29}(0) = 21$, equality holds in Lemma 3.4(2), and we are in (b). If $D = 2$, then $2c_{29}(0) \equiv14$, so $c_{29}(0) \equiv7$, while $2c_{29}(0) \le14$; hence $c_{29}(0) = 7$ and we are in (c). □

Figure 3 shows the distributions of Lemma 6.1 and of case (c).

Image not extracted

Case (a)

By Lemma 4.1 with $p=29$, $6m=12354\equiv580\pmod{841}$ would be congruent to $f_{35}(1+2c_{29}(0))$. But $f_{35}(13)=13\cdot14\cdot15-210\cdot13=0$ and $f_{35}(71)=71(72\cdot73-210)=6\cdot71\cdot841\equiv0$. Since $580\not\equiv0\pmod{841}$, case (a) is impossible.

The joint projection

In cases (b) and (c) we have $c_{29}(t)+c_{29}(-t)=D$ for every $t\ne0$, with $D=1$ and $c_{29}(0)=21$, or $D=2$ and $c_{29}(0)=7$. Let $\Gamma=\mathbb{F}_{71}\times\mathbb{F}_{29}$ and $\psi=(\psi_1,\psi_2):G\to\Gamma$. The image of $\psi$ is a subgroup of the cyclic group $\Gamma$ of order $2059$ whose order is divisible by $71$ and by $29$, because both projections are onto; so $\psi$ is surjective and $|G|/|\Gamma|=29$.

Let $R_0=\mathbb{F}_{71}[\mathbb{F}_{29}]$ and let $\Lambda=R_0[\varepsilon]/(\varepsilon^2)$ be the ring of dual numbers over $R_0$. The map

is a homomorphism $\Gamma\to\Lambda^\times$, because $(1+s\varepsilon)(1+s'\varepsilon)=1+(s+s')\varepsilon$. The left side of (2.2) is

because $71=0$ and $\sum_{s\in\mathbb{F}_{71}}s=71\cdot35=0$ in $\mathbb{F}_{71}$. On the right side $T_i=U_i+N_i\varepsilon$ with

Taking the coefficient of $\varepsilon$ in (2.2) gives

The coefficient of $U_i$ at $t$ is $\delta_{t,0}+c_{29}(i^{-1}t)+c_{29}(-i^{-1}t)$, which equals $1+2c_{29}(0)$ at $t=0$ and $D$ at $t\ne0$. Hence $U_i=A[0]+DS$ with $S=S_{\mathbb F_{29}}$ and $A=1+2c_{29}(0)-D$. Since $S[t]=S$ for every $t$, we get $SN_i=0$, and (6.1) becomes

For $t\in\mathbb F_{29}$ put

The coefficient of $N_i$ at $t$ is $i\,s(i^{-1}t)$. In $\mathbb F_{29}$ we have $2^{-1}=15$ and $3^{-1}=10$, so (6.2) says that

In case (b), $A=42$, and the coefficients are $5208\equiv25$, $252\equiv39$ and $6$ modulo $71$. In case (c), $A=13$, and they are $336\equiv52$, $78\equiv7$ and $6$. Multiplying by $12=6^{-1}$ in $\mathbb F_{71}$, we obtain

with $(a,b)=(16,42)$ in case (b) and $(a,b)=(56,13)$ in case (c).

A circulant system

The residue $2$ is a primitive root modulo $29$: $2^4=16\ne1$, $2^7=128\equiv12$ and $2^{14}\equiv144\equiv-1$, so the order of $2$ divides $28$ but not $14$ or $4$. Hence $15=2^{-1}$ has order $28$, $15^{14}=-1$, and $15^5=2^{-5}=3^{-1}=10$, since $2^5=32\equiv3$. Put $\mu_k=s(15^k)$ for $k\in\mathbb Z$. Then $\mu_{k+28}=\mu_k$, and since $s(-t)=-s(t)$, also $\mu_{k+14}=-\mu_k$. Taking $t=15^k$ in (6.4) gives

Figure 4 shows these relations on the orbit of 1.

Let $V$ be the $\mathbb F_{71}$-vector space of sequences $(\mu_k)_{k\in\mathbb Z}$ of period $28$, and let $\sigma$ be the shift, $(\sigma\mu)_k=\mu_{k+1}$. It is invertible, with $\sigma^{-1}=\sigma^{27}$. For our $\mu$ the set $I$ of polynomials $Q\in\mathbb F_{71}[X]$ with $Q(\sigma)\mu=0$ is an ideal. It contains $Q=X^5+bX+a$ by (6.5), and $X^{14}+1$. Applying $\sigma^5\mu=-(a+b\sigma)\mu$ three times gives $\sigma^{15}\mu=-(a+b\sigma)^3\mu$, while $\sigma^{15}\mu=\sigma\sigma^{14}\mu=-\sigma\mu$. So $I$ also contains $C=(a+bX)^3-X$. All congruences below are modulo $71$.

In case (b), $C=35X^3-31X^2+21X-22$ and $I$ contains $\widetilde C=-2C=X^3-9X^2+29X-27$. Division with remainder gives

Hence $X(X+6)\in I$, and then $X-5\in I$. As $\sigma$ is invertible, $(\sigma+6)\mu=0$ and $(\sigma-5)\mu=0$; subtracting, $11\mu=0$, so $\mu=0$.

In case (c), $C=-4X^3-8X^2-30X+33$ and $I$ contains $\widetilde C=-18C=X^3+2X^2-28X-26$. Here

Hence $(X-14)^2\in I$, and then $X+16\in I$. So $\sigma\mu=-16\mu$, and $0=(\sigma-14)^2\mu=30^2\mu=48\mu$; again $\mu=0$.

Image not extracted

End of the proof

Proof of Theorem 1.1 for $n=35$. Cases (a), (b) and (c) of Lemma 6.2 exhaust the possibilities. Case (a) is impossible, and in cases (b) and (c) we have shown that $\mu=0$, in particular $s(1)=\mu_0=0$. The set $J=\{j:y_j=\pm1\}$ has $c_{29}(1)+c_{29}(-1)=D$ elements, and $s(1)=\sum_{j\in J}\pm x_j$. If $D=1$, then $s(1)=\pm x_j$ for one $j$, which is nonzero by Lemma 6.1. If $D=2$, then $s(1)=\pm x_j\pm x_k$ with $j\ne k$, which is nonzero because $x_j\ne\pm x_k$ by Lemma 6.1. Either way $s(1)\ne0$, a contradiction. □

Remark 6.3. Case (b) can also be excluded without the prime 71. In cases (b) and (c) the element $T_i$ of (2.3) for $\Gamma=\mathbb{F}_{29}$ is $A[0]+DS$ with integer coefficients, and $S^2=29S$, so the right side of (2.3) is $f_{35}(A)[0]$ plus an integer multiple of $S$. Comparing the coefficients at $[0]$ and $[1]$ with those of the left side $6mS$ gives $f_{35}(A)=0$. For $A>0$ this means $(A+1)(A+2)=210$, that is $A=13$, which rules out case (b), where $A=42$. Case (c) passes: with $A=13$ and $D=2$ the right side is exactly $12354S=6mS$. Likewise the distribution of Lemma 6.1 gives $T_i=S F_{71}$ and a right side $5046S F_{71}=6\cdot841S F_{71}$, as required. So each of the two distributions of Figure 3 satisfies the projected identity (2.3) exactly, as Xiao and Zhou observed [18 Example 5.14], and only the joint projection of Section 6.4 sees that they cannot occur together.

Formal verification

Theorem 1.1 has been formalized in Lean 4 [12] with the Mathlib library [14]. The formal statement defines a lattice tiling of $\mathbb{Z}^n$ by $B^n(r)$ as a subgroup $L$ of $\mathbb{Z}^n$ such that every $x\in\mathbb{Z}^n$ has exactly one $l\in L$ with $\sum_j|x_j-l_j|\le r$, and it asserts that no such subgroup exists for $(n,r)=(35,3)$ or $(805,3)$. The proof follows § 2–§ 6. Lemma 2.2, Proposition 2.3 for an arbitrary commutative ring, Lemmas 2.4 and 2.6, Proposition 3.1, Lemmas 3.2 and 3.4, Lemma 4.1 for $p=29$, and the arguments of § 5 and § 6 are proved there, and the finite computations in $\mathbb{F}_{29}$, $\mathbb{F}_{71}$ and $\mathbb{Z}/841$, among them Table 1, are checked by the kernel. Two steps are argued differently there: the left side of (2) in § 6.4 is shown to vanish by pairing each element $x$ of a fibre of $\psi_2$ with $2x_0-x$ for a fixed $x_0$ in that fibre, and the system (9) is solved by an explicit linear combination of its twenty-eight equations. Both theorems depend only on the standard axioms of Lean, namely propositional extensionality, choice and quotient soundness. The numbers in § 5 and § 6 were also recomputed independently by the programs archived with the formalization [2].

Data and code availability

The \LaTeX source of the paper, the Lean 4 formalisation of Theorem 1.1 described in § 7, and the C, C++, Python, Julia and shell programs that recompute the finite quantities of § 5 and § 6 are archived at Zenodo under doi:10.5281/zenodo.23398805 [2]; the paper is available at https://github.com/creelie/refactored-waddle/blob/main/preprintGolombWelchRadiusThree/GolombWelchRadiusThree.pdf. Deep Bhattacharjee carried out the computations and the Lean, Julia, C, C++, Python and shell verifications, and the proofs and the text were drafted, with AI assistance (Claude, Anthropic); both authors approved the final version.

Ethical declarations

Funding: none. Competing interests: none.

Formerly, Electro-Gravitational Space Propulsion Laboratory (EGSPL), Bhubaneswar, Odisha 751030, India; Formerly, University of Calcutta, Senate House, 87/1 College Street, Kolkata 700073, West Bengal, India

Email address: [email protected]

Email address: [email protected]

URL: https://orcid.org/0000-0003-0466-750X

Formerly, National Taiwan University, Taipei 106319, Taiwan

Email address: [email protected]

URL: https://orcid.org/0009-0002-2254-3914