Strong simulation of global Jordan–Wigner Gaussian circuits

Open

QAlgorithms.Papers.Independent.Intakethird100.P77.jordanWigner_strongSimulation

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

prove2quantum

Use the Jordan–Wigner generators $c_{2k-1}=Z_1\cdots Z_{k-1}X_k$ and $c_{2k}=Z_1\cdots Z_{k-1}Y_k$ . Let a uniformly described polynomial-size circuit consist of arbitrary Gaussian gates $e^{iH}$ , where $H=i\sum_{\mu\ne\nu}h_{\mu\nu}c_\mu c_\nu$ and $h$ is real antisymmetric. Let the input be any product of normalized one-qubit states. All quadratic coefficients and input amplitudes are given by effective polynomial-time bit descriptions. There is one deterministic polynomial-time simulator, selected before the input, wire $k$ , outcome $b$ , and precision $m$ , whose dyadic output satisfies

|q-p_b|\le2^{-m}.

Gate descriptions, circuit size, and requested precision are charged. These gates may act globally; no locality restriction or Gaussian/parity restriction on the product input is added. The result relies on the bounded-degree observable $Z_k=-ic_{2k-1}c_{2k}$ .

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 pp.10--11 unnumbered Gaussian simulation result. Product inputs need
not be Gaussian and need not have definite fermionic parity. -/
theorem jordanWigner_strongSimulation (F : JWFamily) (I : ProductInputs F.width)
    (hF : F.Effective) (hI : EffectiveNumbers I.data) :
    StrongSimulation F.width (fun s k b =>
      singleWireProbability (gaussianCircuit (jordanWigner (F.width s)) (F.gates s))
        (prodState (I.factor s)) k b) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P77

end

Source

Matchgates and classical simulation of quantum circuits, arXiv:0804.4050v2, PDF p. 10, Section 5: arbitrary Jordan–Wigner Gaussian circuits are strongly simulatable

Read-back

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

For every JW family $F$ , assigning each finite Boolean string $s$ a width $n_s$ and a finite ordered list $h_0,\ldots,h_{L_s-1}$ of real skew-symmetric $2n_s\times2n_s$ matrices, and every family of input vectors $\phi_{s,k}\in\mathbb C^2$ satisfying $\|\phi_{s,k}\|=1$ , assume that $F$ ’s structural encoding is polynomial-time computable and that its gate entries and the input-vector entries are polynomial-time approximable. Explicitly, let $\mathcal T(w_1,\ldots,w_q)$ concatenate $1^{|w_r|}0w_r$ , with $1^j$ denoting $j$ true bits; the structural encoding is $\mathcal T(1^{n_s},1^{L_s})$ . The gate data list contains every matrix entry, embedded into $\mathbb C$ , in gate order and then increasing row and column order; the input data list contains $\phi_{s,k}(\mathrm{false}),\phi_{s,k}(\mathrm{true})$ in increasing wire order. For each of these numerical lists $D_s$ , the approximation assumption means that there exists a polynomial-time Boolean-string function whose signed dyadic value on $\mathcal T(s,1^j,1^m,[b])$ differs by at most $2^{-m}$ from the real component of $D_s[j]$ when $b$ is false and its imaginary component when $b$ is true, for every valid $j$ and natural $m$ . Define $c_{2q}=Z^{\otimes q}\otimes X\otimes I^{\otimes(n_s-q-1)}$ and $c_{2q+1}=Z^{\otimes q}\otimes Y\otimes I^{\otimes(n_s-q-1)}$ for $q<n_s$ , where $X=\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ , $Y=\left(\begin{smallmatrix}0&-\mathrm i\\\mathrm i&0\end{smallmatrix}\right)$ , and $Z=\operatorname{diag}(1,-1)$ in Boolean order. Put

H(h)=\mathrm i\sum_{i\ne j}h_{ij}c_ic_j,\qquad U_s=\exp(\mathrm iH(h_{L_s-1}))\cdots\exp(\mathrm iH(h_0)),\qquad \psi_s(x)=\prod_{k=0}^{n_s-1}\phi_{s,k}(x_k).

The assertion is that there exists a polynomial-time Boolean-string function $f$ such that, for every string $s$ , natural precision $m$ , wire $k<n_s$ , and Boolean $b$ ,

\left|\operatorname{dyad}_m\!\left(f(\mathcal T(s,1^m,1^k,[b]))\right) -\sum_{x:x_k=b}|(U_s\psi_s)(x)|^2\right|\le 2^{-m}.

A signed dyadic output uses the first bit as the sign, negative when true, the remaining bits as a most-significant-bit-first binary magnitude, and denominator $2^m$ , with an empty output representing zero. Empty gate lists use $U_s=I$ . Zero widths and precision zero are included; at zero width there is no output-wire index and hence no output approximation condition for that string.

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