slug: van-herstraeten-et-al-2025-beam-splitter-state-extremality
bibkey: vanherstraeten2025extremewigner
doi: null
url: https://arxiv.org/abs/2512.14831v3
triage: theorem
motivation_gids:
  - D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result

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

Problem

Z. Van Herstraeten, J. Davis, N. C. Dias, J. N. Prata, N. J. Cerf and U. Chabaud, Extreme non-negative Wigner functions, arXiv:2512.14831v3, Section 6, printed page 15, ask:

This leads us to formulate the following open problem: for any two Fock-bounded pure states $|\psi ⟩,|\varphi ⟩$ is the beamsplitter state $\hat{\sigma }(\psi ,\varphi )$ an extreme WPS?

The source is the version-3 paper. The Tier-1 statement, finite-matrix conventions and literature reading are in preregistration #14447. The answer is Refuted.

Motivation

D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result proves the literal negation of claim, which quantifies every natural cutoff $N$ and all normalized $\psi ,\varphi :\mathrm{Fin}(N+1)\to \mathbb{C}$. The consumed private theorem family_not_extreme proves the counterexample for every real $a>0$, using ${\psi }_a=(|0⟩+a|2⟩)/\sqrt{1+a^2}$ and ${\varphi }_a=(|0⟩-a|2⟩)/\sqrt{1+a^2}$. result uses $a=1/2$ and $N=2$.

Gap

The published question extends the paper’s theorem for two Fock-state inputs to arbitrary Fock-bounded pure superpositions. The literature reading in #14447 finds no prior settlement in its stated scope; it is not an exhaustive absence claim. Finite-Fock support does not by itself exclude a nonzero traceless direction whose two small displacements remain positive semidefinite and Wigner-positive.

Route

The module uses the source’s Laguerre expansion, complex Wigner function, positive semidefinite trace-one matrices and midpoint definition of extremality. Its bsState applies the frozen BeamSplitter.beamSplitter at transmissivity $1/2$ to the tensor input, then the frozen ThermofieldMarginalModularSpectrum.countablePartialTraceRight to the PureStateHandshake.rankOneDensity of the joint amplitude and restricts both visible indices to $\mathrm{Fin}(2N+1)$. BeamSplitter.beamUnitary_fock supplies the Fock-basis action used in balanced_fock. The repository rotation and the source rotation differ by second-mode parity. The even-supported inputs are fixed by input parity, and output parity disappears under the partial trace.

Write $T=(1+a^2{)}^2$, $h=2a^2$ and $b=\sqrt{6}{a}^2/4$. Then

$$S_a=\left(\begin{array}{ccccc}1+3a^4/8& 0& 0& 0& -b\\ 0& 2a^2& 0& 0& 0\\ 0& 0& a^4/4& 0& 0\\ 0& 0& 0& 0& 0\\ -b& 0& 0& 0& 3a^4/8\end{array}\right),H_a=\left(\begin{array}{ccccc}{a}^2/2& 0& 0& 0& -b\\ 0& a^2& 0& 0& 0\\ 0& 0& a^2/2& 0& 0\\ 0& 0& 0& 0& 0\\ -b& 0& 0& 0& 0\end{array}\right).$$

The output is ${\sigma }_a=S_a/T$. Set $K_a=H_a-(h/T)S_a$ and ${ϵ}_a=\min (1/2,a^2/4,3a^4/[16(3+a^2/2)])$. The endpoints $E_a(t)=(S_a+t{K}_a)/T$ for $t=\pm {ϵ}_a/2$ belong to WPS, have midpoint ${\sigma }_a$, and the positive endpoint differs from ${\sigma }_a$ at entry $(4,4)$.

Falsifier

An encoding mismatch in the source’s Wigner kernel, finite pure input, mode traced out, normalization or midpoint condition would invalidate application to the source question. A publication already settling the same question in the literature scope would invalidate the novelty premise. The compilation uses no additional axiom beyond the accepted standard set. The general parameter-family proof has no numerical sampling hypothesis.

Evidence

The private declarations below are in the settling module and on result’s elaborated dependency path. All six family obligations are proved in Lean:

The public settling declaration is D5/S3/Quantum/QuantumChannels/FockAttenuator/FiniteFockBeamSplitterNonExtremality.result. The axiom closure of every public declaration is contained in $\{\mathrm{propext},Classical.choice,Quot.sound\}$.

Triage

What the settlement shows

• Mechanism — proved in this module. For every $a>0$ the Gaussian-stripped Wigner polynomial of $S_a$ is $R_a^2+I_a^2$, where $R_a=1-a^2+4a^2|\alpha {|}^2-2a^2|\alpha {|}^4$ and $I_a^2=32a^2\mathrm{Re}(\alpha {)}^2\mathrm{Im}(\alpha {)}^2$. familyS_wigner and familyH_wigner prove that $H_a$ carries only $I_a^2$ with the same Fock support. perturb_psd proves the required PSD allowance, and end_mem_WPS, end_midpoint, end_ne_state and family_not_extreme prove the nontrivial midpoint decomposition. A split with these support, PSD, trace and distinctness properties obstructs extremality by the source’s midpoint definition; a sum-of-squares identity alone does not establish those extra properties.
• Source’s proved case — proved by the paper’s argument. Section 5, Theorem “Beam-splitter states are extreme WPS”, source label theorem:beam-splitter-states-are-extreme, and its appendix “Beam-splitter states” proof establish extremality for inputs $|m⟩,|n⟩$. The conclusion is compatible with the refutation: both counterexample inputs have two nonzero Fock components when $a>0$. This source theorem is not separately formalized in the settling module.
• What survives — open. Extremality with one Fock input and one superposition remains a follow-up question. Extremality when the Wigner polynomial admits no split with the required support and PSD allowance also remains a follow-up question. Neither is asserted by result.
• Unaffected results — proved by the paper’s arguments. The Vertigo-map statements of Section 4 and the Krein–Milman statement in Section 2 (Theorem “Krein–Milman theorem for WPS”, source label th:Krein-Milman, attributed there to the companion paper’s Theorem 40) do not assume the universal question’s positive answer. Their stated hypotheses and conclusions are unaffected by this refutation; the settling module does not separately prove them.

Exact computation at the base instance

Computed, with tested scope exactly $a=1/2$, output Fock levels $0,1,2,3,4$ and both signs. Command: python3 /tmp/op-wps/check.py, exit code 0. SHA-256: c13d73a943bb98492b53a84326a313d80197eae5d755587370c62289e771a16a. The complete script below is the orchestrator’s exact check, reproduced without modification. Save it as check.py and run python3 check.py with SymPy installed.

It yields trace-one $\sigma$ and

$$200\sigma =\left(\begin{array}{ccccc}131& 0& 0& 0& -8\sqrt{6}\\ 0& 64& 0& 0& 0\\ 0& 0& 2& 0& 0\\ 0& 0& 0& 0& 0\\ -8\sqrt{6}& 0& 0& 0& 3\end{array}\right).$$

Both symbolic Wigner identities have ratio one. At $ϵ=3/800$, $S\pm ϵH$ have Wigner polynomials $R^2+(1\pm ϵ)I^2$ and traces $2503/1600$ and $2497/1600$, respectively. Each matrix has the zero eigenvalue from Fock level three; the smallest positive numerical eigenvalues are $0.000366953590422222$ and $0.000682572034392364$. These eigenvalue readings are computations, not uniform PSD proofs; the latter are supplied by perturb_psd for every $a>0$.

import sympy as sp
from sympy import sqrt, Rational as Q, factorial, exp, assoc_laguerre
x,y=sp.symbols('x y',real=True)
al=x+sp.I*y; alc=x-sp.I*y
N=5  # Fock 0..4 output support
# two-mode BS: a^dag -> (a^dag + b^dag)/sqrt2, b^dag -> (a^dag - b^dag)/sqrt2
A,B=sp.symbols('A B')
def state_poly(coeffs,var):  # sum c_k var^k/sqrt(k!)
    return sum(c*var**k/sqrt(factorial(k)) for k,c in coeffs.items())
def bs_output(psi,phi):
    # psi(a^dag) phi(b^dag)|0>, substitute
    P=sp.expand(state_poly(psi,(A+B)/sqrt(2))*state_poly(phi,(A-B)/sqrt(2)))
    poly=sp.Poly(P,A,B)
    amp={}  # amplitude for |m>_a |n>_b : coeff * sqrt(m! n!)
    for (m,n),c in poly.terms(): amp[(m,n)]=sp.nsimplify(c*sqrt(factorial(m)*factorial(n)))
    rho=sp.zeros(N,N)
    for (m,n),c in amp.items():
        for (m2,n2),c2 in amp.items():
            if n==n2 and m<N and m2<N: rho[m,m2]+=c*sp.conjugate(c2)
    return sp.simplify(rho)
def Wkl(k,l):
    # source eq. wigner_funcion_fock_mn without the positive factor 2/pi e^{-2|a|^2}
    r2=4*(x**2+y**2)
    if l>=k: return (-1)**k*sqrt(factorial(k)/factorial(l))*(2*al)**(l-k)*assoc_laguerre(k,l-k,r2)
    return sp.conjugate(Wkl(l,k))
def Wpoly(M):
    return sp.expand(sp.simplify(sum(M[k,l]*Wkl(k,l) for k in range(N) for l in range(N))))
a=Q(1,2)
psi={0:1/sqrt(1+a**2),2:a/sqrt(1+a**2)}; phi={0:1/sqrt(1+a**2),2:-a/sqrt(1+a**2)}
sig=bs_output(psi,phi)
print('sigma*200 =',sp.simplify(sig*200)); print('trace',sp.simplify(sig.trace()))
b=sqrt(6)*a**2/4
S=sp.diag(1+b**2,2*a**2,a**4/4,0,b**2); S[0,4]=S[4,0]=-b
print('S/(1+a^2)^2 == sigma:', sp.simplify(S/(1+a**2)**2-sig)==sp.zeros(N,N))
H=sp.diag(a**2/2,a**2,a**2/2,0,0); H[0,4]=H[4,0]=-b
WS=Wpoly(S); WH=Wpoly(H)
Ra=1-a**2+4*a**2*(x**2+y**2)-2*a**2*(x**2+y**2)**2; Ia2=32*a**2*x**2*y**2
# compare up to a constant factor
cS=sp.simplify(WS/(Ra**2+Ia2)); cH=sp.simplify(WH/Ia2)
print('W(S)/(R^2+I^2) =',cS,' W(H)/I^2 =',cH)
e=min(Q(1,2),a**2/4,3*a**4/(16*(3+a**2/2)))
for s in (1,-1):
    M=S+s*e*H
    ev=[sp.N(v) for v in M.eigenvals(multiple=True)]
    print('sign',s,'eigs',ev,'trace',sp.nsimplify(M.trace()))
    print('  W poly matches R^2+(1+-e)I^2 * c:', sp.simplify(Wpoly(M)-cS*(Ra**2+(1+s*e*cH/cS)*Ia2))==0, ' coef', sp.simplify(1+s*e*cH/cS))

ASSUMED-UNVERIFIED

Literature absence is restricted to the sources and searches recorded in #14447. The parity equivalence and finite-support embedding into the source’s full WPS set are source-level mathematical interpretations, not separately formalized infinite-dimensional bridges in this module. The Lean claim uses exactly the preregistered finite-matrix convention. Information-escape registration is paused under CLAUDE.md section 3.9.