Metadata

slug: sun228884
bibkey: sun2013oeisa228884
doi: null
url: https://oeis.org/A228884/internal
triage: theorem
motivation_gids:
  - D5/S3/Arith/Divisors/SunA228884.result

Composite prime divisors of the gcd determinant

Problem

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 $g c d (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 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.

Motivation

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.

Gap

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.

Route

CRT reindexing gives $D (uv) = D (u)^{v} D (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 $2 p - 1$ , and the remaining composite cofactor gives $2 p \leq n$ .

Falsifier

An index $n \geq 4$ with $\neg Nat.Prime (n)$ and a natural prime $q ∣ 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.

Evidence

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.

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 ∤ 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.

Triage

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 < 2 n$ 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, \dots, 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 \leq 97$ and exponents $2 \leq a \leq 10$ .
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, \dots, 60$ , 199 ordered coprime pairs with $uv \leq 60$ , 42 composite indices in $4 \leq n \leq 60$ , and 225 local cases with prime $p \leq 97$ and $2 \leq a \leq 10$ .

ASSUMED-UNVERIFIED

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.

Keyboard shortcuts

trureturing — Discovering truth