# Reading roadmap: An explicit power saving for the exact discrete Fourier transform

The manuscript proposes a uniform exact DFT speedup by amplifying a finite saving for one two-coordinate kernel. Exact-width Fourier compilation and synchronized tensor sectors transfer that saving to small prime factors; a charged Bluestein reduction covers every length. Appendix A separately develops effective symbolic uniformization.

Source SHA-256: `e9dc36257106c27125cfeb73d82a6af0b4caac4f129012d449b3a097251df921`. Indexed 106,364 characters.

Edges point from prerequisite to consumer. Solid proof edges are attributed inferences, not formal certificates; references remain candidates.

## 1. Freeze the computational question

Read the root and operation contract before comparing bounds.

Claims: thm:main, cor:decimal, cor:polynomial-multiplication

## 2. Obtain and amplify a finite saving

Track arbitrary auxiliary contents, residual dimensions and exact recursive batches.

Claims: net:scalar, net:edge, net:residuals, net:finite-interface, net:indexing, net:tensor-bound

## 3. Compile at the original width

Follow Newton/Toeplitz factorization and dirty-coordinate replay.

Claims: loc:newton-reduction, loc:replay, loc:toeplitz, loc:fourier, loc:compiler

## 4. Synchronize the axes

Pack sectors and charge all prefix traversal and scalar products.

Claims: lem:sector-address, prop:tensor-fourier

## 5. Cover every transform length

Check prime widths, CRT, chirp padding, the fixed-kernel transform and root extraction.

Claims: lem:prime-lengths, sec:all-lengths, thm:main

## Appendix A: a separate qualitative route

Finite algebra extraction and a bounded printer complement the explicit main construction.

Claims: syn:local-certificate, syn:extraction, syn:simulation, syn:printer

## Internal claim index

### Theorem 1.1 — `thm:main`

Source lines 130–137.

Combine a fixed tensor saving, exact-width local Fourier words, synchronized sectors and a chirp reduction at a nearby smooth length. Charge preparation and movement throughout.

- `prop:tensor-fourier` (proof_dependency; source_audit_annotation): Apply Proposition~\ref{prop:tensor-fourier} on the odd-prime axes
- `lem:prime-lengths` (proof_dependency; source_audit_annotation): Substituting~\eqref{eq:axis-count} proves
- `external:good1958` (proof_dependency; source_audit_annotation): We use Good's coprime tensor factorization
- `external:bluestein` (proof_dependency; source_audit_annotation): The reduction is Bluestein's chirp convolution
- `external:motif` (background; source_audit_annotation): We reproduce the network needed here and supply its
- `external:exactfourier` (background; source_audit_annotation): We reproduce the network needed here and supply its
- `syn:section` (excluded_input; source_audit_annotation): The explicit network in the main argument gives the
stronger quantitative conclusion without this search.

Candidate references: `cor:decimal` (candidate_proof_dependency); `eq:working-bounds` (candidate_proof_dependency); `eq:working-transform` (candidate_proof_dependency); `eq:axis-count` (candidate_proof_dependency); `eq:main-bound` (candidate_proof_dependency); `eq:main-constants` (candidate_proof_dependency); `eq:root-size` (candidate_proof_dependency); `net:tensor-bound` (candidate_proof_dependency); `lem:sector-address` (candidate_proof_dependency).

### Corollary 1.2 — `cor:decimal`

Source lines 138–145.

Use the exact integer saving to bound the tensor exponent below 1−2×10⁻¹³, then absorb the fixed log-log factor into another 10⁻¹³ of logarithmic exponent.

- `net:tensor-bound` (proof_dependency; source_audit_annotation): Hence $\theta<1-2\cdot10^{-13}$.

### Corollary 1.3 — `cor:polynomial-multiplication`

Source lines 148–169.

Exact convolution and polynomial multiplication

Zero-pad to length 2n−1, perform two forward transforms and one inverse, and multiply the two variable transformed operands pointwise.

- `thm:main` (proof_dependency; source_audit_annotation): Apply Theorem~\ref{thm:main} at length $M$

Candidate references: `thm:main` (candidate_proof_dependency); `cor:decimal` (candidate_proof_dependency).

### Lemma 2.1 — `net:scalar`

Source lines 311–322.

Subtract the current auxiliary reads, write two incidence summaries, read them, and undo the summaries. Neighbor corrections give RG+JV=I; three invocations exchange the data banks with a sign.

### Lemma 2.2 — `net:edge`

Source lines 383–393.

Walsh-conjugated phase frames differ along orthogonal binary directions. Each residual direction yields a forward C kernel or its inverse; an inverse is corrected by translation.

### Lemma 2.3 — `net:residuals`

Source lines 520–531.

Count residual dimensions for all physical wire roles through the fixed schedule. Norm-one residual bases produce the explicit directional-call saving Δ.

### Proposition 2.4 — `net:finite-interface`

Source lines 615–624.

Finite network interface

Telescope changing frames through the scalar network and correct terminal permutations, signs and translations. All roles, including auxiliaries, undergo the same tensor transform on arbitrary contents.

- `net:scalar` (proof_dependency; source_audit_annotation): Correct these translations
at the sinks and undo the signed bank exchange.
- `net:edge` (proof_dependency; source_audit_annotation): By Lemma~\ref{net:edge}, an edge with residual dimension
- `net:residuals` (proof_dependency; source_audit_annotation): Summing the residual dimensions gives precisely
$s$ directional steps.

Candidate references: `net:telescoping` (candidate_proof_dependency); `net:edge` (candidate_proof_dependency).

### Lemma 2.5 — `net:indexing`

Source lines 667–676.

Enumerate fixed-radix column digits by a prefix tree, accumulating old and new addresses once per extension; collect active bits into contiguous transform fibers in linear work.

### Theorem 2.6 — `net:tensor-bound`

Source lines 725–736.

Pad to 2⁷¹ roles, split k into m-bit columns and spectators, and batch every directional fiber exactly. Normalize total work to t(k)≤A+λt(floor(k/m)); unroll to exponent logₘλ.

- `net:finite-interface` (proof_dependency; source_audit_annotation): On $W$ arrays use Proposition
- `net:indexing` (proof_dependency; source_audit_annotation): After the permutation of

Candidate references: `net:finite-interface` (candidate_proof_dependency); `net:indexing` (candidate_proof_dependency).

### Remark 2.7 — `net:role-remark`

Source lines 812–821.

The recursive interface must hold for arbitrary auxiliary contents, since later batches place arbitrary transform fibers in every role.


Candidate references: `net:scalar` (internal_reference); `net:telescoping` (internal_reference).

### Proposition 3.1 — `loc:compiler`

Source lines 848–871.

Uniform local compiler

Use Newton reduction and a measured workspace compiler to obtain polynomially preparable words on exactly r coordinates. Six forward C slots implement every shear without zero tests.

- `loc:fourier` (proof_dependency; source_audit_annotation): Finally, place each layer from Lemma

### Lemma 3.2 — `loc:newton-reduction`

Source lines 878–890.

Newton reduction

Evaluate monic Newton polynomials at powers of a primitive root. Nonzero H-products factor the lower triangular evaluation matrix into diagonals and Toeplitz; symmetry and LDU uniqueness recover F.

### Lemma 3.3 — `loc:replay`

Source lines 977–989.

Replay with arbitrary borrowed coordinates

Compute into dirty gate coordinates, add outputs and reverse. A second replay omits direct source edges, subtracting the initial-storage contribution and restoring every borrowed coordinate.

### Lemma 3.4 — `loc:toeplitz`

Source lines 1034–1042.

Effective exact-width Toeplitz layers

Split Toeplitz into two diagonal children and a rank-three-displacement cross update. Choose the largest chunk whose printed convolution DAG fits available coordinates; serial replay gives log³ overhead per recursion level.

- `loc:replay` (proof_dependency; source_audit_annotation): Lemma~\ref{loc:replay} implements its

Candidate references: `loc:cross` (candidate_proof_dependency); `loc:displacement-entry` (candidate_proof_dependency); `loc:fit` (candidate_proof_dependency); `loc:chunk-bounds` (candidate_proof_dependency); `loc:replay` (candidate_proof_dependency); `loc:reciprocal` (candidate_proof_dependency); `loc:two-convolutions` (candidate_proof_dependency).

### Lemma 3.5 — `loc:fourier`

Source lines 1195–1202.

Fourier layers at every primitive root

Apply the exact-width Toeplitz compiler to N and its transpose in F=N D⁻¹ Nᵀ, with nonzero denominators inherited from the Newton products.

- `loc:toeplitz` (proof_dependency; source_audit_annotation): Apply Lemma~\ref{loc:toeplitz} to the Toeplitz factor
- `loc:newton-reduction` (proof_dependency; source_audit_annotation): Lemma~\ref{loc:newton-reduction}.  The two diagonal factors

Candidate references: `loc:toeplitz` (internal_reference); `loc:toeplitz` (candidate_proof_dependency); `loc:newton-reduction` (candidate_proof_dependency); `loc:fourier-factorization` (candidate_proof_dependency).

### Lemma 4.1 — `lem:sector-address`

Source lines 1303–1310.

Group ordered pairs and singleton blocks. Accumulate sector start, within-sector offset and original address during one digit traversal, including nonconsecutive original pairs.


Candidate references: `eq:sector-start` (candidate_proof_dependency); `eq:prefix-nodes` (candidate_proof_dependency).

### Proposition 4.2 — `prop:tensor-fourier`

Source lines 1336–1346.

Tensor synchronized slots across all axes. Pair sectors carry C tensor powers; sum their costs over disjoint sectors and multiply by the common local-word depth.

- `loc:compiler` (proof_dependency; source_audit_annotation): Use Proposition~\ref{loc:compiler} on every axis.
- `lem:sector-address` (proof_dependency; source_audit_annotation): A tensor pair slot decomposes into the sectors
- `net:tensor-bound` (proof_dependency; source_audit_annotation): Theorem~\ref{net:tensor-bound} bounds its cost

Candidate references: `loc:compiler` (candidate_proof_dependency); `lem:sector-address` (candidate_proof_dependency); `net:tensor-bound` (candidate_proof_dependency); `eq:tensor-fourier` (candidate_proof_dependency).

### Lemma 5.1 — `lem:prime-lengths`

Source lines 1380–1393.

Bound prime counts using the central binomial coefficient, then bound the product of initial odd primes. Trial division suffices because the largest local prime is polynomial in log n.


Candidate references: `eq:axis-count` (candidate_proof_dependency).

### Lemma A.1 — `syn:local-certificate`

Source lines 1612–1621.

A local certificate for the symbolic search

Turn the explicit multi-role network into an exact-width finite tensor word and add the role axes. A sufficiently large fixed column count absorbs the pointwise shear overhead.


Candidate references: `net:C` (internal_reference); `net:finite-interface` (candidate_proof_dependency); `net:padding` (candidate_proof_dependency); `net:schedule` (candidate_proof_dependency); `loc:nonzero-shear` (candidate_proof_dependency); `net:C` (candidate_proof_dependency).

### Lemma A.2 — `syn:extraction`

Source lines 1665–1674.

Effective finite algebra extraction

Repeatedly test a finite fiber over Q. If it vanishes, Nakayama forces a polynomial elimination relation; a triangular monic change reduces the remaining parameter count.

- `syn:local-certificate` (proof_dependency; source_audit_annotation): Lemma~\ref{syn:local-certificate} gives a complex solution
- `external:stacksNormalization` (proof_dependency; source_audit_annotation): The extraction uses the triangular monic substitution
- `external:stacksNakayama` (proof_dependency; source_audit_annotation): and the determinant form of Nakayama's lemma

### Remark A.3 — `syn:simulation`

Source lines 1764–1777.

Faithful scalar simulation

Represent a fixed rational algebra by multiplication matrices; embed scalars as multiples of its unit and read the first output coordinate to recover the complex transform.

### Theorem A.4 — `syn:printer`

Source lines 1893–1907.

Bounded-printer uniformization

Run an explicit bit printer for floor(log₂n) steps, select an eligible completed radix record, and use mixed-radix/chirp reductions. Its bit length bounds every root order and preparation description.

- `syn:extraction` (proof_dependency; source_audit_annotation): Apply Lemma~\ref{syn:extraction} in a
- `syn:simulation` (proof_dependency; source_audit_annotation): Expand only the fixed algebra $E$ by

Candidate references: `syn:uniform-cost` (candidate_proof_dependency).

## External inputs and references

### [1] exactfourier — `external:exactfourier`

Source lines 2002–2006.

{OpenAI}. {Finite tensor savings and exact Fourier circuits}. 2026. OpenAI Math Release preprint \href{https://github.com/openai/math/blob/main/preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026/main.pdf}{OAI:Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026}.

Finite tensor certificates and positive generation; the main text supplies its own explicit network and compiler.

Role: **companion framework; local mechanism restated**. point. The finite tensor saving and the nonuniform subsequence theorem in Finite tensor savings and exact Fourier circuits~\cite{exactfourier} have an independent proof through matrix prices and exact finite identities. The complex phase network in Integer multiplication below $n\log n$~\cite[Proposition~8 and Section~3.5]{motif} pro

- `thm:main` (background; source_audit_annotation): We reproduce the network needed here and supply its

Candidate references: `section:1` (external_reference); `loc:section` (external_reference); `syn:section` (external_reference).

### [2] motif — `external:motif`

Source lines 2006–2010.

{OpenAI}. {Integer multiplication below $n\log n$}. 2026. OpenAI Math Release preprint \href{https://github.com/openai/math/blob/main/preprints/Integer-multiplication-below-n-log-n-September-23-2026/paper.pdf}{OAI:Integer-multiplication-below-n-log-n-September-23-2026}.

The complex phase-network precursor is credited; integer multiplication precision and tape claims are outside the FFT proof.

Role: **network antecedent; reproduced locally**. oof through matrix prices and exact finite identities. The complex phase network in Integer multiplication below $n\log n$~\cite[Proposition~8 and Section~3.5]{motif} provides a particular two-coordinate kernel with a strict saving. We reproduce the network needed here and supply its uniform array implementation. The integer-multiplication article's arithmetic mod

- `thm:main` (background; source_audit_annotation): We reproduce the network needed here and supply its

Candidate references: `section:1` (external_reference); `net:section` (external_reference).

### [3] cooleytukey — `external:cooleytukey`

Source lines 2010–2013.

Cooley, James W. and Tukey, John W.. An Algorithm for the Machine Calculation of Complex {Fourier} Series. Mathematics of Computation. 1965. \url{https://web.stanford.edu/class/cme324/classics/cooley-tukey.pdf}.

Standard FFT recursion is used in local convolution and the small power-of-two axis.

Role: **background and standard radix construction**. e of replacing a dense linear map by a short sequence of structured operations. The mixed-radix factorization of Cooley and Tukey~\cite{cooleytukey} computes transforms at highly composite lengths in $O(n\log n)$ arithmetic operations. Good's coprime-factor construction identifies certain one-dimensional transforms with tensor products, without i


Candidate references: `section:1` (external_reference).

### [4] bluestein — `external:bluestein`

Source lines 2013–2016.

Bluestein, L. I.. A Linear Filtering Approach to the Computation of Discrete {Fourier} Transform. IEEE Transactions on Audio and Electroacoustics. 1970. \url{https://ieeexplore.ieee.org/document/1162132/}.

The chirp identity transfers arbitrary lengths to convolution; Section 5 writes the identity and charges all three transforms.

Role: **proof input, derived in the manuscript**. es an arbitrary Fourier length to convolution and, with an ordinary FFT, yields the $O(n\log n)$ arithmetic bound at every length~\cite{bluestein}. Rabiner, Schafer, and Rader give the weighted-convolution derivation, padding, and operation count~\cite[Sections~II--III]{rabinerSchaferRader1969}. Improvements within that scale and improvements

- `thm:main` (proof_dependency; source_audit_annotation): The reduction is Bluestein's chirp convolution

Candidate references: `section:1` (external_reference); `sec:all-lengths` (external_reference).

### [5] morgenstern — `external:morgenstern`

Source lines 2016–2019.

Morgenstern, Jacques. Note on a Lower Bound on the Linear Complexity of the Fast {Fourier} Transform. Journal of the ACM. 1973. \url{https://doi.org/10.1145/321752.321761}.

Bounded-coefficient lower bound; the present theorem permits unrestricted coefficients.

Role: **restricted-model background**. permitted operations. Morgenstern's determinant argument applies to the unnormalized Fourier transform with bounded coefficients~\cite{morgenstern}. Ailon's entropy bound concerns the normalized transform on $n$ coordinates with unitary two-coordinate gates~\cite[Theorem~2.1]{ailon}; his later bounds also quantify restrictions on intermediate co


Candidate references: `section:1` (external_reference).

### [6] ailon — `external:ailon`

Source lines 2019–2022.

Ailon, Nir. A Lower Bound for {Fourier} Transform Computation in a Linear Model Over {$2\times2$} Unitary Gates Using Matrix Entropy. 2013. arXiv:1305.4745v1. Version of May 21, 2013. \url{https://arxiv.org/abs/1305.4745v1}.

Unitary two-coordinate lower bound; the compiler includes nonunitary monomial scalings.

Role: **restricted-model background**. ~\cite{morgenstern}. Ailon's entropy bound concerns the normalized transform on $n$ coordinates with unitary two-coordinate gates~\cite[Theorem~2.1]{ailon}; his later bounds also quantify restrictions on intermediate conditioning~\cite{ailonConditioned}. Our model permits unrestricted coefficients and exact intermediate values. The logarithmic word size


Candidate references: `section:1` (external_reference).

### [7] almanrao — `external:almanrao`

Source lines 2022–2025.

Alman, Josh and Rao, Kevin. Faster {Walsh--Hadamard} and Discrete {Fourier} Transforms from Matrix Non-Rigidity. Proceedings of the 55th Annual ACM Symposium on Theory of Computing. 2023. Extended version: arXiv:2211.06459v2. \url{https://arxiv.org/abs/2211.06459v2}.

A real-operation leading-constant improvement for power-of-two DFTs; not a lemma supplying this main proof.

Role: **historical comparator**. non-rigidity to improve the Walsh--Hadamard transform and then the leading constant for power-of-two discrete Fourier transforms~\cite[Theorem~1.2 and Section~7]{almanrao}. Their Fourier bound has leading term $(15/4)n\log_2 n$ in a count of real arithmetic operations, with circuit structure and constants precomputed. Here we obtain a power saving in the logarithm at e


Candidate references: `section:1` (external_reference).

### [8] harveyhoevenlecerf — `external:harveyhoevenlecerf`

Source lines 2025–2029.

Harvey, David and van der Hoeven, Joris and Lecerf, Gr{\'e}goire. Even Faster Integer Multiplication. Journal of Complexity. 2016. The author-hosted manuscript, dated April 26, 2016, discusses Bluestein's chirp reduction in Section 2.5. \url{https://www.texmacs.org/joris/fontart/mul-didot.pdf}.

Prior exposition of chirp reduction; integer multiplication conclusions are not imported.

Role: **bibliography only; no located proof input**. Listed in the bibliography; no literal citation found in the supplied expanded manuscript.

### [9] kailathKungMorf1979 — `external:kailathKungMorf1979`

Source lines 2029–2032.

Kailath, Thomas and Kung, Sun-Yuan and Morf, Martin. Displacement ranks of a matrix. Bulletin of the American Mathematical Society (New Series). 1979. \url{https://doi.org/10.1090/S0273-0979-1979-14659-7}.

Displacement rank motivates the rank-three chunk reconstruction explicitly derived in Section 3.

Role: **method antecedent, formulas restated**. red workspace rule} The matrix representation in the next proof is the displacement-rank construction of Kailath, Kung, and Morf~\cite[Lemmas~1--2]{kailathKungMorf1979}: low-rank shift differences reconstruct a matrix through Toeplitz convolution factors. We give the rectangular-chunk formulas and then fit their computation into the available coordinates. \begin{le


Candidate references: `loc:section` (external_reference).

### [10] good1958 — `external:good1958`

Source lines 2032–2035.

Good, I. J.. The interaction algorithm and practical {Fourier} analysis. Journal of the Royal Statistical Society, Series B (Methodological). 1958. \url{https://doi.org/10.1111/j.2517-6161.1958.tb00300.x}.

Coprime tensor factorization is implemented by explicitly charged CRT permutations.

Role: **proof input, derived in the manuscript**. prime-factor construction identifies certain one-dimensional transforms with tensor products, without intervening twiddle factors~\cite[Sections~11--12]{good1958}; Cooley, Lewis, and Welch explain its relationship with Thomas's construction and the mixed-radix FFT~\cite{cooleyLewisWelch1967}. Bluestein's chirp identity reduces an arbitrary Fourier length to co

- `thm:main` (proof_dependency; source_audit_annotation): We use Good's coprime tensor factorization

Candidate references: `section:1` (external_reference); `sec:all-lengths` (external_reference).

### [11] cooleyLewisWelch1967 — `external:cooleyLewisWelch1967`

Source lines 2035–2038.

Cooley, James W. and Lewis, Peter A. W. and Welch, Peter D.. Historical notes on the fast {Fourier} transform. Proceedings of the IEEE. 1967. \url{https://doi.org/10.1109/PROC.1967.5959}.

Historical relation of Good/Thomas constructions and mixed-radix FFT.

Role: **historical background**. [Sections~11--12]{good1958}; Cooley, Lewis, and Welch explain its relationship with Thomas's construction and the mixed-radix FFT~\cite{cooleyLewisWelch1967}. Bluestein's chirp identity reduces an arbitrary Fourier length to convolution and, with an ordinary FFT, yields the $O(n\log n)$ arithmetic bound at every length~\cite{bluestein}. Rabiner, Schafer,


Candidate references: `section:1` (external_reference).

### [12] rabinerSchaferRader1969 — `external:rabinerSchaferRader1969`

Source lines 2038–2041.

Rabiner, Lawrence R. and Schafer, Ronald W. and Rader, Charles M.. The chirp $z$-transform algorithm. IEEE Transactions on Audio and Electroacoustics. 1969. \url{https://web.ece.ucsb.edu/Faculty/Rabiner/ece259/Reprints/015_czt.pdf}.

Weighted chirp convolution and padding; Section 5 writes its complete formula.

Role: **proof input, formulas restated**. every length~\cite{bluestein}. Rabiner, Schafer, and Rader give the weighted-convolution derivation, padding, and operation count~\cite[Sections~II--III]{rabinerSchaferRader1969}. Improvements within that scale and improvements of the scale itself are different questions. Alman and Rao use matrix non-rigidity to improve the Walsh--Hadamard transform and then the leading cons


Candidate references: `section:1` (external_reference); `sec:all-lengths` (external_reference).

### [13] bennett1973 — `external:bennett1973`

Source lines 2041–2044.

Bennett, Charles H.. Logical Reversibility of Computation. IBM Journal of Research and Development. 1973. \url{https://doi.org/10.1147/rd.176.0525}.

Compute-copy-reverse motivates the first replay; the manuscript additionally proves source-suppressed cancellation.

Role: **method antecedent**. dinates that already carry other data. Its first replay has the compute--copy--reverse pattern of Bennett's reversible simulation~\cite{bennett1973}. Restoring storage with arbitrary initial contents is also the principle of clean transparent computation in catalytic space~\cite[Section~3]{buhrmanEtAl2014}. The source-suppressed second replay bel


Candidate references: `loc:section` (external_reference).

### [14] buhrmanEtAl2014 — `external:buhrmanEtAl2014`

Source lines 2044–2048.

Buhrman, Harry and Cleve, Richard and Kouck{\'y}, Michal and Loff, Bruno and Speelman, Florian. Computing with a Full Memory: Catalytic Space. Proceedings of the Forty-Sixth Annual ACM Symposium on Theory of Computing. 2014. \url{https://doi.org/10.1145/2591796.2591874}.

Catalytic computation motivates restoring arbitrary storage; the required linear identity is proved locally.

Role: **method antecedent**. 973}. Restoring storage with arbitrary initial contents is also the principle of clean transparent computation in catalytic space~\cite[Section~3]{buhrmanEtAl2014}. The source-suppressed second replay below proves the exact cancellation and layer bounds needed here. [Replay with arbitrary borrowed coordinates] Suppose $M:\C^e\to\


Candidate references: `loc:section` (external_reference).

### [15] stacksNormalization — `external:stacksNormalization`

Source lines 2048–2051.

{The Stacks Project Authors}. The Stacks Project: {Noether} normalization. 2026. \url{https://stacks.math.columbia.edu/tag/00OY}. Tags 051M, 051N, 00OX, and 00OY; accessed September 25, 2026.

Triangular monic substitution for finite algebra extraction; the quantitative main theorem does not require it.

Role: **Appendix A method input**. te rational algebra data} The extraction uses the triangular monic substitution from the standard proof of Noether normalization~\cite[Tags 051M, 051N, and 00OX]{stacksNormalization} and the determinant form of Nakayama's lemma~\cite{stacksNakayama}. We give the rational algorithm and its termination proof in full. [Effective finite algebra extraction]\label{syn:ext

- `syn:extraction` (proof_dependency; source_audit_annotation): The extraction uses the triangular monic substitution

Candidate references: `syn:section` (external_reference).

### [16] stacksNakayama — `external:stacksNakayama`

Source lines 2051–2054.

{The Stacks Project Authors}. The Stacks Project: {Nakayama}'s lemma. 2026. \url{https://stacks.math.columbia.edu/tag/00DV}. Tag 00DV; accessed September 25, 2026.

The determinant argument forces a nonzero elimination relation after a zero fiber; excluded from the quantitative main route.

Role: **Appendix A method input**. proof of Noether normalization~\cite[Tags 051M, 051N, and 00OX]{stacksNormalization} and the determinant form of Nakayama's lemma~\cite{stacksNakayama}. We give the rational algorithm and its termination proof in full. [Effective finite algebra extraction] Given finitely many polynomials $f_i$ in $a$ variables ove

- `syn:extraction` (proof_dependency; source_audit_annotation): and the determinant form of Nakayama's lemma

Candidate references: `syn:section` (external_reference).

### [17] ailonConditioned — `external:ailonConditioned`

Source lines 2054–2057.

Ailon, Nir. An {$\Omega((n\log n)/R)$} Lower Bound for {Fourier} Transform Computation in the {$R$}-Well Conditioned Model. 2014. arXiv:1403.1307v5. Version of July 24, 2014. \url{https://arxiv.org/abs/1403.1307v5}.

Well-conditioned model barriers; no stability or conditioning claim is made here.

Role: **restricted-model background**. unitary two-coordinate gates~\cite[Theorem~2.1]{ailon}; his later bounds also quantify restrictions on intermediate conditioning~\cite{ailonConditioned}. Our model permits unrestricted coefficients and exact intermediate values. The logarithmic word size below describes integer addresses; it does not limit the precision of complex registers. The mai


Candidate references: `section:1` (external_reference).

## Coverage and limits

{"mode": "native_latex_index", "claims": 22, "sections": 6, "external_references": 17, "source_bibliography_entries": 17, "unresolved_bibliography": 0, "unresolved": 0}

- Reference edges are not certified proof dependencies. Edge direction is prerequisite → consumer.
- Numbers reflect simple source counters; labels and line anchors are authoritative.
- Extractive statements and proof openings are marked; they are not reconstructed proof gists.
- Macros, included files and custom counters require an expanded source or annotated fallback.
- Appendix A display labels corrected to the PDF; neutral annotations describe proposed proof structure and do not certify validity.