Strong simulation for fixed-degree observables in product-operator CAR representations

Open

QAlgorithms.Papers.Independent.Intakethird100.P77.boundedDegree_strongSimulation

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

prove2quantum

Fix a degree bound $d$ independently of the instance. For each effectively described circuit instance $s$ , select an existing output wire $k_s$ . Supply Hermitian CAR generators as products of one-qubit operators, a product of normalized one-qubit input states, and a list of real antisymmetric quadratic Gaussian coefficients. Supply a canonical ordered square-free polynomial $P_s$ representing $Z_{k_s}$ with degree at most $d$ . Structure, the selected wire, generator factors, gate coefficients, input amplitudes and $P_s$ have polynomial-time finite descriptions to requested precision. A single deterministic polynomial-time machine, selected before $s$ , precision $m$ and outcome $b$ , approximates the selected one-wire probability to error $2^{-m}$ .

For each length- $r$ word in $P_s$ , with $U_s$ the circuit and $R_s$ its Heisenberg rotation,

U_s^\dagger c_{i_1}\cdots c_{i_r}U_s=\sum_{j_1,\ldots,j_r}\left(\prod_{a=1}^r(R_s)_{i_a j_a}\right)c_{j_1}\cdots c_{j_r},\qquad \#\text{tuples}=(2n_s)^r\le(2n_s)^d.

The expansion includes repeated indices and the empty word. The supplied polynomial has at most $\sum_{r=0}^d\binom{2n_s}{r}$ terms. This is a per-monomial count; runtime also charges circuit size, descriptions and precision. Other output wires need no bounded-degree or effective polynomial representation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P77

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P77

open QAlgorithms

open QAlgorithms.Complexity (Str)

open QAlgorithms.Papers.Independent.Advance50.P19 (Major CARSystem)

open QAlgorithms.Papers.Independent.Information100.P32 (Op)

open scoped BigOperators Matrix ComplexConjugate

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.10 Theorem 4: fixed-degree observables on product-operator CAR
representations, for the selected measured wire only. Other Z observables
need not have bounded degree. The tuple bound is per monomial. The total runtime also
includes circuit length, all representation/coefficient descriptions, and m.
The canonical polynomial may have up to the displayed sum of binomial counts. -/
theorem boundedDegree_strongSimulation (d : ℕ) (F : GaussianFamily)
    (I : ProductInputs F.width) (hF : F.Effective)
    (hI : EffectiveNumbers I.data)
    (hdegree : ∀ s, (F.observable s).DegreeLE d) :
    SelectedStrongSimulation (fun s b =>
      singleWireProbability (gaussianCircuit (F.system s).majorana (F.gates s))
        (prodState (I.factor s)) (F.measured s) b) ∧
    (∀ s,
      (F.observable s).terms.length ≤
        ∑ r ∈ Finset.range (d + 1), Nat.choose (2 * F.width s) r) ∧
    (∀ s t, t ∈ (F.observable s).terms →
      Fintype.card (Fin t.1.length → Major (F.width s)) =
        (2 * F.width s) ^ t.1.length ∧
      Fintype.card (Fin t.1.length → Major (F.width s)) ≤ (2 * F.width s) ^ d ∧
      star (gaussianCircuit (F.system s).majorana (F.gates s)) *
          majoranaWord (F.system s).majorana t.1 *
          gaussianCircuit (F.system s).majorana (F.gates s) =
        expandedWord (F.system s).majorana (circuitRotation (F.gates s)) t.1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P77

end

Source

Matchgates and classical simulation of quantum circuits, arXiv:0804.4050v2, PDF p. 10, Theorem 4: bounded-degree observable simulation for product-operator CAR representations

Read-back

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

For every natural number $d$ , every Gaussian family $F$ , and every family of single-qubit vectors $\phi_{s,k}\in\mathbb C^2$ with $\|\phi_{s,k}\|=1$ , indexed by finite Boolean strings $s$ and wires $k<n(s)$ , assume the following effectiveness and degree conditions. The family’s structural code is polynomial-time computable, and its numerical data is effectively approximable; the same numerical approximation condition holds for the input list $[\phi_{s,0}(\mathrm{false}),\phi_{s,0}(\mathrm{true}),\ldots]$ . The structural code encodes, in order, the unary width, unary gate count, unary measured-wire index, and the nested list of unary indices in the observable words. The numerical data lists all four entries of each generator factor, then all real gate-matrix entries as complex numbers, then the observable coefficients, in their respective stored orders. Precisely, for each numerical-data list $D(s)$ there is a polynomial-time string function $a$ such that, for all valid positions $j<|D(s)|$ , natural precisions $m$ , and Booleans $b$ ,

\left|\operatorname{dyad}_m\!\left(a\!\left(\operatorname{tuple}[s,1^j,1^m,[b]]\right)\right) -\begin{cases}\operatorname{Im}D(s)_j,&b=\mathrm{true},\\ \operatorname{Re}D(s)_j,&b=\mathrm{false} \end{cases}\right|\le2^{-m}.

Here tuple encoding prefixes every constituent string by its unary length and a false bit, and $\operatorname{dyad}_m$ reads the output’s first bit as a negative-sign flag and its remaining bits as a binary magnitude divided by $2^m$ , with empty strings representing zero. Assume also that every stored observable word has length at most $d$ . To specify the conclusion, fix $s$ , put $n=n(s)$ , and let $c_i$ , $i<2n$ , be the family’s Hermitian matrices satisfying $c_ic_j+c_jc_i=2\delta_{ij}I$ ; their entries factor as $(c_i)_{x,y}=\prod_{k<n}(F_{i,k})_{x_k,y_k}$ . The stored observable is a sum $\sum_{(w,\alpha)}\alpha c_{w_1}\cdots c_{w_{|w|}}=Z_q$ , where its words are distinct and strictly increasing, $q<n$ is the measured wire, and $Z_q$ acts by $\operatorname{diag}(1,-1)$ on wire $q$ and identity elsewhere. For each stored skew-symmetric real matrix $h$ , define

H_h=\mathrm i\sum_{\substack{i,j<2n\\i\ne j}}h_{ij}c_ic_j,\qquad G_h=e^{\mathrm iH_h}.

If the gate list is $h_1,\ldots,h_L$ , set

U_s=G_{h_L}\cdots G_{h_1},\qquad R_s=e^{-4h_L}\cdots e^{-4h_1},\qquad \Psi_s(x)=\prod_{k<n}\phi_{s,k}(x_k).

Then there exists a polynomial-time string function $f$ such that, for every $s$ , every $m\in\mathbb N$ , and both Booleans $b$ ,

\left|\operatorname{dyad}_m\!\left(f(\operatorname{tuple}[s,1^m,[b]])\right) -\sum_{\substack{x\in\{0,1\}^{n(s)}\\x_q=b}}|(U_s\Psi_s)(x)|^2\right|\le2^{-m}.

Furthermore, for every $s$ , the number of stored observable terms, including any with zero coefficient, is at most

\sum_{r=0}^{d}\binom{2n(s)}r.

Finally, for every stored term $(w,\alpha)$ , writing $r=|w|$ , the set of all functions from $\{0,\ldots,r-1\}$ to $\{0,\ldots,2n-1\}$ has cardinality $(2n)^r\le(2n)^d$ , and

U_s^\dagger c_{w_1}\cdots c_{w_r}U_s = \sum_{j:\{0,\ldots,r-1\}\to\{0,\ldots,2n-1\}} \left(\prod_{a=0}^{r-1}(R_s)_{w_{a+1},j(a)}\right) c_{j(0)}\cdots c_{j(r-1)}.

The conclusions include $d=0$ , empty words, empty gate lists, and precision $m=0$ ; empty matrix products are identities and empty scalar products are $1$ . The measured-wire field ensures $n(s)>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