← All papers
The Godsil–McKay Asymptotic for Latin Rectangles in the Sublinear Range of Erdős Problem 725
math.CO
Aug 3, 2026 · v1
math.PR
TL;DR
The asymptotic enumeration results for k×n Latin rectangles across the full sublinear range are formally verified in Lean.
Abstract
Erdős Problem 725 asks for an asymptotic formula for the number $L_{k,n}$ of ordered, labelled $k\times n$ Latin rectangles. Godsil and McKay proved that $L_{k,n}\sim (n!)^k((n)_k/n^k)^n(1-k/n)^{-n/2}e^{-k/2}$ for $k=o(n^{6/7})$. We provide a partial solution to Erdős Problem 725 by proving this asymptotic for every $k=o(n)$. More precisely, set $\widetilde A_{k,n}=(n!)^k((n)_k/n^k)^n\exp\{[n(H_n-H_{n-k})-k]/2\}$. For every $K(n)=o(n)$, uniformly for $0\leq k\leq K(n)$, we prove $\log(L_{k,n}/\widetilde A_{k,n})=O(k^2/n^2)$, with an absolute implied constant. The results of this paper have been formally verified in Lean.
Problem
Erdős Problem 725 asks for an asymptotic formula for the number L_{k,n} of ordered labelled k×n Latin rectangles. Godsil and McKay proved the asymptotic only for k=o(n^{6/7}).
Approach
The enumeration is split into a universal analytic permanent-approximation theorem and a Latin-specific probabilistic component. A small-line-norm permanent approximation resums the cycle sector of a matching expansion, while a fixed-anchor incomplete-column-path switching controls the fourth Schatten moment of the centred incidence matrix. A one-row extension estimate is telescoped over rows.
Results
The Godsil–McKay asymptotic is established for every k=o(n), with log(L_{k,n}/Ã_{k,n})=O(k^2/n^2) uniformly for 0≤k≤K(n)=o(n). All results have been formally verified in Lean.