§II A example: pairwise nonorthogonal spanning samples are sufficient

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.nonorthogonal_samples_generate

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

prove2quantum

Let a finite normalized pure sample family contain a linearly independent subfamily $\{\phi_j\}_{j=1}^d$ with the same span $H_{\rm in}$ as the entire family. Assume that every pair in this subfamily has nonzero complex inner product. Then

\operatorname{Alg}_{\mathbb C}\{\lvert\phi_k\rangle\langle\phi_k\rvert\}_k=\mathcal L(H_{\rm in}).

Extra sample vectors and their linear dependencies are allowed. This is a sufficient identifiability example, not a necessary condition on every emulator input.

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.3, Eq.(8): pairwise nonorthogonal independent samples are sufficient,
without imposing their pairwise condition on the general emulator results. -/
theorem nonorthogonal_samples_generate [Nonempty J] (phi : K → EuclideanSpace ℂ I) (s : J ↪ K)
    (hphi : ∀ k, IsState (phi k)) (hind : LinearIndependent ℂ (fun j => phi (s j)))
    (hspan : samplePi (pureSamples (fun j => phi (s j))) = samplePi (pureSamples phi))
    (hoverlap : ∀ j k : J, inner ℂ (phi (s j)) (phi (s k)) ≠ 0) :
    Generates (pureSamples phi) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 3, §II A example: pairwise nonorthogonal spanning samples are sufficient

Read-back

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

Let $I$ be a finite coordinate type with decidable equality, let $K,J$ be finite index types with $J$ nonempty, let $\phi_k\in\mathbb C^I$ , and let $s:J\hookrightarrow K$ be injective. Suppose every $\phi_k$ has Euclidean norm $1$ , the selected vectors $(\phi_{s(j)})_{j\in J}$ are complex linearly independent, and $\langle\phi_{s(j)},\phi_{s(k)}\rangle\ne0$ for every $j,k\in J$ , including $j=k$ . For a family $R$ , define $\Pi_R=f(\sum R)$ by continuous functional calculus with $f(0)=0$ and $f(t)=1$ for $t\ne0$ , and suppose

\Pi_{(|\phi_{s(j)}\rangle\langle\phi_{s(j)}|)_{j\in J}} = \Pi_{(|\phi_k\rangle\langle\phi_k|)_{k\in K}}.

Writing $S_k=|\phi_k\rangle\langle\phi_k|$ , whose $(u,v)$ -entry is $\phi_k(u)\overline{\phi_k(v)}$ , the conclusion is that, for every complex matrix $X$ on $I$ , $X$ belongs to the complex linear span of all nonempty finite products of the $S_k$ if and only if $\Pi_S X\Pi_S=X$ . A singleton $J$ is allowed; an empty $I$ is incompatible with the normalized selected vectors.

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