Unitary entanglement assistance under a vacuum energy restriction

Abstract

Four unitary encodings of a partially entangled state outperform every unassisted strategy at the same energy.

Alice receives an input x, applies a unitary to her part of a shared pure state, and sends that part to Bob. Bob chooses a setting y and measures the joint system, obtaining an outcome b. This is the unitary case of the entanglement-assisted prepare-and-measure model in Section II, Eqs. (1)–(2), and Section IV.A. All finite sums range over the entire indicated finite type; each tsum ranges over its indicated arbitrary index type. Matrix entries are complex, probabilities and task values are real, and brackets denote anonymous typeclass assumptions.

Definition 1.1 (Finite positive operator-valued measurements).

$$\forall n\in Type,\forall B\in Type,[\mathrm{Fintype}\left(n\right)],[\mathrm{DecidableEq}\left(n\right)],[\mathrm{Fintype}\left(B\right)],\forall M\in B\to \mathrm{Matrix}\left(n,n,Complex\right),(\mathrm{IsPOVM}\left(M\right))\iff ((\forall b\in B,\mathrm{Matrix}.\mathrm{PosSemidef}\left(M\left(b\right)\right))\wedge (\sum _{b:B}(M\left(b\right))=1))$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.IsPOVM (✓ std3).

Source. Repository-derived.

Acknowledgement. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Every effect is positive semidefinite and the effects sum to the identity. The carrier n and outcome type B are finite; n also has decidable equality.

Definition 1.2 (A pure state with local unitary encodings).

$$\forall X\in Type,\forall Y\in Type,\forall B\in Type,[\mathrm{Fintype}\left(B\right)],\forall dA\in Nat,\forall dB\in Nat,\forall Psi\in \mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)\to Complex,\forall U\in X\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(dA\right),Complex\right),\forall M\in Y\to \left(B\to \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),Complex\right)\right),(\mathrm{UnitaryStrategy}\left(Psi,U,M\right))\iff ((\sum _{i:\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)}(\mathrm{Complex}.\mathrm{normSq}\left(Psi\left(i\right)\right))=1)\wedge (\forall y\in Y,\mathrm{IsPOVM}\left(M\left(y\right)\right)))$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.UnitaryStrategy (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

The squared moduli of the state coordinates sum to one. The type of U requires a unitary matrix on Alice’s factor for every input. For every setting, Bob’s effects form a POVM on the product of the two factors. These are the pure-state unitary strategies considered in Section IV.A.

Definition 1.3 (The state after the message is encoded).

$$\forall X\in Type,\forall dA\in Nat,\forall dB\in Nat,\forall Psi\in \mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)\to Complex,\forall U\in X\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(dA\right),Complex\right),\forall x\in X,\mathrm{encoded}\left(Psi,U,x\right)=\mathrm{Matrix}.\mathrm{mulVec}\left(\mathrm{Matrix}.\mathrm{kronecker}\left((U\left(x\right):\mathrm{Matrix}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dA\right),Complex\right)),(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(dB\right),\mathrm{Fin}\left(dB\right),Complex\right))\right),Psi\right)$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.encoded (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Alice acts on her factor with U(x), while the identity acts on Bob’s factor. The Kronecker product followed by matrix-vector multiplication gives the joint state received by Bob, specializing Eq. (1) to a unitary operation.

Definition 1.4 (The outcome probability of the joint measurement).

$$\forall X\in Type,\forall Y\in Type,\forall B\in Type,\forall dA\in Nat,\forall dB\in Nat,\forall Psi\in \mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)\to Complex,\forall U\in X\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(dA\right),Complex\right),\forall M\in Y\to \left(B\to \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),Complex\right)\right),\forall b\in B,\forall x\in X,\forall y\in Y,\mathrm{unitaryProb}\left(Psi,U,M,b,x,y\right)=\mathrm{Complex}.\mathrm{re}\left(\mathrm{dotProduct}\left(\mathrm{star}\left(\mathrm{encoded}\left(Psi,U,x\right)\right),\mathrm{Matrix}.\mathrm{mulVec}\left(M\left(y,b\right),\mathrm{encoded}\left(Psi,U,x\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.unitaryProb (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

The real part of the quadratic form of M(y,b) on the encoded vector is the Born probability in Eq. (2). The conjugation in star is coordinatewise, and dotProduct sums products of matching coordinates. The expression is defined for arbitrary vectors and effects; UnitaryStrategy supplies their physical normalization.

Definition 1.5 (The vacuum component of the transmitted subsystem).

$$\forall X\in Type,\forall dA\in Nat,\forall dB\in Nat,[\mathrm{NeZero}\left(dA\right)],\forall Psi\in \mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)\to Complex,\forall U\in X\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(dA\right),Complex\right),\forall x\in X,\mathrm{unitaryVacuum}\left(Psi,U,x\right)=\sum _{j:\mathrm{Fin}\left(dB\right)}((\Vert \mathrm{encoded}\left(Psi,U,x\right)\left(\mathrm{Prod}.\mathrm{mk}\left(0,j\right)\right)\Vert {)}^2)$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.unitaryVacuum (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Sum the squared moduli of the encoded coordinates whose Alice index is zero. This is the vacuum population of the reduced message state. Equation (3) requires this quantity to be at least 1 − omega for every input, where omega is the allowed energy and NeZero dA makes the vacuum index available.

Definition 1.6 (Unassisted quantum communication with shared randomness).

$$\forall X\in Type,\forall Y\in Type,\forall B\in Type,\forall H\in Type,\forall L\in Type,\forall K\in Type,[\mathrm{Fintype}\left(B\right)],[\mathrm{NormedAddCommGroup}\left(H\right)],[\mathrm{InnerProductSpace}\left(Complex,H\right)],[\mathrm{CompleteSpace}\left(H\right)],\forall vac\in H,\forall q\in L\to Real,\forall p\in L\to \left(X\to \left(K\to Real\right)\right),\forall psi\in L\to \left(X\to \left(K\to H\right)\right),\forall N\in L\to \left(Y\to \left(B\to \mathrm{ContinuousLinearMap}\left(Complex,H,H\right)\right)\right),(\mathrm{QCStrategy}\left(vac,q,p,psi,N\right))\iff ((\Vert vac\Vert =1)\wedge ((\forall l\in L,0\le q\left(l\right))\wedge ((\mathrm{HasSum}\left(q,1\right))\wedge ((\forall l\in L,\forall x\in X,\forall k\in K,0\le p\left(l,x,k\right))\wedge ((\forall l\in L,\forall x\in X,\mathrm{HasSum}\left(p\left(l,x\right),1\right))\wedge ((\forall l\in L,\forall x\in X,\forall k\in K,\Vert psi\left(l,x,k\right)\Vert =1)\wedge (\forall l\in L,\forall y\in Y,(\forall b\in B,0\le N\left(l,y,b\right))\wedge (\sum _{b:B}(N\left(l,y,b\right))=1))))))))$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.QCStrategy (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

The message space H is an arbitrary complex Hilbert space with unit vacuum vector vac; there is no dimension restriction. Shared randomness ranges over an arbitrary type L, with nonnegative weights q and HasSum q 1. For each l and x, density operators enter through their ensemble decompositions: nonnegative weights p(l,x,k) with sum one and unit vectors psi(l,x,k), indexed by an arbitrary type K. Spectral decomposition represents every density operator in this way. For each l and y, N is a finite POVM of bounded complex linear operators; 0 ≤ N means positivity in the operator order. These are the states and measurements of the unassisted quantum model in Section II.B and Eq. (4). Bob retains no entangled system.

Definition 1.7 (Probabilities averaged over the shared random variable).

$$\forall X\in Type,\forall Y\in Type,\forall B\in Type,\forall H\in Type,\forall L\in Type,\forall K\in Type,[\mathrm{NormedAddCommGroup}\left(H\right)],[\mathrm{InnerProductSpace}\left(Complex,H\right)],\forall q\in L\to Real,\forall p\in L\to \left(X\to \left(K\to Real\right)\right),\forall psi\in L\to \left(X\to \left(K\to H\right)\right),\forall N\in L\to \left(Y\to \left(B\to \mathrm{ContinuousLinearMap}\left(Complex,H,H\right)\right)\right),\forall b\in B,\forall x\in X,\forall y\in Y,\mathrm{qcProb}\left(q,p,psi,N,b,x,y\right)=\mathrm{tsum}\left((l:L)\mapsto (q\left(l\right))\cdot (\mathrm{tsum}\left((k:K)\mapsto (p\left(l,x,k\right))\cdot (\mathrm{Complex}.\mathrm{re}\left(\mathrm{inner}\left(Complex,psi\left(l,x,k\right),N\left(l,y,b\right)\left(psi\left(l,x,k\right)\right)\right)\right))\right))\right)$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.qcProb (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Equation (4) averages the Born probabilities first over each message ensemble and then over shared randomness. For a density operator rho represented by an ensemble, Re Tr(N rho) is the weighted sum of Re inner(Complex,psi,N psi). The two tsum expressions range over the entire arbitrary index types L and K. The definition requires a complex inner-product space; positivity, normalization and completeness are supplied separately by QCStrategy.

Definition 1.8 (The averaged vacuum population).

$$\forall X\in Type,\forall H\in Type,\forall L\in Type,\forall K\in Type,[\mathrm{NormedAddCommGroup}\left(H\right)],[\mathrm{InnerProductSpace}\left(Complex,H\right)],\forall vac\in H,\forall q\in L\to Real,\forall p\in L\to \left(X\to \left(K\to Real\right)\right),\forall psi\in L\to \left(X\to \left(K\to H\right)\right),\forall x\in X,\mathrm{qcVacuum}\left(vac,q,p,psi,x\right)=\mathrm{tsum}\left((l:L)\mapsto (q\left(l\right))\cdot (\mathrm{tsum}\left((k:K)\mapsto (p\left(l,x,k\right))\cdot ({\Vert \mathrm{inner}\left(Complex,vac,psi\left(l,x,k\right)\right)\Vert }^2)\right))\right)$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.qcVacuum (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Equation (5) averages the squared vacuum overlaps over each message ensemble and over shared randomness, using tsum on both arbitrary index types. For unit vac, the ensemble average is the vacuum population of the corresponding density operator. The energy restriction is qcVacuum(vac,q,p,psi,x) at least 1 − omega for each x. It permits the conditional energies to differ. This expression is defined on any complex inner-product space without normalization assumptions.

Definition 1.9 (A general finite linear communication task).

$$\forall X\in Type,\forall Y\in Type,\forall B\in Type,[\mathrm{Fintype}\left(X\right)],[\mathrm{Fintype}\left(Y\right)],[\mathrm{Fintype}\left(B\right)],\forall c\in B\to \left(X\to \left(Y\to Real\right)\right),\forall p\in B\to \left(X\to \left(Y\to Real\right)\right),\mathrm{taskValue}\left(c,p\right)=\sum _{b:B}(\sum _{x:X}(\sum _{y:Y}((c\left(b,x,y\right))\cdot (p\left(b,x,y\right)))))$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.taskValue (✓ std3).

Source. Repository-derived.

Acknowledgement. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Each real coefficient c(b,x,y) multiplies the corresponding probability, and the sum includes all outcomes, inputs and settings. The coefficients are arbitrary; this includes success probabilities as well as other linear figures of merit.

Definition 1.10 (The positive answer to the question for general tasks).

$$(claim)\iff (\forall X\in Type,\forall Y\in Type,\forall B\in Type,[\mathrm{Fintype}\left(X\right)],[\mathrm{Fintype}\left(Y\right)],[\mathrm{Fintype}\left(B\right)],\forall c\in B\to \left(X\to \left(Y\to Real\right)\right),\forall omega\in Real,(0\le omega)\Rightarrow ((omega<\frac{1}{2})\Rightarrow (\forall dA\in Nat,\forall dB\in Nat,[\mathrm{NeZero}\left(dA\right)],\forall Psi\in \mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right)\to Complex,\forall U\in X\to \mathrm{Matrix}.\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(dA\right),Complex\right),\forall M\in Y\to \left(B\to \mathrm{Matrix}\left(\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),\mathrm{Prod}\left(\mathrm{Fin}\left(dA\right),\mathrm{Fin}\left(dB\right)\right),Complex\right)\right),(\mathrm{UnitaryStrategy}\left(Psi,U,M\right))\Rightarrow ((\forall x\in X,1-omega\le \mathrm{unitaryVacuum}\left(Psi,U,x\right))\Rightarrow (\exists H\in Type,\exists [\mathrm{NormedAddCommGroup}\left(H\right)],\exists [\mathrm{InnerProductSpace}\left(Complex,H\right)],\exists [\mathrm{CompleteSpace}\left(H\right)],\exists vac\in H,\exists L\in Type,\exists K\in Type,\exists q\in L\to Real,\exists p\in L\to \left(X\to \left(K\to Real\right)\right),\exists psi\in L\to \left(X\to \left(K\to H\right)\right),\exists N\in L\to \left(Y\to \left(B\to \mathrm{ContinuousLinearMap}\left(Complex,H,H\right)\right)\right),(\mathrm{QCStrategy}\left(vac,q,p,psi,N\right))\wedge ((\forall x\in X,1-omega\le \mathrm{qcVacuum}\left(vac,q,p,psi,x\right))\wedge (\mathrm{taskValue}\left(c,\mathrm{unitaryProb}\left(Psi,U,M\right)\right)\le \mathrm{taskValue}\left(c,\mathrm{qcProb}\left(q,p,psi,N\right)\right))))))))$$

Formalization. D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.claim (✓ std3).

Citation. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Section VI asks whether unitary encoding remains resourceless for general tasks. The displayed proposition is the positive answer for finite alphabets and 0 ≤ omega < 1/2: every unitary entanglement-assisted value would be matched or exceeded by an unassisted strategy with the same energy bound. The latter may use any complex Hilbert message space with a unit vacuum vector, arbitrary shared randomness, density operators represented by ensembles, and POVMs of positive bounded operators. Its message dimension has no restriction. Result 4 concerns only probabilistic transmission of a bit; the proposition here quantifies over all finite linear tasks.

Theorem 1.11 (Four messages give a strict advantage below half-unit energy).

$$\neg (claim)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.result (✓ std3). ∎

Resolves. Problems/roch-i-carceller-tavakoli-2025-energy-restricted-unitary-encoding (refuted) by D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.result.

Source. Repository-derived.

Acknowledgement. Carles Roch i Carceller; Armin Tavakoli (2025). The role of entanglement in energy-restricted communication and randomness generation. DOI: 10.1088/2058-9565/ae4d80. URL: https://arxiv.org/abs/2510.27473v1.

Commentary.

Take inputs and outcomes (u,v) in Fin 2 × Fin 2, one measurement setting, and task weights c(b,x,y) = 1/4 when b = x and zero otherwise. Alice and Bob share the pure state (4/5)|00⟩ + (3/5)|11⟩. Set Z = [[1,0],[0,−1]] and R = [[4/5,−3/5],[3/5,4/5]]. For input (u,v), Alice applies Z^u R Z^v. Bob measures the four rank-one projectors onto the orthonormal vectors m_(u,v) = (1/2)(1,−(−1)^v,(−1)^u,(−1)^(u+v)), in the coordinate order (00,01,10,11).

For input (u,v), the encoded vector has coordinates (16/25,−(9/25)(−1)^v,(12/25)(−1)^u,(12/25)(−1)^(u+v)). Its vacuum component is 337/625 for every input. Thus the energy restriction holds with omega = 288/625 < 1/2. The overlap with the corresponding measurement vector is 49/50, giving task value 2401/2500.

In every complex Hilbert space, unit vectors g and psi and an effect 0 ≤ E ≤ I satisfy Delta = Re inner(psi,E psi) − Re inner(g,E g) ≤ sqrt(1 − |inner(g,psi)|²). Multiply psi by a complex scalar of modulus one so that a = inner(g,psi) is real and nonnegative, and put u = psi + g and v = psi − g. Then Delta is both Re inner(u,E v) and −Re inner(u,(I − E)v). Cauchy–Schwarz for the positive forms of E and I − E gives Delta² ≤ A B and Delta² ≤ (U − A)(V − B), where A = inner(u,E u), B = inner(v,E v), U = norm(u)² = 2 + 2a and V = norm(v)² = 2 − 2a. The inequality sqrt(A B) + sqrt((U − A)(V − B)) ≤ sqrt(U V) yields the stated bound.

For nonnegative weights w summing to one and 0 ≤ t_j ≤ 1, put s = sum_j w_j t_j. Cauchy–Schwarz for sqrt(w_j) and sqrt(w_j t_j) gives sum_j w_j sqrt(t_j) = sum_j sqrt(w_j)·sqrt(w_j t_j) ≤ sqrt(sum_j w_j)·sqrt(sum_j w_j t_j) = sqrt(s). Apply this averaging bound to the ensemble decompositions of the density operators and then to shared randomness. The POVM identity gives sum_x inner(vac,N_x vac) = 1 for each value of the shared random variable. Consequently, in every Hilbert message space the four-guess task value is at most 1/4 + (1/4) sum_x sqrt(1 − qcVacuum(vac,q,p,psi,x)) ≤ 1/4 + sqrt(omega) under the same averaged energy restriction. Since sqrt(288/625) < 17/25, every such value is less than 93/100, whereas 2401/2500 > 93/100. Hence claim is false.

References

• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.IsPOVM
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.QCStrategy
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.UnitaryStrategy
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.claim
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.encoded
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.qcProb
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.qcVacuum
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.result
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.taskValue
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.unitaryProb
• Truth anchor: D5/S3/Quantum/Entanglement/EnergyRestrictedUnitaryEncodingRefutation.unitaryVacuum
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/Quantum/QuantumChannels/PositiveFilterTransposeRefutation