The following describes the scope of the Lean formalization related to the following accompanying paper(s):
Scope
The formalization proves optimal-order mixing of the Thorp shuffle on \(2^d\) cards. After \(1600d\) complete shuffles, the full permutation law converges in total variation to uniform as \(d\to\infty\), uniformly over initial decks. Together with the support lower bound of \(2d-O(1)\), this gives mixing time \(\Theta(d)=\Theta(\log(2^d))\).
The linked supporting results include frame and conditional-list estimates, regular trace and spectral bounds, signed moments, and full-density \(L^2\) control. They also bound reciprocal Specht-dimension sums and give the eight-block Fourier estimate used in the mixing argument.
The formalized supporting result turns bounds on partial-permutation cosets into Fourier bounds. Partition a finite set into \(b\ge1\) nonempty blocks, and let \(f\ge0\) be a subprobability weight on its symmetric group whose left-coset masses for each block subgroup are at most \(B\). For every irreducible unitary representation of dimension \(D\) and every \(u>0\), both the squared Hilbert–Schmidt norm and squared operator norm of its Fourier transform are at most \(bB\,C(u)D^{-1+(u+2)/b}\), where \(C(u)\) is the stated symmetric-group degree constant.
The paper's asymptotic conclusion about the product of two random permutations is outside this selected finite estimate.
The formalized results give averaged conditional mixing for half-permutations in the revealed-path model and full-deck mixing for the Thorp shuffle. In particular, the full-deck total-variation distance tends to zero after \(16040400d\) steps on \(2^d\) cards, uniformly over deterministic initial decks. The conditional estimate is averaged over the actual outside-path law, rather than asserted for each individual environment. The formalization also includes the associated overlay, reset minorization, and two-color conditional constructions.
The formalization covers nine routing and representation estimates for Thorp sweeps: adaptive operator and fourth-trace bounds, Casimir moments, dense truncation, sparse contact, harmonic-cycle contraction, smoothing, and three tail or sparse-saving estimates. They bound routing-density deviations and Fourier operators in dense and sparse regimes, including exponential savings in the level scale and representation dimension.
The conditional high-height estimate requires a sufficiently large cutoff height \(J\) that exceeds twice the number \(s\) of coordinates in the fixed low block, so \(J>2s\). These are the earlier nine statements associated with the paper; its changed later statements and six other result blocks are outside this scope.
The formalization proves uniform representation bounds for one coordinate sweep of the Thorp shuffle. For each irreducible representation of dimension \(D\), it chooses a weight between \(D^{3/4}\) and \(D\) and a Schatten exponent bounded by one absolute constant so that the weighted Schatten moment is at most one. The sweep's operator norm is consequently at most \(D^{-c}\) for one absolute \(c>0\).
The supporting row–column estimate bounds the total squared overlap over all multiplicity copies on an occupied board, with explicit dependence on the row and column representation dimensions, the global dimension, the number of missing cells, and the number of rows or columns containing the global Young diagram. The paper's full physical-mixing conclusion is outside these selected representation estimates.
The formalization proves a uniform trace-smoothing estimate for coordinate sweeps of the Thorp shuffle on \(2^d\) cards. One absolute sweep parameter works for every \(d\ge1\): the regular trace is at most \(1+(2^d)^{-10}\), and the full permutation law after the corresponding fixed number of sweeps is within \(\tfrac12(2^d)^{-5}\) of uniform in total variation, for every initial deck. Thus the selected upper bound uses \(O(d)\) physical shuffles.
The formalized result is the weighted compatibility theorem for balanced \(A\times D\) rectangles, with \(n=AD\) and \(\sqrt n/2\le A,D\le2\sqrt n\). For arbitrary nonnegative weights on the row and column permutation groups, the normalized compatibility average is bounded by \(\exp(C_0n^{54/100})\) times the product of the marginal \(L^{1/\theta}\) factors, where \(\theta=1-L/\log\sqrt n>0\) and the constants are absolute. Compatibility means injectivity in every original column. The bounded regular-moment and other moment/rank conclusions are not included.
The formalization gives signed representation estimates for coordinate sweeps of the Thorp shuffle. For every signed occurrence of a Young diagram of size \(2^d\), it bounds the logarithm of a fixed-order weighted sweep moment by a small multiple of the signed partition entropy plus an explicit remainder-size budget. The moment order is uniform over the diagrams and decompositions after the two small coefficients are fixed.
The linked supporting angle bound controls the overlap of row, column, and global signed-type projections on an occupied rectangle, with explicit entropy, dimension, and missing-cell factors. These selected estimates support the paper's full-density argument; the full \(L^2\) and total-variation mixing conclusion is outside them.
The formalized binary-sweep theorem gives a universal power contraction in every irreducible representation: for sufficiently large \(d\), the averaged sweep on \(2^d\) slots has operator norm at most \(D^{-g}\) in representation dimension \(D\), for some \(g>0\). The sign expectation is zero, and a fixed number of independent sweeps approaches uniform in total variation from every initial deck. A separate conditional moment estimate covers allowed power-of-two grids and disjoint coordinate-respecting trajectories, with its stated feasibility premise. Physical-shuffle law identification is not included.
The formalization proves the paper's strict four-row permanent inequality. There are constants \(4/3<p<2\) and \(\varepsilon>0\) such that every probability law on \(S_4\) within total-variation distance \(\varepsilon\) of uniform, and with exactly uniform coordinate marginals, satisfies the permanent bound by the product of the four \(L^p\) row norms for every nonnegative matrix. The exponent and neighborhood are uniform over those laws. The Thorp mixing consequence is outside this selected statement.
Comparator links
