Lemma 2: rotated maximally entangled contraction

Proved

QAlgorithms.Papers.Independent.Intakenext100.P52.rotated_entangled_contraction

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $I$ be a nonempty finite basis of cardinality $d$ , let $U$ be a unitary on this register, and let $|\alpha\rangle$ have unit norm. Define $|\phi\rangle=d^{-1/2}\sum_i|i,i\rangle$ and $|\phi(U)\rangle=(U^\dagger\otimes I)|\phi\rangle$ . Then

(\langle\phi(U)|_{12}\otimes I_3)(|\alpha\rangle_1\otimes|\phi\rangle_{23})=d^{-1}U|\alpha\rangle_3.

The resource on registers $2,3$ is unrotated. This identity is the general gate-teleportation contraction, with its branch scale unchanged.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P52

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate

namespace QAlgorithms.Papers.Independent.Intakenext100.P52

open QAlgorithms.Papers.Independent.Information100.P21 (Vec)

open QAlgorithms.Papers.Independent.Gap20.P01 (applyRect)

/-- Lemma 2, PDF p.3: unrotated resource on 23 and U† on measured ket 12;
the surviving gate is U, with no transpose. -/
theorem rotated_entangled_contraction {I : Type*} [Fintype I] [Nonempty I] [DecidableEq I]
    (U : Matrix I I ℂ) (hU : U ∈ Matrix.unitaryGroup I ℂ)
    (alpha : Vec I) (halpha : IsState alpha) :
    teleportContraction alpha (finiteMaxEntangled I) (rotatedEntangledKet U) =
      ((Fintype.card I : ℂ)⁻¹) • act U alpha := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P52

end

Source

An introduction to measurement based quantum computation, arXiv:quant-ph/0508124v2, PDF p. 3, Lemma 2: rotated maximally entangled contraction

Read-back

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

For every finite nonempty index type $I$ with decidable equality, every unitary complex $I\times I$ matrix $U$ , and every vector $\alpha\in\mathbb C^I$ with Euclidean norm $1$ , let $D=|I|$ , define $\Omega_I(i,j)=D^{-1/2}$ when $i=j$ and $0$ otherwise, and put $r_U=(U^\dagger\otimes I_D)\Omega_I$ . Contracting against $r_U$ gives $D^{-1}U\alpha$ ; explicitly, for every $\ell\in I$ ,

\sum_{i,j\in I}\overline{r_U(i,j)}\,\alpha_i\,\Omega_I(j,\ell) =\frac1D\sum_{i\in I}U_{\ell i}\alpha_i.

The statement includes $D=1$ .

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph