Weak Typicality of von Neumann Entanglement Entropy in Gaussian Boson Sampling

Abstract

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 $\alpha \ge 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 $\epsilon >0$ and all sufficiently large $n$, $\mathbb{P}\left(\left|\frac{S_{1,n}}{\mathbb{E}{S}_{1,n}}-1\right|\ge \epsilon \right)\le 2\exp \left[-\frac{c_{s,r}{\epsilon }^2{n}^2}{{\log }^2(en)}\right].$ The proof represents the entropy as a singular value statistic of a principal block of $U{U}^{\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.

19 pages, 1 figure, 1 table. Accompanying Lean 4 formalization available at https://doi.org/10.5281/zenodo.21969265