← All papers
First page of Spectral extremes under exact cycle conditioning

Spectral extremes under exact cycle conditioning

Zhipeng Lu

math.CO Sep 11, 2026 · v1 math.PR
The full argument, including the main theorem and corollary over the finite permutation model, was formalized and kernel-checked in Lean 4.
Let $P_n$ be the matrix of a random permutation of $n$ symbols and let $M_n=\log\max_{|z|=1}|\det(I-zP_n)|$. Cook and Zeitouni proved that $M_n/\log n$ converges in probability to a constant $x_0$ for a uniform permutation. We show that the $\sqrt{\log n}$ fluctuations of $M_n$ are carried entirely by the number of cycles $K_n$. Write $λ(s)=\log\{Γ(1+s)/Γ(1+s/2)^2\}$, let $s_κ$ minimize $(1+κλ(s))/s$ on $(0,\infty)$, and put $v(κ)=κλ'(s_κ)$ and $a_θ=λ(s_θ)/s_θ$. Under the Ewens measure with any fixed parameter $θ>0$ we prove $M_n=v(θ)\log n+a_θ(K_n-θ\log n)+O_P(\log\log n)$, so that the standardized pair $(K_n,M_n)$ converges jointly to $(G,G)$ with $G$ standard normal: the maximum and the cycle count are asymptotically perfectly aligned. This is deduced from a statement about the exact conditional law, which does not depend on $θ$: for every compact $[κ_-,κ_+]\subset(0,\infty)$ there is a finite $C$ such that $P(|M_n-v(k/\log n)\log n|>C\log\log n \mid K_n=k)$ tends to $0$ uniformly over integers $k$ with $κ_-\log n\le k\leκ_+\log n$, that is, over exact and possibly atypical cycle counts. The proof keeps the size and the cycle count simultaneously in a two-variable coefficient extraction. Cycles longer than $n/(\log n)^4$ are reserved as an analytic factor whose coefficients are flat under every size shift produced by the shorter cycles; positivity then converts a scalar coefficient asymptotic into a relative comparison of the entire path-constrained measure, with an error that does not degrade with the number of constraints or with the rarity of the event. The constrained lower bound comes from pointwise saddle estimates for killed convolutions along a dyadic chain of endpoint boxes.

For a random permutation matrix P_n, study the maximum modulus M_n = log max_{|z|=1}|det(I-zP_n)| of the characteristic polynomial on the unit circle. The goal is to describe the sqrt(log n) fluctuations of M_n and their relation to the cycle count K_n under the Ewens measure.

The characteristic polynomial is factored along cycles and the field is analyzed as a log-correlated process governed by a Legendre transform of lambda(s)=log{Gamma(1+s)/Gamma(1+s/2)^2}. The proof performs a two-variable coefficient extraction keeping both size and cycle count constrained, reserving long cycles as an analytic reservoir and using positive coefficient transfer plus pointwise saddle estimates for killed convolutions. The mathematical development was translated into Lean 4 and verified.

Under the Ewens measure with any fixed theta>0, M_n = v(theta)log n + a_theta(K_n - theta log n) + O_P(log log n), so the standardized pair (K_n, M_n) converges jointly to (G,G) with G standard normal. A uniform conditional localization holds over exact and atypical cycle counts. The Lean formalization covers the conditional law, Theorem 1.1 and Corollary 6.1, checked with trust=0 using only propext, Classical.choice and Quot.sound.