Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Free input-independent preparation of prior entanglement

Open
QAlgorithms.Papers.Independent.Intakethird100.P81.prior_entanglement_preparation

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let ψ\psiψ be any unit vector on NNN qubits, and specify which qubits Alice and Bob should own. There is an input-independent unitary UUU and a legal one-message preparation phase such that

U∣0N⟩=∣ψ⟩.U\lvert0^N\rangle=\lvert\psi\rangle.U∣0N⟩=∣ψ⟩.

Alice initially owns all NNN blank qubits and applies UUU 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.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P81
Formal statement
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
Source
On rounds in quantum communication, arXiv:quant-ph/0004100v5, PDF p. 7, Paragraph preceding Definition 6
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number NNN, every ownership assignment o:{0,…,N−1}→{Alice,Bob}o:\{0,\ldots,N-1\}\to\{\text{Alice},\text{Bob}\}o:{0,…,N−1}→{Alice,Bob}, and every complex vector ψ\psiψ indexed by NNN-bit strings with Euclidean norm 111, there exists a unitary matrix UUU such that U∣0N⟩=ψU|0^N\rangle=\psiU∣0N⟩=ψ, where ∣0N⟩|0^N\rangle∣0N⟩ has coefficient 111 at the all-false bit string and 000 elsewhere. Moreover, the single round in which Alice applies UUU and transmits exactly the wires qqq with o(q)=Bobo(q)=\text{Bob}o(q)=Bob 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 kkk, an injection w:{0,…,k−1}↪{0,…,N−1}w:\{0,\ldots,k-1\}\hookrightarrow\{0,\ldots,N-1\}w:{0,…,k−1}↪{0,…,N−1}, and a complex matrix MMM indexed by kkk-bit strings, with the image of www contained in Alice’s initially owned wires, such that Uy,z=My∘w,z∘wU_{y,z}=M_{y\circ w,z\circ w}Uy,z​=My∘w,z∘w​ when yyy and zzz agree outside that image, and Uy,z=0U_{y,z}=0Uy,z​=0 otherwise. Updating ownership after the round gives exactly ooo: transmitted wires become Bob’s, and the remaining wires stay Alice’s. The statement includes N=0N=0N=0, when there are no wires to transmit and the state space has one basis vector.

Human review
  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me