Zhi-Wei Sun’s OEIS A228884 composite gcd-determinant bound

Abstract

Prime divisors of composite gcd determinants are smaller than the index.

Definition 1.1 (The gcd-entry matrix).

$$\forall n\in \mathbb{N},\forall i\in \mathrm{Fin}\left(n\right),\forall j\in \mathrm{Fin}\left(n\right),C\left(n\right)\left(i,j\right)=(\mathrm{Int}.\gcd \left(((\mathrm{val}\left(i\right):\mathbb{Z})+1)-((\mathrm{val}\left(j\right):\mathbb{Z})+1),(n:\mathbb{Z})\right):\mathbb{Z})$$

Formalization. D5/S3/Arith/Divisors/SunA228884.C (✓ std3).

Citation. Zhi-Wei Sun (2013). Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n. URL: https://oeis.org/A228884/internal.

Commentary.

OEIS A228884 NAME, page not numbered: “Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n.” The source program is “a[n_]:=Det[Table[GCD[i-j,n],{i,1,n},{j,1,n}]]”. The Lean expression uses Fin n labels, adds one to each label, performs integer subtraction, and applies Int.gcd before casting the result to the matrix entry type.

Definition 1.2 (The determinant sequence).

$$\forall n\in \mathbb{N},D\left(n\right)=\mathrm{Matrix}.\det \left(C\left(n\right)\right)$$

Formalization. D5/S3/Arith/Divisors/SunA228884.D (✓ std3).

Citation. Zhi-Wei Sun (2013). Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n. URL: https://oeis.org/A228884/internal.

Commentary.

OEIS A228884 NAME, page not numbered: “Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n.” D n is Matrix.det of C n, including the empty determinant at n=0.

Definition 1.3 (The composite-index prime-divisor conjecture).

$$claim=\left(\forall n\in \mathbb{N},(4\le n)\Rightarrow ((\neg (\mathrm{Nat}.\mathrm{Prime}\left(n\right)))\Rightarrow (\forall q\in \mathbb{N},(\mathrm{Nat}.\mathrm{Prime}\left(q\right))\Rightarrow (((q:\mathbb{Z})\mid D\left(n\right))\Rightarrow (q<n))))\right)$$

Formalization. D5/S3/Arith/Divisors/SunA228884.claim (✓ std3).

Citation. Zhi-Wei Sun (2013). Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n. URL: https://oeis.org/A228884/internal.

Commentary.

OEIS A228884 COMMENTS clause (ii), page not numbered: “(ii) For any composite number n, all prime divisors of a(n) are smaller than n.” The source definition is encoded with n ≥ 4, ¬Nat.Prime n, integer divisibility of D n by the natural prime q, and q < n.

Theorem 1.4 (The prime-divisor bound holds).

$$\forall n\in \mathbb{N},(4\le n)\Rightarrow ((\neg (\mathrm{Nat}.\mathrm{Prime}\left(n\right)))\Rightarrow (\forall q\in \mathbb{N},(\mathrm{Nat}.\mathrm{Prime}\left(q\right))\Rightarrow (((q:\mathbb{Z})\mid D\left(n\right))\Rightarrow (q<n))))$$

Proof. Machine-checked in Lean as D5/S3/Arith/Divisors/SunA228884.result (✓ std3). ∎

Resolves. Problems/sun228884 (proved) by D5/S3/Arith/Divisors/SunA228884.result.

Source. Repository-derived.

Acknowledgement. Zhi-Wei Sun (2013). Determinant of the n X n matrix with (i,j)-entry equal to the greatest common divisor of i-j and n. URL: https://oeis.org/A228884/internal.

Commentary.

CRT reindexing gives D(uv)=D(u)^v D(v)^u for coprime positive u and v. The gcd Fourier transform factors over prime powers, and its local eigenvalue products at exponent at least two have prime divisors below the local order. Exponent-one factors are bounded by 2p-1 and the remaining cofactor in a composite index supplies 2p ≤ n.

The proof therefore establishes the complete statement for every n ≥ 4 with ¬Nat.Prime n. Positivity and the separate divisibility clause of the OEIS entry are not asserted here.

References

• Truth anchor: D5/S3/Arith/Divisors/SunA228884.C
• Truth anchor: D5/S3/Arith/Divisors/SunA228884.D
• Truth anchor: D5/S3/Arith/Divisors/SunA228884.claim
• Truth anchor: D5/S3/Arith/Divisors/SunA228884.result
• Dependency: D5/S3/Analytic/Certified/FiniteRamanujanDivisorIdentity
• Dependency: D5/S3/Arith/RoldanCirculantEnergyP2Q3
• Dependency: D5/S3/ConceptDynamics/Coding/CountedOriginalOrbitGyration
• Dependency: D5/S3/Quantum/Matrix/CirculantCharpoly