Composite prime divisors of the gcd determinant

Zhi-Wei Sun's OEIS A228884, COMMENTS clause (ii), states: “For any composite number $n$, all prime divisors of $a(n)$ are smaller than $n$.” The source defines $a(n)$ as the determinant of the $n\times n$ matrix whose $(i,j)$ entry is $gcd(i-j,n)$ for $1\leq i,j\leq n$.

The formal claim uses the literal integer-entry matrix C, its determinant D, the hypotheses $4\leq n$ and $\neg\operatorname{Nat.Prime}(n)$, and integer divisibility by a natural prime $q$.

Statement echo

The settling declaration is D5/S3/Arith/Divisors/SunA228884.result : D5/S3/Arith/Divisors/SunA228884.claim. Its Scribe mirror expands the complete proposition, including every binder and the integer cast in the divisibility clause.

The result settles the composite-index prime-support assertion for the source's gcd determinant while retaining the source's separate positivity and divisibility assertions as distinct questions.

The source entry contains no proof of clause (ii). The settlement supplies the unbounded proof for every composite index represented by the formal claim. Priority and completeness beyond the cited OEIS source remain ASSUMED-UNVERIFIED.

CRT reindexing gives $D(uv)=D(u)^vD(v)^u$ for coprime positive $u,v$. The gcd Fourier transform gives an integer eigenvalue product on each prime-power component. For exponent at least two, every prime divisor of a local factor is below the prime power; exponent-one factors are bounded by $2p-1$, and the remaining composite cofactor gives $2p\leq n$.

An index $n\geq4$ with $\neg\operatorname{Nat.Prime}(n)$ and a natural prime $q\mid D(n)$ with $q\geq n$ would refute the settled claim. The finite checks below are evidence for bounded ranges only and do not replace the kernel proof.

The Lean kernel checks D5/S3/Arith/Divisors/SunA228884.result with the standard axiom closure. The experiment repository entry sun-a228884-gcd-determinant-primes is pinned to commit a2d67e289ac6b31fce4e18bc3e0273dd4c4a94d6. Running python3 docs/reports/sun-a228884-gcd-determinant-primes/check.py from that commit exits 0 and ends ALL_CHECKS_OK; the script SHA-256 is 92efdf754f9f73d705703344048e640a64770abc322680735446e689633787aa.

The escape audit for the settling declaration is unfinished under issue #22671.

Related literature: abstract screening

Sburlati, On prime factors of determinants of circulant matrices, Linear Algebra and its Applications 432 (2010), 100–106, DOI 10.1016/j.laa.2009.07.029. The abstract concerns the probability that a prime $p$ divides the determinant of a random integer circulant matrix of order $n$, under $p\nmid n$. It does not state the composite-index prime-support assertion A228884(ii).

Yangklan–Laohakosol–Mavecha, Integer factorization and finite Fourier series expansion, Lithuanian Mathematical Journal 61 (2021), 274–284, DOI 10.1007/s10986-020-09506-5. The abstract concerns counts of factorizations modulo an integer $k$, obtained through finite Fourier expansions of functions involving greatest common divisors. It does not state A228884(ii).

These are abstract-level readings supplied by the source and literature checks. Neither full text has been read for this settlement; the abstract screening does not exclude a relevant result in either full text and does not establish complete prior-art clearance.

What the settlement shows

| item | status | evidence | | --- | --- | --- | | CRT isolates prime-power components; the gcd DFT makes each component an integer eigenvalue product. | proved | D5/S3/Arith/Divisors/SunA228884.D_coprime, D_spectral, and D_prime_power are compiled declarations in the settling module. | | The live helper all_support proves $q<2n$ for every positive $n$ whenever prime $q$ divides $D(n)$, and $q<n$ when $n$ is nonprime. | proved | D5/S3/Arith/Divisors/SunA228884.all_support, used by result. | | For prime powers of exponent at least two, every local prime divisor is below the prime power. | proved | D5/S3/Arith/Divisors/SunA228884.E_higher_support, used by prime_power_support. | | $D_2=3$ and $D_3=20$ show the composite hypothesis is necessary; $D_6=10800$ has prime divisor 5, so $q<n-1$ fails uniformly. | computed | python3 docs/reports/sun-a228884-gcd-determinant-primes/check.py, exit 0, script SHA-256 above; scope $n=0,\ldots,60$. | | $p=2,a=2$ gives $B_a=p^a=4$; the proof excludes equality by primality. | computed | The same script, exit 0, checks the local bound for prime $p\leq97$ and exponents $2\leq a\leq10$. | | Sharper bounds, other arithmetic circulants, and the separate full divisibility assertion in clause (i) are outside this settlement. Positivity has Petrov's separate published proof. | open | No declaration in this module asserts these extensions; literature completeness is ASSUMED-UNVERIFIED. |

The experiment's exact tested scopes are $n=0,\ldots,60$, 199 ordered coprime pairs with $uv\leq60$, 42 composite indices in $4\leq n\leq60$, and 225 local cases with prime $p\leq97$ and $2\leq a\leq10$.

• Complete literature and citing-work enumeration for the OEIS-only source.
• Full text of the identified related papers and all later Sun papers.
• Exhaustive comparison with journal versions and MathOverflow comments.
• Any priority or novelty claim beyond the source and repository evidence cited above.