Lemma 1: maximally entangled contraction

Proved

QAlgorithms.Papers.Independent.Intakenext100.P52.maximally_entangled_contraction

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

prove2quantum

Let $I$ be a nonempty finite computational basis of cardinality $d$ , and let $|\alpha\rangle$ be a unit vector on this register. Put $|\phi\rangle=d^{-1/2}\sum_{i\in I}|i,i\rangle$ . With registers ordered $1,2,3$ , destructive contraction of the first two registers gives

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

The factor $1/d$ is retained: this is the subnormalized branch vector, rather than its normalized conditional state.

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 1, PDF p.3: the displayed output is a destructive bra contraction,
not a normalized conditional state or a projector retaining registers 1 and 2. -/
theorem maximally_entangled_contraction {I : Type*} [Fintype I] [Nonempty I] [DecidableEq I]
    (alpha : Vec I) (halpha : IsState alpha) :
    teleportContraction alpha (finiteMaxEntangled I) (finiteMaxEntangled I) =
      ((Fintype.card I : ℂ)⁻¹) • 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 1: 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 and every vector $\alpha\in\mathbb C^I$ with Euclidean norm $1$ , let $D=|I|$ and let $\Omega_I(i,j)=D^{-1/2}$ if $i=j$ and $0$ otherwise. The vector obtained by contracting $\alpha$ and one copy of $\Omega_I$ against another copy of $\Omega_I$ equals $D^{-1}\alpha$ ; explicitly, for every $\ell\in I$ ,

\sum_{i,j\in I}\overline{\Omega_I(i,j)}\,\alpha_i\,\Omega_I(j,\ell) =\frac{\alpha_\ell}{D}.

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