Efficient computation: O(ND^5) per fixed-support marginal entry

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.fixed_support_contraction

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

prove2quantum

Fix a support bound $s\ge0$ . There are a constant $C_s>0$ and scalar programs, chosen before all numerical tensor, graph, rotation and operator data, with the following property. For all $N,D\ge1$ , every subset $S$ with $|S|\le s$ , all admissible RAGE data with nonzero raw MPS, and every operator $O$ on $S$ , the program computes all intermediate transfer products, the cross-edge kernel, the positive normalization, every normalized marginal entry, and $\operatorname{tr}(O\rho_S)$ exactly, using

\mathrm{work}\le C_sND^5.

Work counts executed scalar reads, arithmetic, conjugation, and the specified phase evaluations; division by zero fails explicitly. No product-evaluator oracle is allowed. The full output still contains $4^{|S|}$ marginal entries. This is ideal scalar complexity, with the sum-of-Kronecker structure retained; it makes no finite-precision or polynomial-in- $s$ claim. It supplies local and arbitrarily separated two-site expectations.

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 pp.2–3: exact fixed-support computation in O(ND⁵) ideal scalar work, uniformly
in all tensor/graph/rotation/observable data. Entire marginals retain the 4^|S| output size.
No dense D²-by-D² multiplication is treated as an atomic instruction: the implementation
must retain the sum-of-Kronecker structure to meet this bound. Constants and programs precede
all numerical data. A supplied list of local terms is evaluated term by term and summed. -/
theorem fixed_support_contraction :
    ∀ s : ℕ, ∃ C : ℕ, 0 < C ∧
      ∃ programs : (N D : ℕ) → (S : Finset (Fin N)) → MarginalProgram N D S,
      ∀ (N D : ℕ) (S : Finset (Fin N)), 1 ≤ N → 1 ≤ D → S.card ≤ s →
        let p := programs N D S
        p.scalar.calls = 0 ∧ p.scalar.work 0 ≤ C * N * D ^ 5 ∧
        (∀ (A : Tensors N D) (G : PhaseGraph N) (V : Fin N → Matrix.unitaryGroup Bool ℂ)
          (O : Matrix (S → Bool) (S → Bool) ℂ), traceMPS A ≠ 0 → p.Correct A G V O) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 2, Efficient computation: O(ND^5) per fixed-support marginal entry

Read-back

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

For every natural number $s$ , including zero, there exist a positive natural number $C$ and a family assigning a program record $p_{N,D,S}$ to every pair of natural numbers $N,D$ and every subset $S\subseteq I_N=\{0,\ldots,N-1\}$ , such that whenever $N\ge1$ , $D\ge1$ , and $|S|\le s$ , the assigned scalar program has no external product-call instructions and its work is at most $CND^5$ . Work assigns cost $4N+1$ to each external product call and cost $1$ to every other instruction, so here it is the code length. The family and $C$ are chosen before the following data: arbitrary complex $D\times D$ matrices $A_k(b)$ , symmetric real weights $w_{ij}$ with $w_{ii}=0$ and $0\le w_{ij}<2\pi$ , unitary complex $2\times2$ matrices $V_k$ , and an arbitrary complex matrix $O$ indexed by Boolean assignments on $S$ . For every such choice for which the vector

\phi_c=\operatorname{tr}\!\left(A_0(c_0)\cdots A_{N-1}(c_{N-1})\right), \qquad c\in\mathcal B_N=\{\mathrm{false},\mathrm{true}\}^{I_N},

is nonzero, the program has the following execution and output properties. Set $\epsilon(\mathrm{false})=0$ , $\epsilon(\mathrm{true})=1$ , and define

Z=\sum_c|\phi_c|^2,\qquad r_b=\sum_c\left(\prod_k(V_k)_{b_kc_k}\right) \exp\!\left(i\sum_{i<j}w_{ij}\epsilon(c_i)\epsilon(c_j)\right)\phi_c,

R_{ab}= \left(\sum_c|r_c|^2\right)^{-1} \sum_{e:I_N\setminus S\to\{\mathrm{false},\mathrm{true}\}} r_{a\sqcup e}\,\overline{r_{b\sqcup e}},

where $a\sqcup e$ combines assignments on $S$ and its complement. Define

E_k(u,v)=A_k(u)\otimes\overline{A_k(v)},\qquad T_k(a,b)= \begin{cases} E_k(a_k,b_k),&k\in S,\\[2mm] \displaystyle\sum_{u\in\{\mathrm{false},\mathrm{true}\}} e^{\,i\epsilon(u)\sum_{j\in S}w_{jk}(\epsilon(a_j)-\epsilon(b_j))} E_k(u,u),&k\notin S, \end{cases}

with entrywise matrix conjugation, and let $P_t(a,b)=T_0(a,b)\cdots T_{t-1}(a,b)$ , including $P_0=I$ . There exists a final memory $m:\mathbb N\to\mathbb C$ from successful execution of the program such that, writing $L$ for its code length,

\begin{gathered} \operatorname{norm}<L,\quad m(\operatorname{norm})=Z,\qquad \operatorname{expectation}<L,\quad m(\operatorname{expectation})=\operatorname{tr}(OR),\\ \operatorname{stage}(a,b,t,i,j)<L,\quad m(\operatorname{stage}(a,b,t,i,j))=(P_t(a,b))_{ij},\\ \operatorname{cross}(a,b)<L,\quad m(\operatorname{cross}(a,b))=\operatorname{tr}(P_N(a,b)),\\ \operatorname{entry}(a,b)<L,\quad m(\operatorname{entry}(a,b))=R_{ab}. \end{gathered}

The stage equations hold for every pair of assignments $a,b$ on $S$ , every $0\le t\le N$ , and every $i,j\in I_D\times I_D$ ; the cross and entry equations hold for every $a,b$ . Execution starts with all memory zero, writes instruction number $q$ 's result at address $q$ , and uses tensor entries, complex embeddings of weights, rotation entries, and observable entries as inputs. Its available scalar operations are complex constants, input reads, addition, multiplication, division that fails on a zero denominator, conjugation, and $z\mapsto e^{i\operatorname{Re}z}$ ; operand addresses are arbitrary natural numbers, with unwritten addresses still zero. The execution supplies the constant-zero function as the external product evaluator. In the formulas, inverse at zero is zero. The guarantee includes $S=\varnothing$ and $s=0$ ; the family is also defined when $N=0$ or $D=0$ , but no stated bounds or execution guarantees apply there.

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