结果族 238：Optimal logarithmic mixing of the Thorp shuffle · 学科：Probability and statistical mechanics · 验证状态：主结果已 Lean 形式化
证明洗牌快，有种套路是”先剧透再看”：先亮出几张牌各自怎么走，再检查剩下的随机安排像不像均匀。麻烦在于剧透会改变剩余部分的概率——这篇论文把这笔”剧透税”精确入账，再用复分析的最大值原理，把好估计从一个人造模型”搬运”到真正的 Thorp 洗牌。
关键词卡片
@@M@@u@@ 个座位的组合账单 @@M@@(m)_u=m(m-1)\cdots@@，剧透越多账越贵看个具体例子
剧透税有多便宜？在一条 @@M@@m=64@@ 的线上指定 @@M@@u=3@@ 张牌的落点，代价 @@M@@C=\ln\frac{64^3}{64\cdot63\cdot62}\approx0.047@@——只多付约 5%。再看搬运：把扫掠掺进参数 @@M@@z@@（@@M@@z=0@@ 是均匀线律、好证，@@M@@z=1@@ 是二进制真扫掠、要证的目标），矩阵系数 @@M@@f(z)@@ 在 @@M@@z=0@@ 附近有维数节省、在某个圆周上范数 @@M@@\le1@@；在挖去实轴一线段的圆盘上对 @@M@@\log|f|@@ 用最大值原理，节省便搬到 @@M@@z=1@@。结论：@@M@@\|K_\lambda\|_{\rm op}\le D_\lambda^{-g}@@，固定次数扫掠后全变差趋于零，@@M@@t_{\rm mix}=\Theta(d)@@。
为什么值得关心
“条件矩＋复分析搬运”的组合拳是本族被机器验证的骨干路线，也成为伙伴论文反复借用的证明模板。
已 Lean 形式化
第一级台阶
入门导读的比喻是”先剧透再看”：先亮出几张牌各自的完整走线，再检查剩下的随机安排像不像均匀。半数学地说：对象是剧透之后剩下的那份随机性——每个阶段还没被占用的座位之间的对应关系；操作是先固定一批牌的轨迹，再估计这个剩余对应表。剧透会改变剩余选择的概率，导读里那笔”剧透税”，就是不许重复地指定座位所要多付的组合账。
第二级台阶
精确化这些对象：把指定轨迹的全体记作族 @@M@@\mathcal H@@，一个有序扫掠里牌的输入输出唯一决定其路径，可行性即各层强制路径互不撞位。剩余随机性是一个双射，其收缩用 Schatten 矩（算子幂的迹）度量。为了让”好证的”与”要证的”之间有连续过渡，把每条线上的律换成掺混 @@M@@(1-z)U_m+zB_m@@：@@M@@z=0@@ 是均匀置换（好证），@@M@@z=1@@ 是真正的二进制扫掠（目标）。剧透税在尺寸 @@M@@m@@ 的线上、指定 @@M@@u@@ 个落点时为 @@M@@\log\bigl(m^u/(m)_u\bigr)@@，其中 @@M@@(m)_u=m(m-1)\cdots@@ 是下降阶乘；全轨迹族求和记 @@M@@C(\mathcal H)@@。
第三级台阶
条件定理对线尺寸取自固定区间 @@M@@[R,R^2]@@ 的二的幂、小实区间 @@M@@0\le z\le z_*@@、任意可行 @@M@@\mathcal H@@ 陈述：剩余双射在每个不可约表示中的 Schatten 矩有一致上界，含三块——正比于 @@M@@-\log D_\lambda@@ 的维数节省、指定牌数的容许项、以及 @@M@@-C(\mathcal H)@@；正是这项差值让”再剧透一批路径”时估计保持稳定，归纳得以对所有条件律同时成立。随后取 @@M@@\mathcal H=\varnothing@@：无条件扫掠算子是 @@M@@z@@ 的矩阵多项式，在实区间上有维数节省，在半径大于一的圆盘上范数不超过一（立方体边对换生成整个对称群给出的谱隙）；在挖去实线段的圆盘上对矩阵系数用次调和最大值原理，把节省搬到 @@M@@z=1@@，得 @@M@@\|K_\lambda\|_{\rm op}\le D_\lambda^{-g}@@。配上支撑下界 @@M@@2d-O(1)@@，混合时间为 @@M@@\Theta(\log N)@@。
本文先对”给定了部分牌轨迹”的条件坐标扫掠证明一个普适的 Schatten 矩估计，再用次调和最大值原理（subharmonic maximum principle）把近均匀线律下的收缩解析转移到二进制扫掠，证明固定次数扫掠即可混合 @@M@@2^d@@ 张牌的 Thorp 洗牌，混合时间 @@M@@O(d)@@ 与支撑下界同阶。
Thorp 洗牌把 @@M@@N=2^d@@ 张牌按二进制位置配对、独立掷币交换；剥离确定性坐标旋转后，一次坐标扫掠（coordinate sweep）恰是 @@M@@d@@ 次物理洗牌。混合时间问题此前卡在 Morris 的 @@M@@O(d^3)@@ 物理洗牌（更早有 @@M@@O(d^{44})@@、@@M@@O(d^{29})@@、@@M@@O((\log N)^4)@@），而硬币串计数只给出下界 @@M@@2d-O(1)@@。以往的分析——Morris 的变色龙过程与熵收缩、Morris–Rogaway–Stegers 与 Czumaj–Vöcking 对部分牌的研究——都靠”揭示牌的运动信息”来组织证明，但揭示路径会改变剩余选择的概率律。本文的关键是控制揭示路径之后剩下的整个随机双射（bijection），并精确支付”无放回地指定位置”的费用，使估计在证明过程中反复揭示更多路径时保持稳定。
论文的二元结论是：存在绝对常数 @@M@@g>0@@ 与 @@M@@d_0@@，使对一切 @@M@@d\ge d_0@@ 与 @@M@@\lambda\vdash 2^d@@，扫掠算子在不可约表示（irreducible representation）中的 Fourier 系数满足 @@M@@\|K_\lambda\|_{\op}\le D_\lambda^{-g}@@，且 sign 表示被完全消灭；于是存在绝对正整数 @@M@@w@@，使 @@M@@w@@ 次独立扫掠后与均匀律的全变差距离对一切确定性初始牌序一致趋于零。配合支撑障碍 @@M@@\|q_d^{*t}-U_N\|_{\TV}\ge1-2^{tN/2}/N!@@（@@M@@t@@ 次物理洗牌只有 @@M@@2^{tN/2}@@ 个硬币串），得 @@M@@t_{\rm mix}(d)=\Theta(d)@@。核心输入是条件定理：对线尺寸取自固定区间 @@M@@[R,R^2]@@ 内 2 的幂、线律为混合 @@M@@(1-z)U_m+zB_m@@ 的有序扫掠网格，对任何可行的指定轨迹族 @@M@@\mathcal H@@，剩余随机双射在每个不可约表示中的 Schatten 矩都有一致界，界含三项：正比于 @@M@@\log D_\lambda@@ 的负项、指定牌数的容许项，以及无放回修正 @@M@@C(\mathcal H)=\sum\log\bigl(m^u/(m)_u\bigr)@@，其中 @@M@@(m)_u@@ 是下降阶乘（falling factorial）。
证明分四大步。第一步证条件定理的稀疏层：对只在跟踪少数牌时才首次出现的表示类型，把放置概率对其子集交错求和，使任何与其余轨迹不共享阶段线的被跟踪路径相消；坐标很多时用有根森林计数说明”所有被跟踪路径都共享某条线”概率很小；坐标数有界时线更长、此计数失效，改在 @@M@@z=0@@ 处用逆伽马矩恒等式把下降阶乘比写成期望，把共享同一条线的粒子分组后再取矩；固定 @@M@@R@@ 后只剩有限多个网格，用连续性把估计延拓到一个共同的小实区间。第二步处理大维数的钩型：把坐标分成两块、把网格看成矩形，第一块在行内扫、第二块在列内扫；在带号张量表示中，每个行或列同型投影（isotypic projection）被”迹为一的正定矩阵的张量幂的概率混合”的受控倍数控制；对所选行矩阵取平均得到一个迹一参考矩阵，用以界定行、列投影在自由格上的重叠；子矩估计恰好抵消该重叠中子群维数的成本，给出全钩型的更强估计。第三步是”增广路径”：当附加放置把 @@M@@\mathcal H@@ 增广为 @@M@@\mathcal H^+@@ 时，用差值 @@M@@C(\mathcal H^+)-C(\mathcal H)@@ 控制其转移概率；分支法则把杨图（Young diagram）去框的实现记录为这种放置，循环迹展开与 Hölder 不等式把原始的 @@M@@-C(\mathcal H)@@ 收回来，因此归纳必须对所有条件律同时成立。最后是解析转移：令 @@M@@\mathcal H=\varnothing@@，无条件扫掠算子是 @@M@@z@@ 的矩阵多项式，在实区间 @@M@@[0,z_*]@@ 上有维数节省 @@M@@D_\lambda^{-a_0}@@；另一方面，二进制线平均在非平凡不可约表示中有严格小于一的谱隙（立方体的边对换生成整个对称群），故在半径 @@M@@r>1@@ 的圆盘上算子范数不超过一。在去掉实线段 @@M@@[u,v]@@ 的圆盘上构造对数位势型的调和障碍 @@M@@G@@，对每个矩阵系数 @@M@@f(z)@@ 使用 @@M@@\log|f|@@ 的次调和性与边界最大值原理，把维数节省搬到 @@M@@z=1@@，即二进制扫掠本身。收尾用 Diaconis–Shahshahani 有限群 Fourier 分析，按 @@M@@k(\lambda)=\min(N-\lambda_1,N-\lambda'_1)@@ 分层、配合维数下界与划分计数控制求和，得到全变差收敛。
本篇在任务元数据中被标注为主结果已有 Lean 形式化证明，是结果族 238 中可信度最高的一条路线。两篇姊妹篇分别用带号张量熵预算与四行 permanent 不等式独立导出同一 @@M@@\Theta(d)@@ 混合阶，三种机制互相印证。即便如此，完整证明中的条件矩估计与解析转移细节，仍建议对照 Lean 形式化文档与社区核验来阅读。
问 1：证明中最关键、最脆弱的一步是哪里？
（答：两处联动。其一是”增广路径”归纳：新增放置把 @@M@@\mathcal H@@ 增广为 @@M@@\mathcal H^+@@ 时用差值 @@M@@C(\mathcal H^+)-C(\mathcal H)@@ 控制转移概率，分支法则把去框实现记录为这种放置，循环迹展开加 Hölder 不等式把原始的 @@M@@-C(\mathcal H)@@ 收回来——归纳因此必须对所有条件律同时成立。其二是解析转移：在挖去实线段 @@M@@[u,v]@@ 的圆盘上构造对数位势型障碍，对每个矩阵系数的 @@M@@\log|f|@@ 用次调和最大值原理。任何一处链条断裂，@@M@@z=1@@ 处的 @@M@@D_\lambda^{-g}@@ 都不存在。）
问 2：”剧透税”为什么恰好是 @@M@@\log(m^u/(m)_u)@@，这项的作用是什么？
（答：这是在同一尺寸 @@M@@m@@ 的线上无放回地指定 @@M@@u@@ 个不同座位相对有放回的组合代价。它是关键不变量：再揭示更多路径时，新账单与旧账单的差恰好控制新增放置的转移概率，使估计在反复剧透下稳定。）
问 3：为什么线尺寸要限制在固定区间 @@M@@[R,R^2]@@ 的二的幂上？
（答：稀疏层证明分两种情形——坐标多时用有根森林计数说明”所有被跟踪路径都共享某条线”概率小；坐标数有界时线更长、计数失效，改在 @@M@@z=0@@ 用逆伽马矩恒等式把下降阶乘比写成期望。固定 @@M@@R@@ 后这类网格只有有限多个，才能用连续性把估计延拓到共同的小实区间。@@M@@[R,R^2]@@ 正是这两种机制交接的可行窗口。）
问 4：与 Morris 的变色龙过程、熵收缩相比，真正新意是什么？
（答：前人揭示部分牌的运动信息后只控制所选牌的边缘律；本文控制揭示路径之后剩下的整个剩余双射，在每个不可约表示中给出带精确无放回修正的 Schatten 矩界，并首次用复分析（掺混参数 @@M@@z@@ 加最大值原理）把近均匀模型上的收缩搬到真二进制扫掠。）
问 5：作为 AI 生成的证明，最可能出错的模式是什么？
（答：典型风险在”软硬拼接”处：矩阵多项式在半径 @@M@@r>1@@ 圆盘上范数 @@M@@\le1@@ 依赖二进制线平均的严格谱隙（立方体边对换生成 @@M@@S_N@@），其常数必须对所有允许线尺寸一致；带号同型投影被”迹一正定矩阵张量幂的概率混合”支配的比较系数也是易错点。主结果已 Lean 形式化，风险相对可控，但条件矩估计的细节仍以 Lean 文档为准绳。）
问 6：这个结果谁会用到？
（答：族内多篇伙伴篇借用其”条件矩＋解析转移”模板；揭示路径的估计方式对小域加密中置换生成的可证明安全分析直接相关；显式 @@M@@1600d@@ 物理洗牌界在同族另文给出。）
问 7：sign 表示为什么被完全消灭，这一步重要吗？
（答：奇偶结构使一次扫掠的置换全为偶（或带固定奇偶性），sign 块的 Fourier 系数直接为零；消灭它才能让其余非平凡块的维数随 @@M@@d@@ 增长，使 @@M@@w@@ 次扫掠的误差经维数幂放大后趋于零。）
总评
这篇论文把”揭示信息改变条件律”这一老大难变成可记账的下降阶乘修正，并用次调和最大值原理完成从人造模型到真洗牌的搬运，主结果有 Lean 形式化，是族内骨干路线；最大风险是谱隙一致性与位势障碍构造等硬分析细节即便形式化也需人工复核其假设覆盖。