Quantum and Circuits

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \hypertarget{q:abstract}{%
2 \section*{Overview}\label{q:abstract}}
3 
4 A finite arithmetic selector can be transported into a rational signal
5 projector and a complex projective measurement by one explicitly
6 normalized Fourier transformation. This chapter gives the full proof chain
7 and follows a single exact twelve-dimensional example through every
8 representation. The arithmetic input is the coprime residue set modulo
9 twelve. Its Fourier synthesis is the integer-valued Ramanujan signal.
10 The associated circulant matrix is an orthogonal projector of rank four.
11 A normalized version of the signal is a quantum state, and an inverse
12 Fourier transformation recovers the arithmetic support. An unsigned
13 state has the same probabilities in the original basis yet zero
14 probability on the selected support after transformation. The two states
15 are orthogonal. A continuous relative-phase family makes that difference
16 visible without changing the initial probability histogram.
17 
18 The general finite Fourier, Möbius, divisor-projector, and polyphase
19 identities are proved in the text. The formal companion covers the
20 concrete modulus-twelve realization, including the sound interpretation
21 of exact rational coordinates in the ordinary complex numbers, both
22 unitarity identities, projector transport, state preparation and
23 recovery, and the phase-sensitive probability conclusions. The formal companion contains ninety-six named theorems across five modules, including the twenty-two original bridge statements. The formal appendix identifies its exact coverage and verification evidence.
24 
25 Ramanujan sums, Fourier orthogonality, rational cyclic projectors, and
26 Ramanujan signal subspaces are classical. The contribution of this
27 presentation is an exact, inspectable realization chain, its
28 theorem-to-code concordance, and its explicit account of the information
29 retained or discarded at each map. It makes no circuit-efficiency or
30 quantum-advantage claim.
31 
32 \hypertarget{q:the-mathematical-object-being-transported}{%
33 \section{The mathematical object being
34 transported}\label{q:the-mathematical-object-being-transported}}
35 
36 The word \emph{bridge} is useful only when its arrows have definitions.
37 In the present example the common object is a selector: a diagonal
38 operator that retains certain Fourier coordinates and discards the
39 others. Arithmetic supplies the selected labels. Fourier synthesis
40 expresses that selector in sample coordinates. Complex normalization
41 then supplies a unitary transformation and the state vectors used in a
42 quantum interpretation.
43 
44 The basic identity is
45 
46 \[
47 P=FDF^\dagger.
48 \]
49 
50 Here \(D\) is a diagonal zero-or-one matrix, \(F\) is unitary, and
51 \(\dagger\) denotes conjugate transpose. Consequently \(P\) is an
52 orthogonal projector. The transformation \(F\) is reversible. The
53 selection \(P\) need not be. A complete decomposition consists of both
54 \(Px\) and \((I-P)x\), whose sum recovers \(x\).
55 
56 This distinction determines what can be transported. A Fourier basis
57 change preserves dimension, inner products, norms, and the entire
58 vector. A projector preserves only its selected component. Measurement
59 probabilities discard still more information. The same exact operator
60 can appear in arithmetic, signal processing, and finite-dimensional
61 quantum theory, while those uses retain different observables and have
62 different implementation costs.
63 
64 We work over \(\mathbb C\) for Fourier transformations and use
65 \(\mathbb Q\) for the rational kernels. All index sets in the main
66 finite construction are specified, and no limit argument is needed. A
67 packet in this chapter means a component together with its stated
68 realization map. This definition does not turn every kind of component
69 into the same object. Character-order packets and coefficient-residue
70 lanes will be distinguished explicitly in the polyphase section.
71 
72 \hypertarget{q:claim-labels-and-evidence-classes}{%
73 \subsection{Claim labels and evidence
74 classes}\label{q:claim-labels-and-evidence-classes}}
75 
76 The labels QA01 through QA20 refer to mathematical statements in this
77 paper. They are not a count of Lean declarations. A single claim can use
78 several formal lemmas, and a general theorem can have a formally checked
79 specialization rather than a generic Lean proof.
80 
81 We use three evidence descriptions. A \emph{general prose theorem} has a
82 proof below for all inputs satisfying its hypotheses. A \emph{formal
83 specialization} is an actual declaration in the preserved modulus-twelve
84 source. A \emph{finite computational check} is a bounded verification of
85 an implementation. These descriptions can support the same identity, but
86 they are not interchangeable. The Lean guide gives the exact declaration
87 mapping.
88 
89 The central example uses the vectors
90 
91 \[
92 \begin{aligned}
93 c&=(4,0,2,0,-2,0,-4,0,-2,0,2,0),\\
94 b&=(5,2,-1,2,5,2,-1,2,5,2,-1,2),\\
95 x&=(9,2,1,2,3,2,-5,2,3,2,1,2).
96 \end{aligned}
97 \]
98 
99 These are the literal coefficients of the formal source, and \(x=c+b\).
100 Keeping one example fixed makes every arrow independently checkable.
101 
102 \hypertarget{q:fourier-conventions-and-the-finite-proof-chain}{%
103 \section{Fourier conventions and the finite proof
104 chain}\label{q:fourier-conventions-and-the-finite-proof-chain}}
105 
106 Let \(q\) be a positive integer. Write \(I_q=\{0,1,\ldots,q-1\}\),
107 interpreting indices modulo \(q\), and put
108 
109 \[
110 \zeta_q=e^{2\pi i/q}.
111 \]
112 
113 A signal is a vector \(x:I_q\to\mathbb C\). We write \(\operatorname{Id}_q\) for the identity matrix of dimension \(q\), and \(I\) for an identity matrix when its dimension is clear. Our inner product is
114 conjugate-linear in the first argument:
115 
116 \[
117 \langle x,y\rangle=\sum_{n=0}^{q-1}\overline{x(n)}y(n),
118 \qquad \|x\|^2=\langle x,x\rangle.
119 \]
120 
121 The unscaled negative-sign discrete Fourier transform is
122 
123 \[
124 \widehat{x}(k)=\sum_{n=0}^{q-1}x(n)\zeta_q^{-kn}.
125 \]
126 
127 The positive-sign normalized Fourier matrix is
128 
129 \[
130 (F_q)_{na}=q^{-1/2}\zeta_q^{na}.
131 \]
132 
133 Thus \(F_q\) synthesizes a signal from normalized frequency coordinates,
134 while \(F_q^\dagger x=\widehat{x}/\sqrt q\) analyzes it. This convention
135 explains all signs and all square-root factors below. The negative-sign
136 transform and the positive-sign synthesis are adjoints of one another.
137 
138 \hypertarget{q:theorem-qa01.-the-order-of-a-finite-phase}{%
139 \subsection*{Theorem QA01. The order of a finite
140 phase}\label{q:theorem-qa01.-the-order-of-a-finite-phase}}
141 
142 For \(a\in I_q\), the multiplicative order of \(\zeta_q^a\) is
143 
144 \[
145 \frac q{\gcd(a,q)}.
146 \]
147 
148 \textbf{Proof.} The equation \((\zeta_q^a)^t=1\) holds exactly when
149 \(q\) divides \(at\). Write \(g=\gcd(a,q)\), \(q=gq'\), and \(a=ga'\),
150 with \(\gcd(a',q')=1\). The divisibility condition is \(q'\mid a't\),
151 which is equivalent to \(q'\mid t\). Its smallest positive solution is
152 \(t=q'\). This includes \(a=0\): then \(g=q\) and the order is one.
153 \(\square\)
154 
155 \hypertarget{q:theorem-qa02.-character-orthogonality}{%
156 \subsection*{Theorem QA02. Character
157 orthogonality}\label{q:theorem-qa02.-character-orthogonality}}
158 
159 For any integer \(h\),
160 
161 \[
162 \sum_{n=0}^{q-1}\zeta_q^{hn}
163 =\begin{cases}q,&q\mid h,\\0,&q\nmid h.\end{cases}
164 \]
165 
166 \textbf{Proof.} If \(q\mid h\), every summand is one. Otherwise
167 \(r=\zeta_q^h\ne1\) and \(r^q=1\). Multiplying the sum by \(1-r\) gives
168 \(1-r^q=0\), so the sum is zero. This argument also covers \(q=1\),
169 where only the first case occurs. \(\square\)
170 
171 \hypertarget{q:theorem-qa03.-unitarity-inversion-and-parseval}{%
172 \subsection*{Theorem QA03. Unitarity, inversion, and
173 Parseval}\label{q:theorem-qa03.-unitarity-inversion-and-parseval}}
174 
175 For every positive \(q\),
176 
177 \[
178 F_q^\dagger F_q=\operatorname{Id}_q,
179 \qquad F_qF_q^\dagger=\operatorname{Id}_q.
180 \]
181 
182 Consequently,
183 
184 \[
185 x(n)=\frac1q\sum_{k=0}^{q-1}\widehat{x}(k)\zeta_q^{kn},
186 \qquad
187 \sum_n|x(n)|^2=\frac1q\sum_k|\widehat{x}(k)|^2.
188 \]
189 
190 \textbf{Proof.} The \((a,b)\) entry of the first matrix product is
191 
192 \[
193 \frac1q\sum_{n=0}^{q-1}\zeta_q^{n(b-a)}.
194 \]
195 
196 By QA02 it is one when \(a=b\) and zero otherwise. The \((n,m)\) entry
197 of the second product is the same orthogonality sum with indices
198 interchanged. Since \(F_q^\dagger x=\widehat{x}/\sqrt q\), the identity
199 \(F_qF_q^\dagger x=x\) is the displayed inverse formula. Finally, a
200 unitary matrix preserves inner products:
201 
202 \[
203 \|F_q^\dagger x\|^2
204 =x^\dagger F_qF_q^\dagger x
205 =x^\dagger x.
206 \]
207 
208 Replacing \(F_q^\dagger x\) by \(\widehat{x}/\sqrt q\) proves Parseval.
209 \(\square\)
210 
211 These proofs use finite sums, ordinary complex multiplication, and the
212 positive real square root of \(q\). No asymptotic approximation enters.
213 At \(q=1\) the Fourier matrix is the one-by-one identity, and all
214 identities have their literal scalar meanings.
215 
216 \hypertarget{q:coprimality-becomes-an-integer-signal}{%
217 \section{Coprimality becomes an integer
218 signal}\label{q:coprimality-becomes-an-integer-signal}}
219 
220 Let
221 
222 \[
223 U_q=\{a\in I_q:\gcd(a,q)=1\},
224 \qquad \varphi(q)=|U_q|.
225 \]
226 
227 The Ramanujan sum is
228 
229 \[
230 c_q(n)=\sum_{a\in U_q}\zeta_q^{an},
231 \qquad n\in\mathbb Z.
232 \]
233 
234 It adds the primitive \(q\)th-root phases selected by QA01. Its
235 definition is complex, but its value is an integer. That integrality is
236 the step that makes the sample-coordinate projector rational. Ramanujan
237 sums and their divisor formulas are classical arithmetic constructions
238 \cite{q:Ramanujan1918}.
239 
240 \hypertarget{q:theorem-qa04.-muxf6bius-formula-and-integrality}{%
241 \subsection*{Theorem QA04. Möbius formula and
242 integrality}\label{q:theorem-qa04.-muxf6bius-formula-and-integrality}}
243 
244 Let \(\mu\) be the Möbius function, with \(\mu(1)=1\). For every
245 positive \(q\) and every integer \(n\),
246 
247 \[
248 \boxed{c_q(n)=\sum_{d\mid\gcd(q,n)}d\,\mu(q/d)\in\mathbb Z.}
249 \]
250 
251 In particular \(c_q\) has period \(q\), is real-valued, satisfies
252 \(c_q(-n)=c_q(n)\), and has \(c_q(0)=\varphi(q)\).
253 
254 \textbf{Proof.} For a positive integer \(g\),
255 
256 \[
257 \sum_{d\mid g}\mu(d)
258 =\begin{cases}1,&g=1,\\0,&g>1.\end{cases}
259 \]
260 
261 To see this, only squarefree divisors contribute. If \(g\) has \(r\)
262 distinct prime factors, the sum is \((1-1)^r\), with value one when
263 \(r=0\). Therefore
264 
265 \[
266 \mathbf1_{\gcd(a,q)=1}=\sum_{d\mid\gcd(a,q)}\mu(d).
267 \]
268 
269 Substitute this into the phase sum over all \(a\in I_q\), exchange the
270 finite sums, and write \(a=db\) in the terms where \(d\mid a\):
271 
272 \[
273 \begin{aligned}
274 c_q(n)
275 &=\sum_{d\mid q}\mu(d)
276   \sum_{b=0}^{q/d-1}e^{2\pi ibn/(q/d)}\\
277 &=\sum_{\substack{d\mid q\\(q/d)\mid n}}\mu(d)\frac qd.
278 \end{aligned}
279 \]
280 
281 The second equality is QA02. Replacing \(q/d\) by \(e\) gives the
282 displayed divisor sum. It is an integer. Periodicity follows already
283 from the phase definition. The divisor formula is unchanged by
284 \(n\mapsto -n\), so \(c_q(-n)=c_q(n)\). At \(n=0\), every selected phase
285 is one, giving \(c_q(0)=|U_q|\). \(\square\)
286 
287 At \(q=1\), \(U_1=\{0\}\) because \(\gcd(0,1)=1\). The phase sum and the
288 divisor formula both give \(c_1(n)=1\). This boundary case is included
289 in the proofs even though the inherited arithmetic regression range
290 begins at modulus two.
291 
292 \hypertarget{q:theorem-qa05.-exact-spectral-support-and-energy}{%
293 \subsection*{Theorem QA05. Exact spectral support and
294 energy}\label{q:theorem-qa05.-exact-spectral-support-and-energy}}
295 
296 Over one period,
297 
298 \[
299 \boxed{\widehat{c_q}(k)=q\,\mathbf1_{k\in U_q},\qquad k\in I_q.}
300 \]
301 
302 Moreover,
303 
304 \[
305 \sum_{n=0}^{q-1}|c_q(n)|^2=q\varphi(q).
306 \]
307 
308 \textbf{Proof.} Substitute the phase definition and exchange two finite
309 sums:
310 
311 \[
312 \widehat{c_q}(k)
313 =\sum_{a\in U_q}\sum_{n=0}^{q-1}\zeta_q^{(a-k)n}.
314 \]
315 
316 QA02 makes the inner sum \(q\) exactly when \(a=k\), and zero otherwise.
317 The energy identity follows from QA03:
318 
319 \[
320 \|c_q\|^2
321 =\frac1q\sum_k|\widehat{c_q}(k)|^2
322 =\frac1q\varphi(q)q^2.
323 \] \(\square\)
324 
325 The selector has been recovered by an identity. A numerical spectrum can
326 illustrate the result, but neither a tolerance nor a peak-finding rule
327 defines the arithmetic support.
328 
329 \hypertarget{q:rational-character-order-projectors}{%
330 \section{Rational character-order
331 projectors}\label{q:rational-character-order-projectors}}
332 
333 It is helpful to distinguish the size of an ambient signal from the
334 order of a character. Fix a positive ambient length \(N\). For each
335 divisor \(d\) of \(N\), define
336 
337 \[
338 S_d=\{a\in I_N:N/\gcd(a,N)=d\}.
339 \]
340 
341 The set \(S_d\) contains the labels of characters of exact order \(d\).
342 Put \(D_d=\operatorname{diag}(\mathbf1_{a\in S_d})\) and
343 
344 \[
345 P_d^{(N)}=F_ND_dF_N^\dagger.
346 \]
347 
348 The superscript records the ambient dimension. In particular, the kernel
349 normalization below is \(1/N\), even when \(d<N\).
350 
351 \hypertarget{q:theorem-qa06.-rational-kernels-and-complete-divisor-decomposition}{%
352 \subsection*{Theorem QA06. Rational kernels and complete divisor
353 decomposition}\label{q:theorem-qa06.-rational-kernels-and-complete-divisor-decomposition}}
354 
355 For every \(d\mid N\),
356 
357 \[
358 \boxed{(P_d^{(N)})_{nm}=\frac1N c_d(n-m).}
359 \]
360 
361 The matrices have rational entries and satisfy
362 
363 \[
364 \begin{aligned}
365 (P_d^{(N)})^\dagger&=P_d^{(N)},\\
366 P_d^{(N)}P_e^{(N)}&=\delta_{de}P_d^{(N)},\\
367 \sum_{d\mid N}P_d^{(N)}&=\operatorname{Id}_N,\\
368 \operatorname{rank}P_d^{(N)}&=\operatorname{tr}P_d^{(N)}=\varphi(d).
369 \end{aligned}
370 \]
371 
372 \textbf{Proof.} A label in \(S_d\) has the unique form \(a=(N/d)b\),
373 where \(0\le b<d\) and \(\gcd(b,d)=1\). Indeed,
374 
375 \[
376 \gcd((N/d)b,N)=(N/d)\gcd(b,d).
377 \]
378 
379 Direct multiplication therefore gives
380 
381 \[
382 \begin{aligned}
383 (F_ND_dF_N^\dagger)_{nm}
384 &=\frac1N\sum_{a\in S_d}\zeta_N^{a(n-m)}\\
385 &=\frac1N\sum_{b\in U_d}\zeta_d^{b(n-m)}
386 =\frac1N c_d(n-m).
387 \end{aligned}
388 \]
389 
390 QA04 proves rationality. Each \(D_d\) is a self-adjoint diagonal
391 projector. The sets \(S_d\) partition \(I_N\), because every character
392 has exactly one order dividing \(N\). Hence \(D_dD_e=\delta_{de}D_d\)
393 and \(\sum_{d\mid N}D_d=\operatorname{Id}_N\). Conjugating these identities by the
394 unitary \(F_N\) proves the projector identities. The rank is unchanged
395 under multiplication by invertible matrices, so it equals the number of
396 selected diagonal entries, \(|S_d|=\varphi(d)\). The diagonal kernel
397 entries are all \(c_d(0)/N=\varphi(d)/N\), whose sum is \(\varphi(d)\).
398 \(\square\)
399 
400 This orthogonal divisor-shell decomposition has established antecedents
401 in Ramanujan subspaces and filter banks \cite{q:Vaidyanathan2014FIR,q:Vaidyanathan2014I,q:Vaidyanathan2014II}. The general theorem above is
402 proved independently in this text. The formal companion certifies the
403 concrete \(N=d=12\) projector and its transport identity, rather than an
404 arbitrary-divisor Lean theorem.
405 
406 \hypertarget{q:a-shift-operator-realization-and-its-sign}{%
407 \subsection{A shift-operator realization and its
408 sign}\label{q:a-shift-operator-realization-and-its-sign}}
409 
410 Let \(A\) be the cyclic shift \((Ax)(n)=x(n-1)\). A Fourier column
411 \(f_a(n)=N^{-1/2}\zeta_N^{na}\) satisfies \(Af_a=\zeta_N^{-a}f_a\).
412 Therefore
413 
414 \[
415 E_a=\frac1N\sum_{\ell=0}^{N-1}\zeta_N^{a\ell}A^\ell
416 \]
417 
418 acts as the identity on \(f_a\) and as zero on every other column, by
419 QA02. Summing \(E_a\) over \(S_d\) gives
420 
421 \[
422 P_d^{(N)}=\frac1N\sum_{\ell=0}^{N-1}c_d(\ell)A^\ell.
423 \]
424 
425 This formula also follows entrywise because \((A^\ell)_{nm}\) is one
426 exactly when \(n-m=\ell\) modulo \(N\). A group-algebra convention with
427 the opposite shift sign writes individual idempotents with the opposite
428 phase sign. The divisor shells are unchanged under \(a\mapsto -a\), and
429 \(c_d(-\ell)=c_d(\ell)\), so the rational shell formula remains the
430 same.
431 
432 Proposition 21.11 of \emph{Stratified Universality for Resolved
433 Representations}, gives the rational cyclic order-projector
434 formula in the group algebra. Boundary 21.12 distinguishes it from
435 formal-series coefficient-residue selection \cite{q:KomorebiStratified16}.
436 The present shift calculation makes the representation and the sign
437 explicit.
438 
439 \hypertarget{q:unions-of-order-classes}{%
440 \subsection{Unions of order
441 classes}\label{q:unions-of-order-classes}}
442 
443 If \(\mathcal D\) is any set of divisors of \(N\), then
444 
445 \[
446 P_{\mathcal D}=\sum_{d\in\mathcal D}P_d^{(N)}
447 \]
448 
449 is a rational orthogonal projector of rank
450 \(\sum_{d\in\mathcal D}\varphi(d)\). Its complement is the sum over the
451 remaining divisors. Individual split Fourier projectors can have
452 nonrational entries. Summing complete order classes is a sufficient
453 mechanism for rationality. No converse classification of every rational
454 selector is needed for the present bridge.
455 
456 \hypertarget{q:selection-residuals-and-information-loss}{%
457 \section{Selection, residuals, and information
458 loss}\label{q:selection-residuals-and-information-loss}}
459 
460 For any set \(S\subseteq I_N\), let \(D_S\) be its diagonal indicator
461 and \(P_S=F_ND_SF_N^\dagger\). This construction does not require \(S\)
462 to be an order class. Rationality is special, but orthogonal projection
463 is general.
464 
465 \hypertarget{q:theorem-qa07.-projector-geometry-and-exact-residual-reconstruction}{%
466 \subsection*{Theorem QA07. Projector geometry and exact residual
467 reconstruction}\label{q:theorem-qa07.-projector-geometry-and-exact-residual-reconstruction}}
468 
469 For every \(x\in\mathbb C^N\),
470 
471 \[
472 \begin{aligned}
473 x&=P_Sx+(I-P_S)x,\\
474 \langle P_Sx,(I-P_S)x\rangle&=0,\\
475 \|x\|^2&=\|P_Sx\|^2+\|(I-P_S)x\|^2.
476 \end{aligned}
477 \]
478 
479 Furthermore, \(P_S\) is injective exactly when \(S=I_N\). If \(S\) is
480 proper, its kernel has dimension \(N-|S|\).
481 
482 \textbf{Proof.} The first equality is distributivity. Since
483 \(P_S^\dagger=P_S\) and \(P_S^2=P_S\),
484 
485 \[
486 \langle P_Sx,(I-P_S)x\rangle
487 =x^\dagger P_S(I-P_S)x=0.
488 \]
489 
490 Expanding the norm square of the orthogonal sum proves the energy
491 identity. In Fourier coordinates, \(P_S\) is \(D_S\), whose kernel
492 consists exactly of the vectors supported outside \(S\). Its dimension
493 is \(N-|S|\). This kernel is zero exactly when every label is selected.
494 \(\square\)
495 
496 This gives a precise reconstruction contract. The pair of packets
497 \((P_Sx,(I-P_S)x)\) retains the complete vector, subject to the
498 compatibility condition that the first lies in the range and the second
499 in the kernel. Keeping only the first packet is an exact projection but
500 an incomplete representation of an arbitrary input.
501 
502 For character-order packets, QA06 gives the stronger complete
503 decomposition
504 
505 \[
506 x=\sum_{d\mid N}P_d^{(N)}x,
507 \qquad
508 \|x\|^2=\sum_{d\mid N}\|P_d^{(N)}x\|^2.
509 \]
510 
511 The decomposition is a change in organization rather than a reduction in
512 the dimension of the whole signal. Smaller stored selectors do not make
513 an arbitrary signal contain less information. Compression requires a
514 restriction on the admissible signals or an explicit approximation
515 criterion.
516 
517 \hypertarget{q:coefficient-residue-lanes-and-polyphase-transport}{%
518 \section{Coefficient-residue lanes and polyphase
519 transport}\label{q:coefficient-residue-lanes-and-polyphase-transport}}
520 
521 There is a second exact decomposition that is common in Komorebi
522 calculations and in signal processing. It separates \emph{positions} by
523 residue class rather than separating \emph{Fourier characters} by order.
524 Both decompositions use projectors, but they select different objects.
525 
526 \hypertarget{q:formal-coefficient-lanes}{%
527 \subsection{Formal coefficient
528 lanes}\label{q:formal-coefficient-lanes}}
529 
530 Let \(L\ge1\) and let \(f(z)=\sum_{n\ge0}a_nz^n\) be a formal power
531 series over a field containing a primitive \(L\)th root \(\omega\) and
532 \(1/L\). For \(0\le r<L\), define
533 
534 \[
535 E_rf(t)=\sum_{m\ge0}a_{r+Lm}t^m,
536 \qquad
537 R_rf(z)=z^rE_rf(z^L).
538 \]
539 
540 The first expression addresses the lane in a new variable. The second
541 places that lane back at its original coefficient positions.
542 
543 \Needspace{13\baselineskip}
544 \hypertarget{q:theorem-qa08.-exact-coefficient-residue-decomposition}{%
545 \subsection*{Theorem QA08. Exact coefficient-residue
546 decomposition}\label{q:theorem-qa08.-exact-coefficient-residue-decomposition}}
547 
548 The coefficient-residue maps satisfy
549 
550 \[
551 \begin{aligned}
552 R_rf(z)&=\frac1L\sum_{j=0}^{L-1}\omega^{-rj}f(\omega^jz),\\
553 R_rR_s&=\delta_{rs}R_r,\\
554 \sum_{r=0}^{L-1}R_rf&=f.
555 \end{aligned}
556 \]
557 
558 \textbf{Proof.} The coefficient of \(z^n\) in the first right-hand side
559 is
560 
561 \[
562 \frac{a_n}{L}\sum_{j=0}^{L-1}\omega^{j(n-r)}.
563 \]
564 
565 Character orthogonality makes it \(a_n\) when \(n\equiv r\pmod L\) and
566 zero otherwise. This is precisely the coefficient of \(R_rf\). Each
567 coefficient position belongs to a unique lane, so the projector and
568 completeness identities follow coefficientwise. The equality is formal,
569 with no analytic convergence hypothesis. \(\square\)
570 
571 For an infinite analytic series, the same identity holds wherever all
572 displayed evaluations are defined, but the formal theorem does not need
573 that interpretation. The lane index is an exponent residue. It is not a
574 multiplicative-order class of a Fourier character.
575 
576 \hypertarget{q:finite-polyphase-lanes}{%
577 \subsection{Finite polyphase lanes}\label{q:finite-polyphase-lanes}}
578 
579 Now suppose \(N=LM\) with positive integers \(L\) and \(M\). For a
580 vector \(x\in\mathbb C^N\), define its \(L\) lanes by
581 
582 \[
583 x_r(m)=x(r+Lm),
584 \qquad 0\le r<L,\quad 0\le m<M.
585 \]
586 
587 The addressing map \(T:x\mapsto(x_0,\ldots,x_{L-1})\) is bijective.
588 Interleaving the lanes reconstructs \(x\), and
589 
590 \[
591 \sum_{n=0}^{N-1}|x(n)|^2
592 =\sum_{r=0}^{L-1}\sum_{m=0}^{M-1}|x_r(m)|^2.
593 \]
594 
595 This energy identity is an exact reindexing. It is useful to preserve it
596 separately from the spectral aliasing identity that follows.
597 
598 \Needspace{19\baselineskip}
599 \hypertarget{q:theorem-qa09.-polyphase-fourier-identities-and-decimation-aliasing}{%
600 \subsection*{Theorem QA09. Polyphase Fourier identities and decimation
601 aliasing}\label{q:theorem-qa09.-polyphase-fourier-identities-and-decimation-aliasing}}
602 
603 Write \(\widehat{x_r}\) for the unscaled \(M\)-point transform of lane
604 \(r\). Then for \(k\in I_N\),
605 
606 \[
607 \boxed{\widehat{x}(k)
608 =\sum_{r=0}^{L-1}\zeta_N^{-kr}\widehat{x_r}(k\bmod M).}
609 \]
610 
611 Conversely, for \(\ell\in I_M\),
612 
613 \[
614 \boxed{\widehat{x_r}(\ell)
615 =\frac1L\sum_{j=0}^{L-1}
616 \zeta_N^{r(\ell+jM)}\widehat{x}(\ell+jM).}
617 \]
618 
619 \textbf{Proof.} Partition the \(N\) samples by their unique
620 representation \(n=r+Lm\):
621 
622 \[
623 \begin{aligned}
624 \widehat{x}(k)
625 &=\sum_{r=0}^{L-1}\sum_{m=0}^{M-1}
626 x_r(m)\zeta_N^{-k(r+Lm)}\\
627 &=\sum_r\zeta_N^{-kr}\sum_mx_r(m)\zeta_M^{-km}.
628 \end{aligned}
629 \]
630 
631 The inner sum is \(\widehat{x_r}(k\bmod M)\), proving the first
632 identity. For the second, insert Fourier inversion into the lane
633 transform:
634 
635 \[
636 \begin{aligned}
637 \widehat{x_r}(\ell)
638 &=\sum_{m=0}^{M-1}x(r+Lm)\zeta_M^{-\ell m}\\
639 &=\frac1N\sum_{k=0}^{N-1}\widehat{x}(k)\zeta_N^{kr}
640 \sum_{m=0}^{M-1}\zeta_M^{(k-\ell)m}.
641 \end{aligned}
642 \]
643 
644 QA02 makes the inner sum \(M\) exactly when \(k=\ell+jM\) for some
645 \(0\le j<L\). Since \(M/N=1/L\), this is the second displayed identity.
646 \(\square\)
647 
648 Every lane transform combines an alias class of \(L\) full-spectrum
649 coefficients. One decimated lane generally cannot distinguish those
650 coefficients. All \(L\) offsets together retain the original signal. For
651 a fixed alias class \(\ell\), the equations across \(r\) are an
652 invertible Fourier mixing system after the nonzero phases
653 \(\zeta_N^{r\ell}\) are removed. The apparent collapse is resolved by
654 preserving the complete collection of offsets.
655 
656 \hypertarget{q:why-the-two-projectors-must-not-be-conflated}{%
657 \subsection{Why the two projectors must not be
658 conflated}\label{q:why-the-two-projectors-must-not-be-conflated}}
659 
660 A coefficient-residue selector keeps samples such as
661 \(x(0),x(3),x(6),x(9)\). A character-order projector keeps spectral
662 modes such as \(1,5,7,11\). The former is diagonal in sample
663 coordinates; the latter is diagonal in frequency coordinates. Under a
664 Fourier basis change, a sample-residue mask generally produces a
665 different operator, with its own alias structure.
666 
667 A valid comparison therefore specifies the conjugating matrix and the
668 chosen selector. The fact that both constructions use roots of unity
669 does not identify their packets. QA08 and QA09 supply an explicit
670 rotation and Fourier calculation where a bridge is needed. Neither
671 statement is claimed as a generic theorem in the inherited Lean package
672 used here.
673 
674 \hypertarget{q:the-exact-modulus-twelve-arithmetic-calculation}{%
675 \section{The exact modulus-twelve arithmetic
676 calculation}\label{q:the-exact-modulus-twelve-arithmetic-calculation}}
677 
678 We now fix \(q=12\). The coprime labels are
679 
680 \[
681 U_{12}=\{1,5,7,11\},
682 \qquad \varphi(12)=4,
683 \qquad \zeta=e^{\pi i/6}=\frac{\sqrt3}{2}+\frac i2.
684 \]
685 
686 The signal is
687 
688 \[
689 c(n)=\zeta^n+\zeta^{5n}+\zeta^{7n}+\zeta^{11n}
690 =2\cos(\pi n/6)+2\cos(5\pi n/6).
691 \]
692 
693 The cosine formula comes from conjugate pairs. It exposes interference,
694 while the integer divisor formula provides an independent arithmetic
695 route to each value.
696 
697 \hypertarget{q:theorem-qa10.-the-exact-phase-and-transform-tables}{%
698 \subsection*{Theorem QA10. The exact phase and transform
699 tables}\label{q:theorem-qa10.-the-exact-phase-and-transform-tables}}
700 
701 Over one period,
702 
703 \[
704 c=(4,0,2,0,-2,0,-4,0,-2,0,2,0),
705 \]
706 
707 and
708 
709 \[
710 \widehat c=(0,12,0,0,0,12,0,12,0,0,0,12).
711 \]
712 
713 \textbf{Proof.} For \(q=12\), QA04 becomes
714 
715 \[
716 c(n)=2\mathbf1_{2\mid n}-4\mathbf1_{4\mid n}
717 -6\mathbf1_{6\mid n}+12\mathbf1_{12\mid n}.
718 \]
719 
720 Indeed, the only divisors \(d\) of twelve for which \(\mu(12/d)\ne0\)
721 are \(2,4,6,12\), with coefficients \(2,-4,-6,12\). Evaluating the
722 divisibility indicators at \(0,\ldots,11\) gives the sample table. QA05
723 gives value twelve at the four coprime labels and zero elsewhere.
724 \(\square\)
725 
726 At sample zero, all four phases agree and the value is four. At sample
727 one, they cancel. At sample six, all four are minus one and the value is
728 minus four. Those signs are the relative phase information that will
729 later distinguish two states with the same initial probabilities.
730 
731 \hypertarget{q:a-compact-projector-matrix}{%
732 \subsection{A compact projector
733 matrix}\label{q:a-compact-projector-matrix}}
734 
735 Put \(P=P_{12}^{(12)}\). Its entries are
736 
737 \[
738 P_{nm}=\frac{c(n-m)}{12}.
739 \]
740 
741 Equivalently, its first row is
742 
743 \[
744 \left(\frac13,0,\frac16,0,-\frac16,0,-\frac13,0,-\frac16,0,\frac16,0\right),
745 \]
746 
747 and each subsequent row is the cyclic right shift of the preceding row.
748 This specifies every entry of the twelve-by-twelve rational matrix. It
749 agrees exactly with the literal matrix in the original formal module and
750 with the indexed matrix in the later transport module.
751 
752 With \(D=\operatorname{diag}(\mathbf1_{a\in U_{12}})\) and \(F=F_{12}\),
753 
754 \[
755 P=FDF^\dagger,
756 \qquad P^2=P,
757 \qquad P^\dagger=P,
758 \qquad \operatorname{rank}P=\operatorname{tr}P=4.
759 \]
760 
761 The six divisor shells of length twelve have orders \(1,2,3,4,6,12\) and
762 ranks \(1,1,2,2,2,4\). Their ranks add to twelve, and their orthogonal
763 sum is the identity by QA06.
764 
765 \hypertarget{q:the-finite-lanes-of-the-same-signal}{%
766 \subsection{The finite lanes of the same
767 signal}\label{q:the-finite-lanes-of-the-same-signal}}
768 
769 For \(L=3\) and \(M=4\), the coefficient-residue lanes are
770 
771 \[
772 \begin{aligned}
773 c_0&=(4,0,-4,0),\\
774 c_1&=(0,-2,0,2),\\
775 c_2&=(2,0,-2,0).
776 \end{aligned}
777 \]
778 
779 Their four-point Fourier transforms are
780 
781 \[
782 \widehat c_0=(0,8,0,8),
783 \quad \widehat c_1=(0,4i,0,-4i),
784 \quad \widehat c_2=(0,4,0,4).
785 \]
786 
787 For example, a full coefficient at \(k=1\) is reconstructed as
788 
789 \[
790 \widehat c(1)=8+4i\zeta^{-1}+4\zeta^{-2}=12.
791 \]
792 
793 At \(k=9\), the same lane-frequency index \(1\) gives
794 
795 \[
796 \widehat c(9)=8+4i\zeta^{-9}+4\zeta^{-18}=8-4-4=0.
797 \]
798 
799 The offsets distinguish two full Fourier labels with the same reduced
800 frequency. These equations demonstrate the role of the phases in QA09.
801 They do not identify a lane with a character-order shell.
802 
803 \hypertarget{q:filtering-a-signal-with-something-to-remove}{%
804 \section{Filtering a signal with something to
805 remove}\label{q:filtering-a-signal-with-something-to-remove}}
806 
807 Take the off-band perturbation
808 
809 \[
810 b(n)=3\cos(\pi n/2)+2.
811 \]
812 
813 The constant occupies frequency zero, and the cosine occupies labels
814 three and nine. These labels all lie outside \(U_{12}\). The
815 perturbation has the literal rational vector
816 
817 \[
818 b=(5,2,-1,2,5,2,-1,2,5,2,-1,2).
819 \]
820 
821 Set \(x=c+b\), giving
822 
823 \[
824 x=(9,2,1,2,3,2,-5,2,3,2,1,2).
825 \]
826 
827 \Needspace{13\baselineskip}
828 \hypertarget{q:theorem-qa11.-exact-filter-recovery-and-orthogonal-energy}{%
829 \subsection*{Theorem QA11. Exact filter recovery and orthogonal
830 energy}\label{q:theorem-qa11.-exact-filter-recovery-and-orthogonal-energy}}
831 
832 The test signal satisfies
833 
834 \[
835 Pc=c,
836 \qquad Pb=0,
837 \qquad Px=c,
838 \qquad (I-P)x=b,
839 \]
840 
841 and
842 
843 \[
844 \langle c,b\rangle=0,
845 \qquad \|c\|^2=48,
846 \qquad \|b\|^2=102,
847 \qquad \|x\|^2=150=48+102.
848 \]
849 
850 \textbf{Proof.} QA05 gives the support of \(\widehat c\). Write the
851 cosine as
852 
853 \[
854 3\cos(\pi n/2)=\frac32(\zeta^{3n}+\zeta^{9n}).
855 \]
856 
857 Thus \(\widehat b\) equals twenty-four at zero, eighteen at three and
858 nine, and zero elsewhere. Multiplication by \(D\) fixes the spectrum of
859 \(c\) and kills the spectrum of \(b\), proving the filter identities.
860 Their supports are disjoint, so Parseval for inner products gives
861 \(\langle c,b\rangle=0\). QA05 gives \(\|c\|^2=12\cdot4=48\), and
862 
863 \[
864 \|b\|^2=\frac{24^2+18^2+18^2}{12}=102.
865 \]
866 
867 QA07 then gives \(\|x\|^2=48+102=150\). The same numbers follow by
868 direct rational squaring of the displayed vectors. \(\square\)
869 
870 The discarded component is part of a complete explanation of the input.
871 It is called a perturbation because the example declares \(c\) to be the
872 target. It is a perfectly exact signal component rather than an error
873 introduced by the representation. If the task were to recover all of
874 \(x\), deleting \(b\) would lose valid information.
875 
876 \hypertarget{q:normalized-states-and-literal-unitary-transport}{%
877 \section{Normalized states and literal unitary
878 transport}\label{q:normalized-states-and-literal-unitary-transport}}
879 
880 In a twelve-dimensional complex Hilbert space, let
881 \(|0\rangle,\ldots,|11\rangle\) be an orthonormal basis. Define
882 
883 \[
884 |u\rangle=\frac{|1\rangle+|5\rangle+|7\rangle+|11\rangle}{2}.
885 \]
886 
887 Its squared norm is \(4(1/2)^2=1\). Define the amplitude states
888 
889 \[
890 |\psi\rangle=\frac1{\sqrt{48}}\sum_{n=0}^{11}c(n)|n\rangle,
891 \qquad
892 |\chi\rangle=\frac1{\sqrt{48}}\sum_{n=0}^{11}|c(n)|\,|n\rangle.
893 \]
894 
895 Both have norm one because \(\sum_nc(n)^2=48\). The second state is a
896 separately specified state, constructed from the absolute-value vector.
897 No universal quantum operation implementing the nonlinear rule
898 \(z\mapsto|z|\) is being asserted.
899 
900 \Needspace{16\baselineskip}
901 \hypertarget{q:theorem-qa12.-exact-preparation-and-recovery}{%
902 \subsection*{Theorem QA12. Exact preparation and
903 recovery}\label{q:theorem-qa12.-exact-preparation-and-recovery}}
904 
905 With the positive-sign Fourier matrix defined in Section~\ref{q:fourier-conventions-and-the-finite-proof-chain},
906 
907 \[
908 \boxed{F|u\rangle=|\psi\rangle,
909 \qquad F^\dagger|\psi\rangle=|u\rangle.}
910 \]
911 
912 \textbf{Proof.} At coordinate \(n\), the first left-hand side is
913 
914 \[
915 \frac1{2\sqrt{12}}\sum_{a\in U_{12}}\zeta^{na}
916 =\frac{c(n)}{\sqrt{48}}.
917 \]
918 
919 This is the defining coordinate of \(\psi\). Applying \(F^\dagger\) and
920 using \(F^\dagger F=I\) proves the second equality. \(\square\)
921 
922 The normalization relation is \(\sqrt{48}=2\sqrt{12}\). In the exact
923 coordinate implementation the Fourier scale is \(\sqrt3/6=1/\sqrt{12}\),
924 and the state scale is \(\sqrt3/12=1/\sqrt{48}\). The later formal
925 source proves those scale identities and the exponential entry formula,
926 rather than leaving them as informal interpretations of a rational
927 tuple.
928 
929 This is a mathematical quantum-state construction. An actual realization
930 would additionally require state preparation, a twelve-dimensional
931 unitary implementation, coherence control, and sampling. A
932 twelve-dimensional Fourier matrix is not the ordinary
933 sixteen-dimensional Fourier transformation on four qubits. The unitary
934 direct sum \(F_{12}\oplus I_4\) supplies a mathematical
935 sixteen-dimensional embedding, but it supplies no gate synthesis or
936 resource bound by itself.
937 
938 \hypertarget{q:relative-phase-is-absent-from-one-histogram-and-present-in-another}{%
939 \section{Relative phase is absent from one histogram and present in
940 another}\label{q:relative-phase-is-absent-from-one-histogram-and-present-in-another}}
941 
942 For a normalized state \(|v\rangle=\sum_nv(n)|n\rangle\), the
943 standard-basis probabilities are \(|v(n)|^2\). In the basis analyzed by
944 \(F^\dagger\), the probabilities are \(|(F^\dagger v)(k)|^2\).
945 
946 These describe two measurement procedures on separately prepared copies.
947 Measuring the first histogram on a particular copy does not preserve
948 that copy as a coherent input for the second procedure.
949 
950 \hypertarget{q:theorem-qa13.-equal-initial-probabilities-and-orthogonal-states}{%
951 \subsection*{Theorem QA13. Equal initial probabilities and orthogonal
952 states}\label{q:theorem-qa13.-equal-initial-probabilities-and-orthogonal-states}}
953 
954 The states \(\psi\) and \(\chi\) have identical probabilities in the
955 original basis and are orthogonal:
956 
957 \[
958 |\psi(n)|^2=|\chi(n)|^2\quad\text{for all }n,
959 \qquad \langle\psi,\chi\rangle=0.
960 \]
961 
962 \textbf{Proof.} Squaring a real number or its absolute value gives the
963 same result, proving the first claim. For orthogonality,
964 
965 \[
966 \langle\psi,\chi\rangle
967 =\frac1{48}\sum_{n=0}^{11}c(n)|c(n)|.
968 \]
969 
970 The positive entries contribute \(16+4+4=24\), and the negative entries
971 contribute \(-4-16-4=-24\). Their sum is zero. \(\square\)
972 
973 This is a strong information boundary. The states are distinct even
974 after the physically irrelevant overall phase is disregarded. Orthogonal
975 normalized states cannot be scalar multiples of one another. Yet their
976 original-basis probability histograms are identical.
977 
978 \Needspace{18\baselineskip}
979 \hypertarget{q:theorem-qa14.-complete-arithmetic-phase-separation}{%
980 \subsection*{Theorem QA14. Complete arithmetic phase
981 separation}\label{q:theorem-qa14.-complete-arithmetic-phase-separation}}
982 
983 After applying \(F^\dagger\),
984 
985 \[
986 \Pr_{F^\dagger\psi}(k\in U_{12})=1,
987 \qquad
988 \Pr_{F^\dagger\chi}(k\in U_{12})=0.
989 \]
990 
991 More explicitly,
992 
993 \[
994 (F^\dagger\psi)(k)
995 =\begin{cases}1/2,&k\in\{1,5,7,11\},\\0,&\text{otherwise},\end{cases}
996 \]
997 
998 whereas
999 
1000 \[
1001 (F^\dagger\chi)(k)
1002 =\begin{cases}
1003 2/3,&k\in\{0,6\},\\
1004 1/6,&k\in\{2,4,8,10\},\\
1005 0,&\text{otherwise}.
1006 \end{cases}
1007 \]
1008 
1009 \textbf{Proof.} QA12 gives the first amplitude table. For the second,
1010 set \(a(n)=|c(n)|\). Its vector is
1011 
1012 \[
1013 a=(4,0,2,0,2,0,4,0,2,0,2,0).
1014 \]
1015 
1016 It has period six. Pairing \(n\) and \(n+6\) in its twelve-point
1017 transform produces a factor \(1+(-1)^k\), so every odd transform
1018 coefficient vanishes. For \(k=2\ell\), its transform is twice the
1019 six-point transform of \((4,0,2,0,2,0)\). The doubled transform is
1020 sixteen when \(\ell\) is divisible by three and four otherwise, as one
1021 sees from
1022 
1023 \[
1024 2\left(4+2e^{-2\pi i\ell/3}+2e^{-4\pi i\ell/3}\right).
1025 \]
1026 
1027 When \(\ell\equiv0\pmod3\), the bracket is eight. Otherwise the two
1028 cubic phases sum to minus one and the bracket is two. Thus
1029 
1030 \[
1031 \widehat a=(16,0,4,0,4,0,16,0,4,0,4,0).
1032 \]
1033 
1034 State normalization and the unitary inverse transform divide this table
1035 by \(\sqrt{48}\sqrt{12}=24\), producing the second amplitude table. Its
1036 support is even, while every label in \(U_{12}\) is odd. The selected
1037 probability is therefore zero. The signed state has four probabilities
1038 of \(1/4\), with total one. \(\square\)
1039 
1040 \Needspace{18\baselineskip}
1041 The full probability comparison is:
1042 
1043 {\small\begin{longtable}[]{@{}
1044   >{\centering\arraybackslash}p{\dimexpr 0.2500\columnwidth - 1.5000\tabcolsep\relax}
1045   >{\centering\arraybackslash}p{\dimexpr 0.2500\columnwidth - 1.5000\tabcolsep\relax}
1046   >{\centering\arraybackslash}p{\dimexpr 0.2500\columnwidth - 1.5000\tabcolsep\relax}
1047   >{\centering\arraybackslash}p{\dimexpr 0.2500\columnwidth - 1.5000\tabcolsep\relax}@{}}
1048 \toprule\noalign{}
1049 \begin{minipage}[b]{\linewidth}\centering
1050 Label
1051 \end{minipage} & \begin{minipage}[b]{\linewidth}\centering
1052 Initial probability, both states
1053 \end{minipage} & \begin{minipage}[b]{\linewidth}\centering
1054 After \(F^\dagger\), signed state
1055 \end{minipage} & \begin{minipage}[b]{\linewidth}\centering
1056 After \(F^\dagger\), unsigned state
1057 \end{minipage} \\
1058 \midrule\noalign{}
1059 \endhead
1060 \bottomrule\noalign{}
1061 \endlastfoot
1062 0 & \(1/3\) & \(0\) & \(4/9\) \\
1063 1 & \(0\) & \(1/4\) & \(0\) \\
1064 2 & \(1/12\) & \(0\) & \(1/36\) \\
1065 3 & \(0\) & \(0\) & \(0\) \\
1066 4 & \(1/12\) & \(0\) & \(1/36\) \\
1067 5 & \(0\) & \(1/4\) & \(0\) \\
1068 6 & \(1/3\) & \(0\) & \(4/9\) \\
1069 7 & \(0\) & \(1/4\) & \(0\) \\
1070 8 & \(1/12\) & \(0\) & \(1/36\) \\
1071 9 & \(0\) & \(0\) & \(0\) \\
1072 10 & \(1/12\) & \(0\) & \(1/36\) \\
1073 11 & \(0\) & \(1/4\) & \(0\) \\
1074 \end{longtable}}
1075 
1076 Every column sums to one. The Fourier probability supports are disjoint.
1077 Negative amplitudes in the original arithmetic signal therefore encode
1078 observable relative phase, even though their signs do not appear in the
1079 first probability column.
1080 
1081 \hypertarget{q:theorem-qa15.-no-inverse-from-the-initial-histogram-alone}{%
1082 \subsection*{Theorem QA15. No inverse from the initial histogram
1083 alone}\label{q:theorem-qa15.-no-inverse-from-the-initial-histogram-alone}}
1084 
1085 There is no function from original-basis probability histograms to state
1086 vectors that reconstructs both \(\psi\) and \(\chi\). There is also no
1087 reconstruction of both states up to overall phase from that histogram
1088 alone.
1089 
1090 \textbf{Proof.} The two histograms are equal by QA13. A function assigns
1091 the same output to equal inputs, so it cannot output the two distinct
1092 vectors. For the phase-insensitive formulation, QA13 shows that the
1093 states are orthogonal and normalized. If \(\chi=\lambda\psi\) for any
1094 complex scalar of modulus one, then
1095 \(\langle\psi,\chi\rangle=\lambda\ne0\), a contradiction. \(\square\)
1096 
1097 The first formulation is formalized in the later publication module. The
1098 strengthening to equivalence up to global phase is a prose corollary
1099 proved here. It is not counted as an additional inherited Lean
1100 declaration.
1101 
1102 \hypertarget{q:the-selector-as-a-projective-measurement}{%
1103 \section{The selector as a projective
1104 measurement}\label{q:the-selector-as-a-projective-measurement}}
1105 
1106 The pair \(\{P,I-P\}\) is a projective measurement because its two
1107 members are self-adjoint, idempotent, orthogonal, and sum to the
1108 identity. For the conditional update we choose the ideal Lüders
1109 instrument, whose unnormalized branches send a density matrix \(\rho\)
1110 to \(P\rho P\) and \((I-P)\rho(I-P)\). The projector effects determine
1111 the outcome probabilities; this chosen instrument determines the state
1112 update. The probability rule and this conditional update can be stated
1113 independently of the arithmetic example.
1114 
1115 \hypertarget{q:theorem-qa16.-selection-probability-and-conditional-state}{%
1116 \subsection*{Theorem QA16. Selection probability and conditional
1117 state}\label{q:theorem-qa16.-selection-probability-and-conditional-state}}
1118 
1119 Let \(P\) be an orthogonal projector on \(\mathbb C^N\) and let \(v\) be
1120 a normalized state. For the ideal Lüders instrument just specified, the
1121 two probabilities are
1122 
1123 \[
1124 p=\|Pv\|^2=\langle v,Pv\rangle,
1125 \qquad 1-p=\|(I-P)v\|^2.
1126 \]
1127 
1128 When \(p>0\), the normalized selected state is \(Pv/\sqrt p\). When
1129 \(1-p>0\), the normalized complementary state is \((I-P)v/\sqrt{1-p}\).
1130 The probabilities belong to \([0,1]\) and sum to one.
1131 
1132 \textbf{Proof.} Since \(P^\dagger P=P\), the quadratic form equals
1133 \(\|Pv\|^2\) and is nonnegative. QA07 applied to a unit vector gives the
1134 probability sum and the upper bound. Division by the positive square
1135 root produces a state of squared norm one in each nonzero branch.
1136 \(\square\)
1137 
1138 For the explicit normalized test signal \(v=x/\sqrt{150}\), QA11 gives
1139 
1140 \[
1141 p=\frac{48}{150}=\frac8{25},
1142 \qquad 1-p=\frac{102}{150}=\frac{17}{25}.
1143 \]
1144 
1145 The selected conditional state is \(c/\sqrt{48}=\psi\), and the
1146 complementary conditional state is \(b/\sqrt{102}\). An exact classical
1147 filter applied to the full vector returns \(c\). A projective
1148 measurement on the normalized input instead returns a branch with these
1149 probabilities. These are compatible uses of the same operator with
1150 different observation rules.
1151 
1152 The vector \(\chi\) makes noninjectivity concrete: \(P\chi=0\) although
1153 \(\|\chi\|=1\). A reversible Fourier change of basis cannot be
1154 substituted for this loss of information. Conversely, retaining both
1155 complementary packets reconstructs every vector, as QA07 and the
1156 publication module explicitly state.
1157 
1158 The inherited formal source certifies the concrete projectors, states,
1159 and probability identities. It does not provide a general quantum
1160 measurement library or a generic theorem implementing the conditional
1161 state-update rule. QA16 is a general prose theorem, with the usual
1162 finite-dimensional measurement interpretation.
1163 
1164 \hypertarget{q:exact-arithmetic-coordinates-and-their-complex-meaning}{%
1165 \section{Exact arithmetic coordinates and their complex
1166 meaning}\label{q:exact-arithmetic-coordinates-and-their-complex-meaning}}
1167 
1168 The twelfth root contains \(\sqrt3\) and \(i\). Its relevant exact
1169 arithmetic can be represented without floating-point trigonometric
1170 evaluation. Let a tuple
1171 
1172 \[
1173 (a,b,c,d)\in\mathbb Q^4
1174 \]
1175 
1176 denote
1177 
1178 \[
1179 \iota(a,b,c,d)=a+b\sqrt3+i(c+d\sqrt3).
1180 \]
1181 
1182 The coordinate root is \((0,1/2,1/2,0)\), whose interpretation is
1183 \(\sqrt3/2+i/2\). Coordinate conjugation sends \((a,b,c,d)\) to
1184 \((a,b,-c,-d)\). Addition is entrywise, and multiplication is
1185 
1186 \[
1187 \begin{aligned}
1188 (a,b,c,d)(A,B,C,D)=\big(&aA+3bB-cC-3dD,\\
1189 &aB+bA-cD-dC,\\
1190 &aC+3bD+cA+3dB,\\
1191 &aD+bC+cB+dA\big).
1192 \end{aligned}
1193 \]
1194 
1195 \hypertarget{q:theorem-qa17.-sound-interpretation-of-the-exact-operations}{%
1196 \subsection*{Theorem QA17. Sound interpretation of the exact
1197 operations}\label{q:theorem-qa17.-sound-interpretation-of-the-exact-operations}}
1198 
1199 The map \(\iota\) preserves zero, one, rational scalars, addition,
1200 multiplication, conjugation, natural powers, and finite sums. Therefore
1201 an equality obtained with these exact coordinate operations yields the
1202 corresponding equality in \(\mathbb C\).
1203 
1204 \textbf{Proof.} The claims for zero, one, rational scalars, addition,
1205 and conjugation follow directly from the definition. For multiplication,
1206 write the two interpreted values as \((a+b\sqrt3)+i(c+d\sqrt3)\) and
1207 \((A+B\sqrt3)+i(C+D\sqrt3)\). Their product has real part
1208 
1209 \[
1210 (a+b\sqrt3)(A+B\sqrt3)-(c+d\sqrt3)(C+D\sqrt3)
1211 \]
1212 
1213 and imaginary part
1214 
1215 \[
1216 (a+b\sqrt3)(C+D\sqrt3)+(c+d\sqrt3)(A+B\sqrt3).
1217 \]
1218 
1219 Expanding and using \((\sqrt3)^2=3\) gives exactly the displayed tuple
1220 product. Power preservation follows by induction from multiplication and
1221 one. Finite-sum preservation follows by induction from addition and
1222 zero. Applying a function to equal coordinate tuples gives equal complex
1223 numbers. \(\square\)
1224 
1225 Only sound transport of equalities is needed here. The formal source
1226 does not install the tuple type as a global field instance, and it does
1227 not need an injectivity theorem for \(\iota\). It proves preservation of
1228 the actual operations and explicitly connects the scales and root to
1229 their conventional complex formulas.
1230 
1231 The matrix interpretation is entrywise. Since multiplication is a finite
1232 sum of products and the adjoint uses conjugation, QA17 also transports
1233 coordinate matrix multiplication and adjoints. The same argument
1234 transports matrix action on vectors and squared norms. This is what
1235 closes the gap between an exact coordinate certificate and an identity
1236 about an ordinary complex unitary matrix.
1237 
1238 \hypertarget{q:the-central-finite-bridge-theorem}{%
1239 \section{The central finite bridge
1240 theorem}\label{q:the-central-finite-bridge-theorem}}
1241 
1242 The arithmetic, signal, and state statements can now be gathered without
1243 leaving any undefined arrow.
1244 
1245 \hypertarget{q:theorem-qa18.-arithmetic-rational-signal-and-unitary-realization}{%
1246 \subsection*{Theorem QA18. Arithmetic, rational signal, and unitary
1247 realization}\label{q:theorem-qa18.-arithmetic-rational-signal-and-unitary-realization}}
1248 
1249 Let \(F\), \(D\), \(P\), \(c\), \(b\), \(x\), \(u\), \(\psi\), and
1250 \(\chi\) have the explicit modulus-twelve definitions above. Then:
1251 
1252 \begin{enumerate}
1253 \def\labelenumi{\arabic{enumi}.}
1254 
1255 \item
1256   \(F^\dagger F=FF^\dagger=I\).
1257 \item
1258   \(P=FDF^\dagger\), \(P^2=P\), and \(P^\dagger=P\).
1259 \item
1260   \(Px=c\) and \((I-P)x=b\), with \(\|x\|^2=48+102=150\).
1261 \item
1262   \(Fu=\psi\) and \(F^\dagger\psi=u\).
1263 \item
1264   \(u\), \(\psi\), and \(\chi\) are normalized, and \(\psi\) is
1265   orthogonal to \(\chi\).
1266 \item
1267   \(\psi\) and \(\chi\) have identical original-basis probabilities.
1268 \item
1269   Their inverse-Fourier coprime probabilities are respectively one and
1270   zero.
1271 \item
1272   \(P\psi=\psi\), \(P\chi=0\), and \(P\) is not injective.
1273 \end{enumerate}
1274 
1275 \textbf{Proof.} QA03 gives the unitarity identities. QA06 gives
1276 projector transport and the two projector identities. QA11 gives the
1277 filter and energy statements. QA12 gives preparation and recovery; the
1278 displayed normalizations and QA13 give statement five and statement six.
1279 QA14 gives statement seven. In Fourier coordinates \(\psi\) is supported
1280 on \(U_{12}\) while \(\chi\) is supported outside it, so \(P\psi=\psi\)
1281 and \(P\chi=0\). The normalized nonzero vector \(\chi\) is therefore in
1282 the kernel, proving noninjectivity. \(\square\)
1283 
1284 The later formal publication theorem gathers the principal complex
1285 transport and probability identities into a single conjunction. Its
1286 supporting modules also supply the exact vector coefficients, filter
1287 recovery, residual reconstruction, and noninjectivity theorem. The
1288 general prose route above explains why the identities hold; the finite
1289 formal source certifies this literal example under its exact
1290 definitions.
1291 
1292 One mathematical object has thus appeared in three realizations.
1293 Arithmetic selects coprime character labels. The signal realization is a
1294 rational circulant projector. The complex state realization uses a
1295 unitary basis change and a projective measurement. The complete vector
1296 information is preserved by the basis change, while selection and
1297 observation have separately stated losses.
1298 
1299 \hypertarget{q:a-continuous-phase-family-with-a-fixed-initial-histogram}{%
1300 \section{A continuous phase family with a fixed initial
1301 histogram}\label{q:a-continuous-phase-family-with-a-fixed-initial-histogram}}
1302 
1303 The two endpoint states are especially simple, but the mechanism is
1304 continuous. Define the nonnegative vectors \(v_+\) and \(v_-\) by
1305 placing \(|c(n)|/\sqrt{48}\) respectively on the positive and negative
1306 entries of \(c\), with zero elsewhere. Thus
1307 
1308 \[
1309 \chi=v_++v_-,
1310 \qquad \psi=v_+-v_-.
1311 \]
1312 
1313 Their supports are disjoint, and each has squared norm \(1/2\). For real
1314 \(\theta\), define
1315 
1316 \[
1317 \chi_\theta=v_++e^{i\theta}v_-.
1318 \]
1319 
1320 It is a normalized state with the same original-basis probabilities for
1321 every \(\theta\). The endpoints are \(\chi_0=\chi\) and
1322 \(\chi_\pi=\psi\).
1323 
1324 \hypertarget{q:theorem-qa19.-relative-phase-response}{%
1325 \subsection*{Theorem QA19. Relative-phase
1326 response}\label{q:theorem-qa19.-relative-phase-response}}
1327 
1328 For this family,
1329 
1330 \[
1331 \boxed{\Pr_{F^\dagger\chi_\theta}(k\in U_{12})
1332 =\|P\chi_\theta\|^2=\sin^2(\theta/2).}
1333 \]
1334 
1335 \textbf{Proof.} Disjoint support gives
1336 \(\|\chi_\theta\|^2=\|v_+\|^2+\|v_-\|^2=1\) and unchanged entrywise
1337 squared magnitudes. Solving for \(v_+\) and \(v_-\) in terms of \(\chi\)
1338 and \(\psi\) gives
1339 
1340 \[
1341 \chi_\theta
1342 =\frac{1+e^{i\theta}}2\chi
1343 +\frac{1-e^{i\theta}}2\psi.
1344 \]
1345 
1346 Since \(P\chi=0\) and \(P\psi=\psi\),
1347 
1348 \[
1349 P\chi_\theta=\frac{1-e^{i\theta}}2\psi.
1350 \]
1351 
1352 Its squared norm is
1353 
1354 \[
1355 \frac{|1-e^{i\theta}|^2}{4}
1356 =\frac{1-\cos\theta}{2}
1357 =\sin^2(\theta/2).
1358 \]
1359 
1360 Finally, \(P=FDF^\dagger\) and unitarity imply
1361 \(\|P\chi_\theta\|^2=\|DF^\dagger\chi_\theta\|^2\), exactly the sum of
1362 the selected Fourier-basis probabilities. \(\square\)
1363 
1364 This is a proved prose extension for the visual guide. It is not
1365 presented as an inherited Lean theorem. It shows that a probability
1366 histogram can stay fixed while an interference-based observation varies
1367 from zero to one.
1368 
1369 \hypertarget{q:phase-replacement-and-dephasing-are-different-operations}{%
1370 \section{Phase replacement and dephasing are different
1371 operations}\label{q:phase-replacement-and-dephasing-are-different-operations}}
1372 
1373 The unsigned endpoint is a coherent state with specified positive
1374 amplitudes. It should not be confused with a state obtained by
1375 forgetting all relative phases. The latter is represented by a mixed
1376 state, not generally by one state vector.
1377 
1378 For a normalized vector \(v\), its density matrix is \(vv^\dagger\).
1379 Complete dephasing in the sample basis keeps only its diagonal entries.
1380 In the present example, dephasing either \(\psi\) or \(\chi\) gives the
1381 same diagonal matrix
1382 
1383 \[
1384 \rho_{\mathrm{diag}}=\operatorname{diag}\big(c(n)^2/48\big)_{n=0}^{11}.
1385 \]
1386 
1387 Its trace is one, and every diagonal entry is nonnegative.
1388 
1389 \hypertarget{q:theorem-qa20.-the-dephased-selected-probability}{%
1390 \subsection*{Theorem QA20. The dephased selected
1391 probability}\label{q:theorem-qa20.-the-dephased-selected-probability}}
1392 
1393 The selected projective-measurement probability of this diagonal state
1394 is
1395 
1396 \[
1397 \operatorname{tr}(P\rho_{\mathrm{diag}})=\frac13.
1398 \]
1399 
1400 \textbf{Proof.} Every diagonal entry of \(P\) is \(c(0)/12=4/12=1/3\).
1401 Multiplication by a diagonal matrix and taking the trace gives
1402 
1403 \[
1404 \operatorname{tr}(P\rho_{\mathrm{diag}})
1405 =\sum_n P_{nn}\frac{c(n)^2}{48}
1406 =\frac13\sum_n\frac{c(n)^2}{48}
1407 =\frac13.
1408 \] \(\square\)
1409 
1410 The three outcomes are therefore distinct: the signed coherent state has
1411 selected probability one, the unsigned coherent state has probability
1412 zero, and the completely dephased state has probability one third. This
1413 calculation prevents an incorrect identification of amplitude sign
1414 removal with physical decoherence. QA20 is a general finite-dimensional
1415 calculation specialized to the example and proved here. Density matrices
1416 and dephasing are outside the inherited Lean package.
1417 
1418 \hypertarget{q:what-is-complete-and-what-remains-a-separate-question}{%
1419 \section{What is complete and what remains a separate
1420 question}\label{q:what-is-complete-and-what-remains-a-separate-question}}
1421 
1422 The finite worked bridge is complete as a mathematical result. Its maps
1423 are defined, its identities are proved, its literal coefficients agree
1424 across the rational and cyclotomic representations, and its principal
1425 modulus-twelve transport and phase claims have formal certificates. The current release provides the traditional paper, visual
1426 guide, formal concordance, source, and reproducibility records.
1427 
1428 The general prose theorems also establish Fourier unitarity, the Möbius
1429 divisor formula, rational divisor-projector completeness, and polyphase
1430 aliasing for the declared finite or formal models. Their
1431 arbitrary-modulus formulations are not claimed as generic Lean
1432 declarations in this package. The continuous phase and dephased-state
1433 extensions are proved prose results rather than inherited formal
1434 additions. The visual guide illustrates the continuous phase family.
1435 
1436 Several broader questions have different proof obligations. Efficient
1437 preparation of coprime-support states needs an algorithm and a cost
1438 model. Efficient circuit synthesis of the twelve-dimensional
1439 transformation or its qubit embedding needs a gate construction and
1440 resource bounds. Incomplete-sample recovery needs an observation map
1441 that is injective on the declared model, or a stability theorem with
1442 stated conditioning. Noisy implementation needs a perturbation analysis.
1443 A physical claim needs an experimental protocol and measured data.
1444 
1445 These questions can be asked using the same operator language. Their
1446 existence does not weaken the exact bridge proved here, and the bridge
1447 does not answer them automatically. The present result shows, in one
1448 fully specified example, how arithmetic selection becomes rational
1449 filtering and phase-sensitive unitary realization while keeping
1450 reconstruction, information loss, and measurement distinct.
1451 

Back to source controls

Back to Quantum and Circuits