Weak Typicality of von Neumann Entanglement Entropy in Gaussian Boson Sampling

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\mathrm{/}n\to r\in (0,1)$, we prove that, for every $\epsilon >0$ and all sufficiently large $n$, $\mathbb{P}(\mid \frac{S_{1,n}}{\mathbb{E}{S}_{1,n}}-1\mid \ge \epsilon )\le 2\exp [-\frac{c_{s,r}{\epsilon }^2{n}^2}{{\log }^2(en)}]\mathrm{.}$ 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}\mathrm{/}\mathbb{E}{S}_{1,n}$ to $1$, a typical volume law, and the variance bound $\mathrm{V}\mathrm{a}\mathrm{r}(S_{1,n})=O_s({\log }^{2}n)$. An accompanying Lean 4 development verifies the proof chain.