Moving an input factor to the output

Proved

QAlgorithms.Papers.Independent.Intakenext100.P95.input_output_reshaping

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

prove2quantum

Let $A_1,A_2,B$ be finite orthonormal basis index sets, and let $T:\mathcal H_{A_2}\otimes\mathcal H_{A_1}\to\mathcal H_B$ be an isometry. Define $\widetilde T:\mathcal H_{A_1}\to\mathcal H_B\otimes\mathcal H_{A_2}$ by $\widetilde T_{(b,a_2),a_1}=T_{b,(a_2,a_1)}$ , with no conjugation. Then

\widetilde T^\dagger\widetilde T=|A_2|I_{A_1}.

This identity justifies reinterpreting input legs as output legs, with the displayed scalar normalization. It also holds when $A_2$ is empty, when both sides vanish.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P95

Formal statement

namespace QAlgorithms.Papers.Independent.Intakenext100.P95

open scoped Matrix ComplexConjugate

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

/-- PDF pp.6–7, (2.4)–(2.5): reshuffling without conjugation gives the scalar
card(A2), including the harmless empty-A2 case. -/
theorem input_output_reshaping {A1 A2 B : Type*}
    [Fintype A1] [Fintype A2] [Fintype B] [DecidableEq A1] [DecidableEq A2]
    (T : Matrix B (A2 × A1) ℂ) (hT : Tᴴ * T = 1) :
    (moveInput T)ᴴ * moveInput T = (Fintype.card A2 : ℂ) • 1 := by sorry

end

end QAlgorithms.Papers.Independent.Intakenext100.P95

Source

Holographic quantum error-correcting codes: Toy models for the bulk/boundary correspondence, arXiv:1503.06237v2, PDF p. 7, §2, moving an input factor to output (2.4)–(2.5)

Read-back

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

Let $A_1,A_2,B$ be finite types, with decidable equality on $A_1$ and $A_2$ , and let $T$ be a complex matrix with rows indexed by $B$ and columns indexed by $A_2\times A_1$ . Suppose $T^\dagger T=I_{A_2\times A_1}$ , where $\dagger$ denotes conjugate transpose. Define the reshaped matrix $R$ , with rows indexed by $B\times A_2$ and columns indexed by $A_1$ , by $R_{(b,a_2),a_1}=T_{b,(a_2,a_1)}$ . Then

R^\dagger R=|A_2|\,I_{A_1}.

Empty index types are allowed: if $A_2$ is empty, the hypothesis concerns an empty matrix and the conclusion is $R^\dagger R=0$ ; if $A_1$ is empty, the conclusion is an equality of empty matrices. When $|B|<|A_2||A_1|$ , the hypothesis cannot hold.

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