Finite-Fock beam-splitter non-extremality

Abstract

Finite-Fock beam-splitter states need not be extreme Wigner-positive states.

Fock cutoff K is represented by Matrix (Fin (K+1)) (Fin (K+1)) Complex. Real coefficients are explicitly mapped by Complex.ofReal; natural coefficients use Nat.cast into Real. The complex order is Mathlib ComplexOrder: a complex value is non-negative precisely when its imaginary part is zero and its real part is non-negative. Nat.sub denotes truncated natural subtraction. Finite indices are sent to their natural values by val. Scalar multiplication uses the Lean scalar action. Proof arguments to beamSplitter are omitted; its transmissivity is one half.

Definition 1.1 (genLaguerre).

$$\forall k:\mathbb{N},(\forall m:\mathbb{N},(\forall x:\mathbb{R},(\mathrm{genLaguerre}\left(k,m,x\right)=\sum _{i:\mathbb{N},i\in \mathrm{Finset}.\mathrm{range}\left(m+1\right)}(\frac{(((-(1){)}^i)\cdot (\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{choose}\left(m+k,\mathrm{Nat}.\mathrm{sub}\left(m,i\right)\right)\right)))\cdot ((x{)}^i)}{\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{factorial}\left(i\right)\right)}))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.genLaguerre (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

The generalized Laguerre polynomial uses the explicit finite sum with real argument x and natural indices k and m.

Definition 1.2 (wignerFock).

$$\forall m:\mathbb{N},(\forall n:\mathbb{N},(\forall alpha:\mathbb{C},(\mathrm{wignerFock}\left(m,n,alpha\right)=\mathrm{ite}\left(m\le n,(((\mathrm{Complex}.\mathrm{ofReal}\left(((\frac{2}{\mathrm{Real}.\mathrm{pi}})\cdot ((-(1){)}^m))\cdot (\mathrm{Real}.\mathrm{sqrt}\left(\frac{\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{factorial}\left(m\right)\right)}{\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{factorial}\left(n\right)\right)}\right))\right))\cdot (((2)\cdot (alpha){)}^{\mathrm{Nat}.\mathrm{sub}\left(n,m\right)}))\cdot (\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{genLaguerre}\left(\mathrm{Nat}.\mathrm{sub}\left(n,m\right),m,(4)\cdot ((\Vert alpha\Vert {)}^2)\right)\right)))\cdot (\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{Real}.\exp \left((-(2))\cdot ((\Vert alpha\Vert {)}^2)\right)\right)),\mathrm{starRingEnd}\left(\mathbb{C},(((\mathrm{Complex}.\mathrm{ofReal}\left(((\frac{2}{\mathrm{Real}.\mathrm{pi}})\cdot ((-(1){)}^n))\cdot (\mathrm{Real}.\mathrm{sqrt}\left(\frac{\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{factorial}\left(n\right)\right)}{\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{factorial}\left(m\right)\right)}\right))\right))\cdot (((2)\cdot (alpha){)}^{\mathrm{Nat}.\mathrm{sub}\left(m,n\right)}))\cdot (\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{genLaguerre}\left(\mathrm{Nat}.\mathrm{sub}\left(m,n\right),n,(4)\cdot ((\Vert alpha\Vert {)}^2)\right)\right)))\cdot (\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{Real}.\exp \left((-(2))\cdot ((\Vert alpha\Vert {)}^2)\right)\right))\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.wignerFock (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Appendix A.1, page 18, equation (48), gives the Fock transition Wigner function. Its continuation is stated verbatim: “for m≤n, otherwise use the relation W|n⟩⟨m|=W*|m⟩⟨n|.” The displayed formula includes the real prefactor, complex power, Laguerre polynomial and Gaussian envelope; the reverse branch is complex conjugation.

Definition 1.3 (wigner).

$$\forall K:\mathbb{N},(\forall A:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),(\forall alpha:\mathbb{C},(\mathrm{wigner}\left(A,alpha\right)=\sum _{m:\mathrm{Fin}\left(K+1\right)}(\sum _{n:\mathrm{Fin}\left(K+1\right)}((A\left(m,n\right))\cdot (\mathrm{wignerFock}\left(\mathrm{val}\left(m\right),\mathrm{val}\left(n\right),alpha\right)))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.wigner (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Page 6, Section 3.1, equation (16): “Consider a quasi-state Â∈𝒜ⁿ, with Fock matrix elements Aₖℓ=⟨k|Â|ℓ⟩. The Wigner function of  is here expressed as:” The displayed expansion retains every matrix entry, including off-diagonal entries, and includes both endpoints of the Fock cutoff.

Definition 1.4 (WPS).

$$\forall K:\mathbb{N},(\mathrm{WPS}\left(K\right)=\{A:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right)\mid \mathrm{Matrix}.\mathrm{PosSemidef}\left(A\right)\wedge \left(\mathrm{Matrix}.\mathrm{trace}\left(A\right)=1\wedge \forall alpha:\mathbb{C},(0\le \mathrm{wigner}\left(A,alpha\right))\right)\})$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.WPS (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Page 1, the introduction describes WPS as “quantum states with non-negative Wigner function”. Page 3, Section 2 specifies: “We denote by 𝒟⊂ℬ₁ the set of Hermitian positive semi-definite (PSD) operators of unit trace and refer to operators in 𝒟 as states.” Matrix.PosSemidef includes Hermitian symmetry. The finite-matrix set implements these conditions without an additional restriction on phase-space points.

Definition 1.5 (IsExtremeWPS).

$$\forall K:\mathbb{N},(\forall sigma:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),(\mathrm{IsExtremeWPS}\left(K,sigma\right)=\left(sigma\in \mathrm{WPS}\left(K\right)\wedge \forall x:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),(x\in \mathrm{WPS}\left(K\right)\Rightarrow \forall y:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),(y\in \mathrm{WPS}\left(K\right)\Rightarrow \left(sigma=(\frac{1}{2})\cdot (x+y)\Rightarrow \left(x=sigma\wedge y=sigma\right)\right)))\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.IsExtremeWPS (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Page 4, Definition 2: “Given a convex set 𝒞, the point a∈𝒞 is an extreme point of 𝒞 if and only if ∀x,y∈𝒞:a=½(x+y)⇔x=y=a.” Membership and the forward midpoint implication are explicit. The reverse implication is automatic when both endpoints equal sigma.

Definition 1.6 (bsState).

$$\forall N:\mathbb{N},(\forall psi:\mathrm{Fin}\left(N+1\right)\to \mathbb{C},(\forall phi:\mathrm{Fin}\left(N+1\right)\to \mathbb{C},(\mathrm{let}Psi=\mathrm{beamSplitter}\left(\frac{1}{2},\sum _{j:\mathrm{Fin}\left(N+1\right)}(\sum _{k:\mathrm{Fin}\left(N+1\right)}(((psi\left(j\right))\cdot (phi\left(k\right)))\cdot (\mathrm{fockPair}\left(\mathrm{val}\left(j\right),\mathrm{val}\left(k\right)\right))))\right);\forall m:\mathrm{Fin}\left((2)\cdot (N)+1\right),(\forall mp:\mathrm{Fin}\left((2)\cdot (N)+1\right),(\mathrm{bsState}\left(psi,phi\right)\left(m,mp\right)=\mathrm{tsum}\left((ell:\mathbb{N})\mapsto (Psi\left(ell\right)\left(\mathrm{val}\left(m\right)\right))\cdot (\mathrm{starRingEnd}\left(\mathbb{C},Psi\left(ell\right)\left(\mathrm{val}\left(mp\right)\right)\right))\right))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.bsState (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Page 4, Definition 1: “A beam-splitter state σ̂ is the single-mode output of a balanced beam-splitter acting on a separable state ρ̂ₛₑₚ, i.e. σ̂=Tr₂[Û₁/₂ ρ̂ₛₑₚ Û†₁/₂].” Here the separable input is a product of finite pure vectors. The second-mode sum is a tsum over all natural occupations. The repository rotation differs from the paper’s by second-mode parity before and after the rotation. Output parity disappears under the partial trace; input parity permutes the finite-Fock pure states and fixes the even-supported inputs used below. Thus the universal question and the counterexample agree with the paper’s convention.

Definition 1.7 (claim).

$$claim=\forall N:\mathbb{N},(\forall psi:\mathrm{Fin}\left(N+1\right)\to \mathbb{C},(\forall phi:\mathrm{Fin}\left(N+1\right)\to \mathbb{C},(\sum _{i:\mathrm{Fin}\left(N+1\right)}((\Vert psi\left(i\right)\Vert {)}^2)=1\Rightarrow \left(\sum _{i:\mathrm{Fin}\left(N+1\right)}((\Vert phi\left(i\right)\Vert {)}^2)=1\Rightarrow \mathrm{IsExtremeWPS}\left((2)\cdot (N),\mathrm{bsState}\left(psi,phi\right)\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.claim (✓ std3).

Citation. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

Page 15, Section 6: “This leads us to formulate the following open problem: for any two Fock-bounded pure states |ψ⟩,|φ⟩ is the beamsplitter state σ̂(ψ,φ) an extreme WPS?” N is any natural cutoff; psi and phi are arbitrary complex vectors on Fin (N+1), each with squared norm sum one. The output cutoff is 2*N. A midpoint decomposition in this finite WPS set also disproves extremality in the full WPS set.

Theorem 1.8 (Two-mode Fock coefficients).

$$\forall m:\mathbb{N},(\forall n:\mathbb{N},(\forall p:\mathbb{N},(\forall q:\mathbb{N},(D5.S3.\mathrm{Quantum}.\mathrm{QuantumChannels}.\mathrm{FockAttenuator}.\mathrm{BeamSplitter}.\mathrm{fockPair}\left(m,n,q,p\right)=\mathrm{ite}\left(p=m\wedge q=n,(1:\mathbb{C}),0\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.fockPair_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coefficient of the two-mode Fock vector is one exactly when the retained occupation is m and the environment occupation is n. Every other coefficient vanishes.

Theorem 1.9 (Refutation).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result (✓ std3). ∎

Resolves. Problems/van-herstraeten-et-al-2025-beam-splitter-state-extremality (refuted) by D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result.

Source. Repository-derived.

Acknowledgement. Zacharie Van Herstraeten; Jack Davis; Nuno C. Dias; João N. Prata; Nicolas J. Cerf; Ulysse Chabaud (2025). Extreme non-negative Wigner functions. URL: https://arxiv.org/abs/2512.14831v3.

Commentary.

For every positive real a, the inputs (|0>+a|2>)/sqrt(1+a^2) and (|0>-a|2>)/sqrt(1+a^2) give a non-extreme state supported on levels zero through four. After the positive Gaussian factor is removed, the output Wigner polynomial splits as the square of a real radial polynomial plus 32a^2Re(alpha)^2*Im(alpha)^2. A perturbation carries just the second square. Subtracting its trace multiple of the output produces a nonzero traceless direction; sufficiently small displacements in both signs remain positive semidefinite and Wigner-positive. Their midpoint is the output state, and the level-four diagonal entry separates the positive endpoint from it. The family at a=1/2 refutes the universal claim. The paper’s extremality theorem for two Fock-state inputs and its Vertigo-map results remain compatible with this conclusion.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.IsExtremeWPS
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.WPS
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.bsState
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.claim
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.fockPair_apply
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.genLaguerre
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.wigner
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.wignerFock
• Dependency: D5/S3/Observer/DefectModularFirstLaw/ThermofieldMarginalModularSpectrum
• Dependency: D5/S3/Quantum/QuantumChannels/FockAttenuator/BeamSplitter