Main properties (iii): completeness when the bond dimension may grow exponentially

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.completeness

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

prove2quantum

Let $N\ge1$ and let $\psi$ be any unit vector in $(\mathbb C^2)^{\otimes N}$ . There exist an integer bond dimension $D$ and periodic trace tensors $A$ such that

1\le D\le2^N,\qquad R(A,0,I)=\psi.

The graph weights and final local rotations can therefore be chosen trivial. This is an exact representability statement with exponential bond dimension allowed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P57

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix

namespace QAlgorithms.Papers.Independent.Intakethird100.P57

attribute [local instance] Classical.propDecidable

/-- PDF p.2, Main properties (iii): exact completeness, explicitly allowing exponential D.
The graph and rotations may be chosen trivial, with the periodic trace convention retained. -/
theorem completeness (N : ℕ) (hN : 1 ≤ N) (v : EuclideanSpace ℂ (Qubits N))
    (hv : IsState v) :
    ∃ D : ℕ, 1 ≤ D ∧ D ≤ 2 ^ N ∧ ∃ A : Tensors N D,
      rage A (emptyPhaseGraph N) (fun _ => 1) = v := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Main properties (iii): completeness when the bond dimension may grow exponentially

Read-back

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

For every natural number $N\ge1$ and every complex vector $v$ indexed by $\{0,1\}^N$ with Euclidean norm $1$ , there exist a natural number $D$ satisfying $1\le D\le2^N$ and complex $D\times D$ matrices $A_k(t)$ , one for each site $k\in\{0,\ldots,N-1\}$ and bit $t$ , such that

v(b)=\operatorname{tr}\!\left(A_0(b_0)\cdots A_{N-1}(b_{N-1})\right) \qquad\text{for every }b\in\{0,1\}^N.

The product uses increasing site order. Equivalently, applying the diagonal phase operator with all weights zero and the product of identity local rotations to this trace-defined vector gives exactly $v$ .

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