Main properties: polynomial-size parameter description

Proved

QAlgorithms.Papers.Independent.Intakethird100.P57.parameter_description

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

prove2quantum

For a chain of $N\ge1$ qubits and bond dimension $D\ge1$ , store the real and imaginary parts of the two complex site matrices, one real graph weight for each unordered pair, and all real and imaginary entries of each local $2\times2$ unitary. This description is injective on the admissible data and uses

P(N,D)=4ND^2+\frac{N(N-1)}2+8N

real entries. In particular, there is an absolute constant $C>0$ , independent of $N,D$ and of all numerical data, such that

P(N,D)\le C(ND^2+N^2).

This is a description-size statement in $N$ and $D$ . The unitary, graph-symmetry and angle constraints remain imposed; the count does not concern independent manifold coordinates or finite-precision bit storage.

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: an injective description with an absolute uniform bound.
This counts real entries, not intrinsic coordinates or bounded-precision bits. -/
theorem parameter_description :
    (∀ (N D : ℕ), 1 ≤ N → 1 ≤ D → Function.Injective (@describe N D)) ∧
    (∀ (N D : ℕ), 1 ≤ N → 1 ≤ D → Fintype.card (DescriptionIndex N D) =
      4 * N * D ^ 2 + N * (N - 1) / 2 + 8 * N) ∧
    (∃ C : ℕ, 0 < C ∧ ∀ N D : ℕ, 1 ≤ N → 1 ≤ D →
      Fintype.card (DescriptionIndex N D) ≤ C * (N * D ^ 2 + N ^ 2)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Main properties: polynomial-size parameter description

Read-back

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

The following three statements hold jointly. For every pair of natural numbers $N,D$ with $N\ge1$ and $D\ge1$ , consider records consisting of arbitrary complex $D\times D$ matrices $A_{k,b}$ for each site $k<N$ and Boolean $b$ , symmetric real weights $w_{jk}$ with zero diagonal and $0\le w_{jk}<2\pi$ , and Boolean-indexed unitary $2\times2$ complex matrices $V_k$ . Encode such a record as a real-valued function whose coordinates are the real and imaginary parts of every tensor entry, the weights $w_{jk}$ for $j<k$ , and the real and imaginary parts of every rotation entry, with these three kinds of coordinates distinguished. First, this encoding is injective: two such records with identical values at every coordinate are equal. Second, the number of coordinates is exactly

4ND^2+\frac{N(N-1)}2+8N.

Here subtraction and division in the displayed count are natural-number subtraction and integer division. Third, there exists a single natural number $C>0$ such that, for every $N,D\ge1$ , the number of these coordinates is at most

C\bigl(ND^2+N^2\bigr).

The assertions impose no normalization condition on the tensor matrices and make no claim for $N=0$ or $D=0$ .

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