Free input-independent preparation of prior entanglement
OpenQAlgorithms.Papers.Independent.Intakethird100.P81.prior_entanglement_preparationLet be any unit vector on qubits, and specify which qubits Alice and Bob should own. There is an input-independent unitary and a legal one-message preparation phase such that
Alice initially owns all blank qubits and applies locally. The constructed preparation round transfers exactly the wires assigned to Bob, leaving precisely the prescribed final ownership and shared state. All preparation communication is uncharged and precedes the inputs and the counted protocol.
This realizes arbitrary finite input-independent prior entanglement without granting input-dependent assistance. The zero-qubit case is included, with an empty transfer and a unit complex phase.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81
noncomputable section
open scoped Matrix ComplexConjugate ENNReal
attribute [local instance] Classical.propDecidable
namespace QAlgorithms.Papers.Independent.Intakethird100.P81
open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntropyBits)
open QAlgorithms.Papers.Independent.Bridge50.P44 (ClassicalFirst)
/-- Unnumbered equivalence preceding Definition 6, PDF p.7: every finite normalized prior
entangled state is prepared with input-independent local work and uncharged communication.
The constructed round transfers actual owned qubits and realizes exactly the requested ownership. -/
theorem prior_entanglement_preparation (N : ℕ) (own : Fin N → Party)
(psi : EuclideanSpace ℂ (Qubits N)) (hpsi : ‖psi‖ = 1) :
∃ U : Matrix.unitaryGroup (Qubits N) ℂ,
act (U : Matrix (Qubits N) (Qubits N) ℂ) (ket (fun _ => false)) = psi ∧
roundsLegal (fun _ => .alice) [preparationRound own U] ∧
(preparationRound own U).update (fun _ => .alice) = own := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P81
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For every natural number , every ownership assignment , and every complex vector indexed by -bit strings with Euclidean norm , there exists a unitary matrix such that , where has coefficient at the all-false bit string and elsewhere. Moreover, the single round in which Alice applies and transmits exactly the wires with is legal when all wires initially belong to Alice: every transmitted wire initially belongs to her, and the applied matrix acts within her initially owned wires. Explicitly, the latter condition means that there exist a natural number , an injection , and a complex matrix indexed by -bit strings, with the image of contained in Alice’s initially owned wires, such that when and agree outside that image, and otherwise. Updating ownership after the round gives exactly : transmitted wires become Bob’s, and the remaining wires stay Alice’s. The statement includes , when there are no wires to transmit and the state space has one basis vector.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.