Weak Typicality of von Neumann Entanglement Entropy in Gaussian Boson Sampling
Hongru Zhao
quant-ph
Aug 18, 2026 · v1
TL;DR
A Lean 4 development verifies the proof chain establishing proportional von Neumann weak typicality of 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 $α\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.
Problem
For a Haar-distributed passive interferometer acting on n equally squeezed input modes, proportional weak typicality of the von Neumann entanglement entropy for subsystems of size k_n/n → r ∈ (0,1) was left open by prior work, which handled only integer Rényi orders and sublinear subsystems. The obstruction is a logarithmic divergence in the one-mode entropy profile as a reduced symplectic eigenvalue approaches its pure value.
Approach
The entropy is represented as a singular value statistic of a principal block of UU^T, which has the COE distribution. The logarithmic endpoint singularity is regularized via a truncated profile, and Lipschitz estimates combined with Mirsky's singular value variation theorem yield sensitivity bounds. Concentration of Haar measure on the unitary group is then applied, together with a self-contained extensive lower bound on the mean. An accompanying Lean 4 development verifies the proof chain.
Results
A subgaussian tail bound P(|S_{1,n}/E S_{1,n} − 1| ≥ ε) ≤ 2 exp[−c_{s,r} ε² n² / log²(en)] is proven, establishing proportional von Neumann weak typicality, almost sure convergence to 1, a typical volume law, and the variance bound Var(S_{1,n}) = O_s(log² n).
