Sharp Berry-Esseen Bounds for the Log Determinant of a Gaussian Sample Correlation Matrix

Let $\widehat{R}$ be the Pearson sample correlation matrix formed from $n$ independent Gaussian observations in $p$ dimensions, and write $m=n-1\ge p$. Under the null correlation $R=I_p$, the classical independent beta product, exact cumulants, and full Fourier inversion yield, along every sequence $p\to \mathrm{\infty }$ with $m\ge p$, a uniform first Edgeworth expansion for $\log \det \widehat{R}$, centered by its exact mean and scaled by its exact standard deviation. The expansion identifies the exact finite dimensional skewness correction and gives the sharp Kolmogorov equivalent $A_{m,p}\mathrm{/}\{6\sqrt{2\pi }{V}_{m,p}^{3\mathrm{/}2}\}$, where $V_{m,p}$ is the exact variance and $A_{m,p}$ is the absolute third cumulant. This equivalent unifies the square, fixed gap, growing gap, proportional, and dilute regimes; in the square regime the error has order $(\log p{)}^{-3\mathrm{/}2}$ with an exact constant. For every positive definite population correlation matrix $R$, we prove a uniform finite sample Berry-Esseen bound that explicitly tracks population dependence. All theoretical results have exact or proved equivalent Lean 4 formulations whose declarations and dependencies are kernel checked.