quantum Fourier transform

Fourier's transform run as a single reversible motion of a quantum register -- the lens that turns hidden periods and phases into things a measurement can land on.

proved in corpus · proved here, no imported axiomsLean qft_unitary

In plain terms

Here is the problem. Quantum interference only helps you if the structure you care about -- a repeating period, an invisible phase -- can be steered onto outcomes a measurement actually produces. You need a lens that focuses spread-out regularity into sharp peaks.

The quantum Fourier transform is that lens. It is the ordinary discrete Fourier transform, the workhorse of signal processing, executed as one physical evolution of the register rather than as arithmetic on a list of numbers. Feed it a state whose amplitudes repeat with some period and the output piles up at the frequencies of that period.

Shor's algorithm is the famous customer: load a modular sequence, apply the transform, and the period that encodes the factors stands out like a struck bell.

In CSD

A Cat-1 library primitive, deliberately CSD-free: the N-level transform matrix with its unitarity proved from roots-of-unity orthogonality -- a geometric series, nothing deeper. The algorithm witnesses (Shor's algorithm, phase estimation) consume it; the standing disclaimer applies, the algorithms consume the unitary pillar and do not support foundations.

The transform is defined at a general level count N, not just powers of two, so it is directly the discrete Fourier unitary; the qubit case is an instance.

Mathematically

F j k = (1/sqrt N) omega^{jk} with omega = exp(2 pi i / N) a primitive N-th root of unity; unitarity F^H F = 1 is the orthogonality sum over k of zeta^k = N [zeta = 1], closed by the geometric series (qft_unitary).

Matrix level only: the corpus states the transform as an N x N unitary and proves its algebra; no gate-level circuit decomposition is claimed.

The name

Joseph Fourier (1768-1830) was an orphan from Auxerre who taught at the Ecole Polytechnique, governed Lower Egypt under Napoleon, and administered the Isere from Grenoble -- where, between prefectural duties, he wrote the analytical theory of heat. His claim that arbitrary functions decompose into sines scandalised Lagrange and became the spine of applied mathematics anyway.

The quantum version arrived with Shor's 1994 paper and its predecessors: the insight that the transform's butterfly structure makes it exponentially cheap as a quantum circuit, which is exactly what period-finding needed.

Module
CsdLean4/Mathlib/QuantumInfo/Fourier.lean
Background
Overview
Related
phase estimation, shor algorithm, deutsch jozsa

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy