AI 中文总结
该研究解决了高斯玻色采样中冯·诺依曼纠缠熵的比例弱典型性问题，通过正则化奇点和幺正群集中不等式完成证明，给出概率界、收敛性及方差界结果，且有Lean 4开发验证证明链。
AI 中文摘要
我们研究由哈尔分布的无源干涉仪作用于n个等压缩输入模式（具有固定非零压缩强度s）所产生的冯·诺依曼纠缠熵。此前的工作已建立了整数Rényi阶α≥2的比例弱典型性，并给出了次线性的冯·诺依曼结果，而比例冯·诺依曼情形仍未解决。对于满足k_n/n→r∈(0,1)的k_n模式子系统，我们证明：对任意ε>0及所有足够大的n，有P(|S_{1,n}/E[S_{1,n}] - 1|≥ε)≤2exp[-c_{s,r}ε²n²/log²(en)]。该证明将熵表示为UU^T主块的奇异值统计量（其中U为幺正干涉仪），它正则化了对应纯高斯模式端点处的对数奇点，并应用了幺正群上的集中不等式。该结果确立了比例冯·诺依曼弱典型性，进一步意味着S_{1,n}/E[S_{1,n}]几乎必然收敛于1、典型体积定律，以及方差界Var(S_{1,n})=O_s(log²n)。配套的Lean 4开发验证了证明链。
英文摘要
We study the von Neumann entanglement entropy generated by a Haar distributed passive interferometer acting on $n$ equally squeezed input modes with fixed nonzero squeezing strength $s$. Previous work established proportional weak typicality for integer R'enyi orders $α\geq 2$ and stated a sublinear von Neumann result, while the proportional von Neumann case remained open. For a subsystem of $k_n$ modes satisfying $k_n/n\to r\in(0,1)$, we prove that, for every $\varepsilon>0$ and all sufficiently large $n$, $\mathbb{P}\left(\left|\frac{S_{1,n}}{\mathbb{E}S_{1,n}}-1\right|\geq\varepsilon\right)\leq2\exp\left[-\frac{c_{s,r}\varepsilon^2n^2}{\log^2(en)}\right].$ The proof represents the entropy as a singular value statistic of a principal block of $UU^{\mathsf T}$, where $U$ denotes the unitary interferometer. It regularizes the logarithmic singularity at the endpoint corresponding to a pure Gaussian mode and applies concentration on the unitary group. The result establishes proportional von Neumann weak typicality and further implies almost sure convergence of $S_{1,n}/\mathbb{E}S_{1,n}$ to $1$, a typical volume law, and the variance bound $\mathrm{Var}(S_{1,n})=O_s(\log^2 n)$. An accompanying Lean 4 development verifies the proof chain.
Comments19 pages, 1 figure, 1 table. Accompanying Lean 4 formalization available at https://doi.org/10.5281/zenodo.21969265
