Papers With

← All papers
First page of Comments on "Multidimensional Costas Arrays and Their Periodicity"

Comments on "Multidimensional Costas Arrays and Their Periodicity"

Shiv Munagala

cs.IT Oct 25, 2026 · v1 math.CO
formalization combinatorics ai-agents
Read PDF arXiv abstract
TL;DR
The counterexample to the Rubio–Torres conjecture is formalized in Lean 4 and checked by kernel evaluation (decide +kernel), with the Lean proof written by Claude.
Abstract
Rubio and Torres conjectured that a multidimensional Costas array, defined by a bijection between two boxes of integer points whose domain has at least as many dimensions as its image, can stay Costas in every window of its periodic extension only if its order is a power of two fixed by the dimension of the domain. We give a four-dimensional periodic Costas array of order $6$, with a two-dimensional domain and a two-dimensional image, so the conjecture is false. The verification reduces to $36$ windows. It has been confirmed by computer and in the Lean proof assistant. The array also meets with equality the pigeonhole bound that Rubio and Torres use for their non-existence results, so that bound is tight.
Problem

Rubio and Torres conjectured that a multidimensional periodic Costas array whose domain has at least as many dimensions as its image must have order 2^k, where k is the domain dimension. The conjecture is also listed as AIM problem 627.

Approach

An explicit four-dimensional array of order 6 is given, built from a bijection between two copies of the box [2]×[3]. A periodicity lemma reduces the check to 36 residue windows, each containing six dots with 30 difference vectors. A script checks the result and also tests all offsets in {-6,…,6}^4 directly. The statement is formalized in Lean 4 and proved by kernel decision, depending only on the standard axioms.

Results

The order-6 periodic Costas array disproves the conjecture in dimension m=4, the smallest dimension not covered by the known non-existence results. The array meets the pigeonhole bound of Rubio–Torres Theorem 3 with equality, so that bound is tight.