A.2 The typed mathematical target
On this page · Permalink · Source line 30
The complex matrices act on vectors indexed by \(\operatorname{Fin}(12)\). The Fourier convention is
The adjoint \(F^*\) therefore carries the negative exponential sign. The selector \(D\) is diagonal with value one precisely at the residues \(U=\{1,5,7,11\}\). The transported operator is \(P=FDF^*\).
Write
Both vectors have norm one. Their initial probability histograms are identical, but their inner product is zero. The vector \(u\) has entry \(1/2\) on \(U\) and zero elsewhere. Lean proves the actual complex identities \(Fu=\psi\) and \(F^*\psi=u\), as well as transformed coprime probability one for \(\psi\) and zero for \(\chi\).
The statements are finite and exact. No parameterized arbitrary-modulus theorem, general circuit construction, physical phase-removal process, or quantum speedup is included in these formal claims.