QFT occurrence counts and modeled quality

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.qft_quality_counts

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

prove2quantum

Assign each $QFT_m$ occurrence fidelity $F_Q\in[-1,1]$ and each type- $j$ phase-swap occurrence fidelity $F_j\in[-1,1]$ . With independent occurrence errors, assigned schedule duration $T\ge0$ , and $T_R>0$ , the modeled quality of the Fig. 7 circuit for $m,k\ge2$ is

q=F_Q^k\prod_{j=1}^{k-1}F_j^{k-j}\,e^{-T/T_R}.

For $2k$ blocks of size five, $k\ge2$ , after truncation identifies every type $j\ge3$ with the same pure-swap module, write $F_5$ for the five-qubit Fourier fidelity and $F_1,F_2,F_3$ for the three remaining module fidelities. Then

q=F_5^{2k}F_1^{2k-1}F_2^{2k-2}F_3^{\binom{2k}{2}-4k+3}e^{-T/T_R}.

The fidelity product is computed from the actual circuit list. The second expression concerns the approximating circuit. Its elapsed duration is assigned independently of the deferred timing formula (25).

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.10, Eqs. (26)-(27): occurrence-count quality formulas. In the
second formula, all phase-swap types j>=3 have been replaced by the same
truncated pure-swap module. T is an assigned elapsed time, without Eq. (25). -/
theorem qft_quality_counts (Fq : ℝ) (Fc : ℕ → ℝ) (T TR : ℝ)
    (hT : 0 ≤ T) (hTR : 0 < TR)
    (hFq : Fq ∈ Set.Icc (-1) 1) (hFc : ∀ j, Fc j ∈ Set.Icc (-1) 1) :
    (∀ m k : ℕ, 2 ≤ m → 2 ≤ k →
      blockQuality Fq Fc T TR (qftAssembly m k) =
        Fq ^ k * (∏ j ∈ Finset.Icc 1 (k - 1), Fc j ^ (k - j)) *
          Real.exp (-T / TR)) ∧
    (∀ (k : ℕ) (F5 F1 F2 F3 : ℝ), 2 ≤ k →
      F5 ∈ Set.Icc (-1) 1 → F1 ∈ Set.Icc (-1) 1 →
      F2 ∈ Set.Icc (-1) 1 → F3 ∈ Set.Icc (-1) 1 →
      blockQuality F5 (fun j => if j = 1 then F1 else if j = 2 then F2 else F3)
        T TR (truncatedQftAssembly 5 (2 * k) 10) =
        F5 ^ (2 * k) * F1 ^ (2 * k - 1) * F2 ^ (2 * k - 2) *
          F3 ^ (Nat.choose (2 * k) 2 - (4 * k - 3)) * Real.exp (-T / TR)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 10, QFT counts and model quality, Eqs. (26)–(27)

Read-back

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

For all real numbers $F_q,T,T_R$ and functions $F_c:\mathbb N\to\mathbb R$ , assume $T\ge0$ , $T_R>0$ , $-1\le F_q\le1$ , and $-1\le F_c(j)\le1$ for every natural number $j$ , including $0$ . Define the quality of a list to be the product of its step weights multiplied by $e^{-T/T_R}$ , assigning weight $F_q$ to a Fourier step, $F_c(j)$ to either kind of phase-swap step of index $j$ , and $F_c(3)$ to a swap. The theorem asserts both of the following equalities:

Q(\mathcal A_{m,k}) =F_q^k\left(\prod_{j=1}^{k-1}F_c(j)^{k-j}\right)e^{-T/T_R} \quad\text{for every }m,k\in\mathbb N\text{ with }m\ge2,\ k\ge2,

where $\mathcal A_{m,k}$ is formed by concatenating, for $t=0,\ldots,k-1$ in increasing order, the phase-swap steps with offset $sm$ , half-width $m$ , and phase index $s+1$ , for $s=t-1,\ldots,0$ in decreasing order, followed by a Fourier step of offset $0$ and width $m$ ; for $t=0$ , that portion contains only the Fourier step. Also, for every $k\in\mathbb N$ with $k\ge2$ and every four real numbers $F_5,F_1,F_2,F_3\in[-1,1]$ ,

Q_{F_5,f}(\mathcal T_k) =F_5^{2k}F_1^{2k-1}F_2^{2k-2} F_3^{\binom{2k}{2}-(4k-3)}e^{-T/T_R}, \qquad f(j)= \begin{cases} F_1&j=1,\\ F_2&j=2,\\ F_3&\text{otherwise}. \end{cases}

Here $Q_{F_5,f}$ uses the same weighting rule with Fourier weight $F_5$ and phase weights $f$ , and $\mathcal T_k$ is formed from $\mathcal A_{5,2k}$ by replacing each phase-swap step of offset $o$ and index $j$ by a swap of offset $o$ and half-width $5$ if $10<5(j-1)+1$ , and otherwise by a truncated phase-swap step with the same offset, half-width, and index and cutoff $10$ . The subtraction $j-1$ in this rule is natural-number subtraction, truncated at zero; the generated indices are all positive. Every exponent displayed above is a natural number, and the stated bounds on $k$ make all the displayed subtractions nonnegative. The second equality uses independently quantified weights $F_5,F_1,F_2,F_3$ , while all the initial hypotheses remain assumptions of the conjunction.

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