Asymptotics of parameter-count lower envelopes

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.parameter_count_asymptotics

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

prove2quantum

For $m=2,10$ , set $s=\lfloor n/m\rfloor$ , $D_m=4^m-2\cdot4^{m/2}+1$ , and $A_m(n)=4^n+1-2\cdot4^{m/2}-s(4^m-1)$ . Let $G_m(n)=s+\lceil A_m(n)/D_m\rceil$ and $L_m(n)=1+\lceil A_m(n)/(sD_m)\rceil$ be the balanced lower-envelope expressions in Eqs. (11)-(12). Their limits as $n\to\infty$ are

\frac{G_2(n)}{4^n}\to\frac19,\quad\frac{G_{10}(n)}{4^n}\to\frac1{1046529},\quad\frac{nL_2(n)}{4^n}\to\frac29,\quad\frac{nL_{10}(n)}{4^n}\to\frac{10}{1046529},

\frac{G_{10}(n)}{G_2(n)}\to\frac1{116281},\qquad\frac{L_{10}(n)}{L_2(n)}\to\frac5{116281}.

These are asymptotics of parameter-count thresholds, not achieved synthesis costs. The source rounds the last ratio to $1/23256$ ; a physical duration ratio additionally includes the ratio of single-module durations. Eventual positive $s$ removes any relevance of the totalized expression at small $n$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.5: the four lower-envelope asymptotics and both ratios.
The exact slot ratio is 5/116281; the printed 1/23256 is rounded.
These are parameter-count expressions, with no achieved physical speed-up. -/
theorem parameter_count_asymptotics :
    Filter.Tendsto (fun n : ℕ => (marginalGateBound n 2 : ℝ) / (4 : ℝ) ^ n)
      Filter.atTop (nhds (1 / 9 : ℝ)) ∧
    Filter.Tendsto (fun n : ℕ => (marginalGateBound n 10 : ℝ) / (4 : ℝ) ^ n)
      Filter.atTop (nhds (1 / 1046529 : ℝ)) ∧
    Filter.Tendsto (fun n : ℕ => (marginalSlotBound n 2 : ℝ) * n / (4 : ℝ) ^ n)
      Filter.atTop (nhds (2 / 9 : ℝ)) ∧
    Filter.Tendsto (fun n : ℕ => (marginalSlotBound n 10 : ℝ) * n / (4 : ℝ) ^ n)
      Filter.atTop (nhds (10 / 1046529 : ℝ)) ∧
    Filter.Tendsto (fun n : ℕ => (marginalGateBound n 10 : ℝ) /
      (marginalGateBound n 2 : ℝ)) Filter.atTop (nhds (1 / 116281 : ℝ)) ∧
    Filter.Tendsto (fun n : ℕ => (marginalSlotBound n 10 : ℝ) /
      (marginalSlotBound n 2 : ℝ)) Filter.atTop (nhds (5 / 116281 : ℝ)) := 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. 5, Asymptotics of the parameter-count bounds

Read-back

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

For $m\in\{2,10\}$ and every natural number $n$ , put

q_m(n)=\left\lfloor\frac nm\right\rfloor,\qquad D_m(n)=4^n+1-2\cdot4^{m-\lfloor m/2\rfloor}-q_m(n)(4^m-1), \qquad E_m=4^m-4^{\lfloor m/2\rfloor}-4^{m-\lfloor m/2\rfloor}+1,

and define the integers

G_m(n)=\left\lceil\frac{D_m(n)}{E_m}\right\rceil+q_m(n), \qquad S_m(n)=1+\left\lceil\frac{D_m(n)}{q_m(n)E_m}\right\rceil.

All fractions here are real fractions, division by zero is zero, and the ceiling is integer-valued; in particular, $S_m(n)=1$ for $n<m$ . The theorem asserts all six real limits, with $n$ tending to infinity through the natural numbers:

\begin{aligned} \lim_{n\to\infty}\frac{G_2(n)}{4^n}&=\frac19, & \lim_{n\to\infty}\frac{G_{10}(n)}{4^n}&=\frac1{1046529}, \\ \lim_{n\to\infty}\frac{S_2(n)n}{4^n}&=\frac29, & \lim_{n\to\infty}\frac{S_{10}(n)n}{4^n}&=\frac{10}{1046529}, \\ \lim_{n\to\infty}\frac{G_{10}(n)}{G_2(n)}&=\frac1{116281}, & \lim_{n\to\infty}\frac{S_{10}(n)}{S_2(n)}&=\frac5{116281}. \end{aligned}

The integer values in these limits are regarded as real numbers. Each sequence is defined for every natural $n$ , including $0$ , using the same zero-denominator convention; no restriction to multiples of $2$ or $10$ is imposed.

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