Circuit simulation: controlled-phase gates update graph weights exactly

Open

QAlgorithms.Papers.Independent.Intakethird100.P57.exact_phase_gate_update

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

prove2quantum

Let $N,D\ge1$ , let $A,\Phi$ be admissible data, take final rotations $V=I$ , and let $j\ne k$ . For any real angle $\theta$ , update the two symmetric entries of the selected edge to $(\Phi_{jk}+\theta)\bmod 2\pi\in[0,2\pi)$ , leaving every other entry fixed. The resulting graph $\Phi'$ is admissible and

R(A,\Phi',I)=U_{jk}(\theta)R(A,\Phi,I).

If the raw MPS is nonzero, normalization gives the same equality for unit vectors. Negative input angles are allowed. The gate acts once on the unordered pair; the simple rule applies in the stated $V=I$ setting.

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.3–4, circuit update: with V=I, phase gates are exact graph-weight updates.
The same equality is asserted for normalized states only when the raw MPS is nonzero. -/
theorem exact_phase_gate_update {N D : ℕ} (hN : 1 ≤ N) (hD : 1 ≤ D)
    (A : Tensors N D) (G : PhaseGraph N) (j k : Fin N) (hjk : j ≠ k) (theta : ℝ) :
    ∃ Gnew : PhaseGraph N, Gnew.weight = updatedWeights G j k theta ∧
      rage A Gnew (fun _ => 1) = controlledPhaseAction j k (Complex.exp (Complex.I * (theta : ℂ)))
        (rage A G (fun _ => 1)) ∧
      (traceMPS A ≠ 0 → IsState (normalizeRageVector (rage A Gnew (fun _ => 1))) ∧
        normalizeRageVector (rage A Gnew (fun _ => 1)) =
          controlledPhaseAction j k (Complex.exp (Complex.I * (theta : ℂ)))
            (normalizeRageVector (rage A G (fun _ => 1)))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P57

end

Source

Renormalization algorithm with graph enhancement, arXiv:0802.1211v1, PDF p. 3, Circuit simulation: controlled-phase gates update graph weights exactly

Read-back

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

For every pair of natural numbers $N,D$ with $1\le N$ and $1\le D$ , every collection of complex $D\times D$ matrices $A_r^s$ , every graph $G$ with real weights $w_{rs}=w_{sr}$ , $w_{rr}=0$ , and $0\le w_{rs}<2\pi$ , every pair of distinct sites $j,k<N$ , and every real $\theta$ , there exists a graph $G_{\mathrm{new}}$ satisfying the same symmetry, zero-diagonal, nonnegativity, and strict $2\pi$ bounds, whose weights are

w'_{ab}= \begin{cases} w_{jk}+\theta-2\pi\left\lfloor\dfrac{w_{jk}+\theta}{2\pi}\right\rfloor, &(a,b)=(j,k)\text{ or }(a,b)=(k,j),\\[4pt] w_{ab},&\text{otherwise}. \end{cases}

To state the remaining conclusions, define $T(b)=\operatorname{tr}(\prod_{r=0}^{N-1}A_r^{b_r})$ , using increasing site order, and $v_G(b)=e^{i\sum_{r<s,\ b_r=b_s=1}w_{rs}}T(b)$ ; this is the vector obtained using identity single-site rotations. Let $C_\theta$ multiply an amplitude by $e^{i\theta}$ when $b_j=b_k=1$ , and by $1$ otherwise, and define $n(v)=\|v\|^{-1}v$ , with $n(0)=0$ . The graph can be chosen so that

v_{G_{\mathrm{new}}}=C_\theta v_G, \qquad T\ne0\ \Longrightarrow\ \left(\|n(v_{G_{\mathrm{new}}})\|=1 \ \text{ and }\ n(v_{G_{\mathrm{new}}})=C_\theta n(v_G)\right).

The nonzero condition is required only for the conditional conclusion, not for existence of the graph or the unnormalized equality. When $N=1$ , the required distinct sites cannot be supplied.

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