Arithmetic complexity

An explicit power saving for the exact discrete Fourier transform

A logarithmic power saving in exact complex arithmetic

31 pages22 claims indexed17 referencesManuscript 2026-09-25

Independent source assessment

Initial source pass recorded 13 October 2026 before opening any completed panel response. Prepared by the Codex curator; this is an AI source assessment, not a human referee certificate. Source: the complete expanded September 25 manuscript at commit 1581d4cbdd69a0faf34b2089614fe2a814316a6a.

Assessment

The main argument supplies a coherent chain from a finite network saving to an all-length exact arithmetic algorithm. The source explicitly charges preparation and index work and uses one supplied, specified root of polynomially bounded order. Its claim does not include finite-precision stability, bounded coefficients, useful crossover lengths, or a bit-complexity improvement. These distinctions matter when comparing the theorem with earlier FFT lower bounds.

This source pass has not established a counterexample or invalid inference in the quantitative main proof. It also does not certify that proof: the complete binary-label schedule and the implementation-level operation ledger still need a dedicated check. Appendix A is a separate symbolic uniformization route and is not needed for the decimal exponent in Corollary 1.2.

Checked identities and source obligations

  • In Section 2, the incidence identity has coefficient (intersection size − 1)/2; the neighbor correction cancels exactly when the intersection has size zero or two. The eight-row replay preserves arbitrary auxiliary contents. Small exact checks cover the incidence identity, while the full three-stage label schedule remains a separate obligation.
  • The role count, padding to 2^71, and integer saving reproduce the displayed fraction 1717850673/590295810358705651712. The recursive normalized inequality is t(k) ≤ A + λ t(floor(k/m)), with complete batches because the relevant power of two is divisible by 2^71. A recurrence alone does not verify that all physical gates satisfy its accounting premises.
  • Section 3's Newton factorization uses nonzero products H_j with j < r and primitive roots. Its Toeplitz update has displacement rank at most three. The second, source-suppressed replay cancels the initial borrowed contents; borrowing an already updated coordinate is therefore compatible with later chunk updates. A toy symbolic replay checks this cancellation.
  • The three-kernel shear factorization is exact. Splitting a possibly zero coefficient into 1+|μ|² and μ−1−|μ|² avoids a zero test. Conjugates are prepared by replacing root leaves in the scalar DAG by inverse roots, not by conjugating variable input.
  • Section 4's prefix enumeration removes a per-entry scan of all axes. The sector start formula is checked on nonconsecutive pair blocks. Tensor composition restores the local word's effect even though other axes modify intermediate borrowed coordinates.
  • Section 5 uses Good's coprime factorization and Bluestein's chirp reduction. The fixed convolution operand's transform is charged as one of three full transforms. The initial odd primes have polynomially bounded local widths; the power-of-two remainder and local preparation are included. The chirp exponent identity and final integer exponent comparison admit direct checks.
  • Appendix A gives local search termination and finite-algebra extraction, then a bounded-printer argument. These are additional proof obligations; their general hypotheses, scalar expansion, and explicit bit records deserve an independent audit. The stronger main bound follows from the explicit network instead.

Reproducible checks and limits

The small-width Newton factorization check was added during post-panel source checking; the initial source assessment and other listed calculations predate opening completed reviews.

See calculation code and results. Small exact examples check identities, not all widths or all physical roles. No target Lean theorem was built, no target axiom inventory was extracted, and no Lean statement comparison was performed for this paper. Companion manuscripts were consulted for scope and citations; they have not received a full independent review in this campaign.

What would settle the remaining obligations

Construct the complete Section 2 binary-label table in a checkable generator, verify every stated subspace transition and arbitrary-role terminal map, and independently count directional calls. Audit the exact-width compiler's topology and all-array indexing against the declared word model. A formal certificate should build the actual target theorem, inspect its axioms, and compare its statement with the manuscript's root, uniformity, and operation-count contract.

Source record

Additional supporting archive items are identified in the original report. View the manuscript hashes and repository snapshot.