§III remarks: matching Gram matrices in distinct input and output spaces

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.different_hilbert_spaces

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

prove2quantum

Let two normalized sample families, $K\ge2$ , lie in possibly different finite-dimensional complex Hilbert spaces and have the same complex Gram matrix. Assume the input samples generate the full algebra on their span. Then there is a partial isometry $M$ matching every input sample to its corresponding output sample, with

M^\dagger M=\Pi_{\rm in},\qquad MM^\dagger=\Pi_{\rm out}.

It restricts to a unitary between the two sample spans. The emulator constructed from these two families converges uniformly on supported input density operators to $\rho\mapsto M\rho M^\dagger$ in trace distance. Gram equality concerns consistent vector representatives; physical density records alone need not reveal those phases. No equality of ambient dimensions is required.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF p.4: equal complex Gram matrices specify a unitary between the sample spans,
represented by a partial isometry between potentially different ambient dimensions. -/
theorem different_hilbert_spaces (phi : K → EuclideanSpace ℂ I) (chi : K → EuclideanSpace ℂ J) (a : K)
    (hK : 2 ≤ Fintype.card K) (hphi : ∀ k, IsState (phi k))
    (hchi : ∀ k, IsState (chi k)) (hgen : Generates (pureSamples phi))
    (hgram : ∀ j k, inner ℂ (phi j) (phi k) = inner ℂ (chi j) (chi k)) :
    ∃ M : Matrix J I ℂ, Mᴴ * M = samplePi (pureSamples phi) ∧
      M * Mᴴ = samplePi (pureSamples chi) ∧
      (∀ k, Matrix.toEuclideanLin M (phi k) = chi k) ∧
      ∀ eps : ℝ, 0 < eps → ∃ N : ℕ, ∀ T ≥ N, ∀ rho : Matrix I I ℂ,
        IsDensityMatrix rho → InSampleSupport (pureSamples phi) rho →
        traceDistance (traceRight (jointEmulator (nonanchorProbability a)
          (erasureGate phi a) (erasureGate chi a) (phi a) (chi a) T rho))
          (M * rho * Mᴴ) ≤ eps := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 4, §III remarks: matching Gram matrices in distinct input and output spaces

Read-back

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

Let $I,J,K$ be finite index types with decidable equality, let $|K|\ge2$ , fix $a\in K$ , and let $\phi_k\in\mathbb C^I$ and $\chi_k\in\mathbb C^J$ all have norm $1$ . For $v=\phi$ or $v=\chi$ , put $P_k^v=v_kv_k^\dagger$ , and let $\Pi_v$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $\sum_kP_k^v$ . Assume that the complex span of all nonempty products of the $P_k^\phi$ is $\{X:\Pi_\phi X\Pi_\phi=X\}$ , and assume $\langle\phi_j,\phi_k\rangle=\langle\chi_j,\chi_k\rangle$ for every $j,k\in K$ . Then there exists a complex matrix $M:\mathbb C^I\to\mathbb C^J$ such that

M^\dagger M=\Pi_\phi,\qquad MM^\dagger=\Pi_\chi,\qquad M\phi_k=\chi_k\quad(k\in K),

and the following approximation property holds for this same $M$ . Define $p_a=0$ , $p_k=(|K|-1)^{-1}$ for $k\ne a$ ; for a system space $\mathbb C^D$ , define $C_D(V)=1_D\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , and put

E_k^v=C_D(1-2P_k^v)(1_D\otimes H)C_D(1-2P_a^v), \qquad H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix},

using $D=I$ for $\phi$ and $D=J$ for $\chi$ . For $h\in K^T$ , let $V_h^v$ apply $E_{h_j}^v$ successively on the system and ancilla $j$ , let $\eta_T=((|0\rangle-|1\rangle)/\sqrt2)^{\otimes T}$ , and put $X_h=V_h^\phi(\rho\otimes\eta_T\eta_T^\dagger)(V_h^\phi)^\dagger$ . With $P_{\mathrm{false}}=P_a^\phi$ and $P_{\mathrm{true}}=1-P_a^\phi$ , the output matrix in the claim is

Y_T(\rho)=\operatorname{Tr}_{\mathrm{anc}} \sum_{h\in K^T}\left(\prod_{j<T}p_{h_j}\right) \sum_b(V_h^\chi)^\dagger \left[ P_a^\chi\otimes \operatorname{Tr}_{I}\!\left((P_b\otimes1)X_h(P_b\otimes1)\right) \right]V_h^\chi.

Empty products are identities. For every real $\varepsilon>0$ , there exists a natural number $N$ such that, for every $T\ge N$ and every positive semidefinite $\rho$ of trace $1$ satisfying $\Pi_\phi\rho\Pi_\phi=\rho$ ,

\tfrac12\operatorname{Re}\operatorname{tr} \sqrt{(Y_T(\rho)-M\rho M^\dagger)^\dagger(Y_T(\rho)-M\rho M^\dagger)} \le\varepsilon.

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