The mathematical object being transported

The word bridge is useful only when its arrows have definitions. In the present example the common object is a selector: a diagonal operator that retains certain Fourier coordinates and discards the others. Arithmetic supplies the selected labels. Fourier synthesis expresses that selector in sample coordinates. Complex normalization then supplies a unitary transformation and the state vectors used in a quantum interpretation.

The basic identity is

Here \(D\) is a diagonal zero-or-one matrix, \(F\) is unitary, and \(\dagger\) denotes conjugate transpose. Consequently \(P\) is an orthogonal projector. The transformation \(F\) is reversible. The selection \(P\) need not be. A complete decomposition consists of both \(Px\) and \((I-P)x\), whose sum recovers \(x\).

This distinction determines what can be transported. A Fourier basis change preserves dimension, inner products, norms, and the entire vector. A projector preserves only its selected component. Measurement probabilities discard still more information. The same exact operator can appear in arithmetic, signal processing, and finite-dimensional quantum theory, while those uses retain different observables and have different implementation costs.

We work over \(\mathbb C\) for Fourier transformations and use \(\mathbb Q\) for the rational kernels. All index sets in the main finite construction are specified, and no limit argument is needed. A packet in this chapter means a component together with its stated realization map. This definition does not turn every kind of component into the same object. Character-order packets and coefficient-residue lanes will be distinguished explicitly in the polyphase section.

Permalink · Source line 36

The labels QA01 through QA20 refer to mathematical statements in this paper. They are not a count of Lean declarations. A single claim can use several formal lemmas, and a general theorem can have a formally checked specialization rather than a generic Lean proof.

We use three evidence descriptions. A general prose theorem has a proof below for all inputs satisfying its hypotheses. A formal specialization is an actual declaration in the preserved modulus-twelve source. A finite computational check is a bounded verification of an implementation. These descriptions can support the same identity, but they are not interchangeable. The Lean guide gives the exact declaration mapping.

The central example uses the vectors

These are the literal coefficients of the formal source, and \(x=c+b\). Keeping one example fixed makes every arrow independently checkable.

Permalink · Source line 76