1.6 Coefficient-residue lanes and polyphase transport
On this page · Permalink · Source line 518
There is a second exact decomposition that is common in Komorebi calculations and in signal processing. It separates positions by residue class rather than separating Fourier characters by order. Both decompositions use projectors, but they select different objects.
1.6.1 Formal coefficient lanes
On this page · Permalink · Source line 527
Let \(L\ge1\) and let \(f(z)=\sum_{n\ge0}a_nz^n\) be a formal power series over a field containing a primitive \(L\)th root \(\omega\) and \(1/L\). For \(0\le r<L\), define
The first expression addresses the lane in a new variable. The second places that lane back at its original coefficient positions.
Theorem QA08: Exact coefficient-residue decomposition
The coefficient-residue maps satisfy
Proof
The coefficient of \(z^n\) in the first right-hand side is
Character orthogonality makes it \(a_n\) when \(n\equiv r\pmod L\) and zero otherwise. This is precisely the coefficient of \(R_rf\). Each coefficient position belongs to a unique lane, so the projector and completeness identities follow coefficientwise. The equality is formal, with no analytic convergence hypothesis. \(\square\)
For an infinite analytic series, the same identity holds wherever all displayed evaluations are defined, but the formal theorem does not need that interpretation. The lane index is an exponent residue. It is not a multiplicative-order class of a Fourier character.
1.6.2 Finite polyphase lanes
On this page · Permalink · Source line 577
Now suppose \(N=LM\) with positive integers \(L\) and \(M\). For a vector \(x\in\mathbb C^N\), define its \(L\) lanes by
The addressing map \(T:x\mapsto(x_0,\ldots,x_{L-1})\) is bijective. Interleaving the lanes reconstructs \(x\), and
This energy identity is an exact reindexing. It is useful to preserve it separately from the spectral aliasing identity that follows.
Theorem QA09: Polyphase Fourier identities and decimation aliasing
Write \(\widehat{x_r}\) for the unscaled \(M\)-point transform of lane \(r\). Then for \(k\in I_N\),
Conversely, for \(\ell\in I_M\),
Proof
Partition the \(N\) samples by their unique representation \(n=r+Lm\):
The inner sum is \(\widehat{x_r}(k\bmod M)\), proving the first identity. For the second, insert Fourier inversion into the lane transform:
QA02 makes the inner sum \(M\) exactly when \(k=\ell+jM\) for some \(0\le j<L\). Since \(M/N=1/L\), this is the second displayed identity. \(\square\)
Every lane transform combines an alias class of \(L\) full-spectrum coefficients. One decimated lane generally cannot distinguish those coefficients. All \(L\) offsets together retain the original signal. For a fixed alias class \(\ell\), the equations across \(r\) are an invertible Fourier mixing system after the nonzero phases \(\zeta_N^{r\ell}\) are removed. The apparent collapse is resolved by preserving the complete collection of offsets.
1.6.3 Why the two projectors must not be conflated
On this page · Permalink · Source line 657
A coefficient-residue selector keeps samples such as \(x(0),x(3),x(6),x(9)\). A character-order projector keeps spectral modes such as \(1,5,7,11\). The former is diagonal in sample coordinates; the latter is diagonal in frequency coordinates. Under a Fourier basis change, a sample-residue mask generally produces a different operator, with its own alias structure.
A valid comparison therefore specifies the conjugating matrix and the chosen selector. The fact that both constructions use roots of unity does not identify their packets. QA08 and QA09 supply an explicit rotation and Fourier calculation where a bridge is needed. Neither statement is claimed as a generic theorem in the inherited Lean package used here.