Realization Calculus

Download original file

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

Read the typeset paper

1 \section{One seed for the computational basis}\label{supp2:section:001}
2 \textbf{Manuscript item 2.4.}\quad \lean{ComputationalSeed.lean}\hfill 14 declarations
3 
4 For $n\geq 0$, let
5 \[
6  A_n=(\mathbb Z/2\mathbb Z)^{\{0,\ldots,n-1\}},\qquad
7  V_n=\{v:A_n\to\C\}.
8 \]
9 For an address $a\in A_n$, define the standard coordinate vector
10 \[
11  \ket a(x)=\begin{cases}1&x=a,\\0&x\ne a.\end{cases}
12 \]
13 The seed is $\psi_0=\ket0$. Define a translation operator by
14 \[
15  (T_a v)(x)=v(x-a).
16 \]
17 At position $j$, the local Pauli $X$ is $X_j=T_{e_j}$, where $e_j$ has a single nonzero binary coordinate. The formal circuit uses the identity when $a_j=0$ and $X_j$ when $a_j=1$.
18 
19 \begin{statement}\label{supp2:statement:001}
20 For every binary address $a$,
21 \[
22  W_a=\prod_{j=0}^{n-1}X_j^{a_j}=T_a,
23  \qquad W_a\psi_0=\ket a.
24 \]
25 The family $(W_a\psi_0)_{a\in A_n}$ is linearly independent, spans $V_n$, and has exactly $2^n$ elements. It is the standard computational basis.
26 \end{statement}
27 
28 \begin{proof}\phantomsection\label{supp2:proof:001}
29 Composition gives $T_aT_b=T_{a+b}$, and direct evaluation gives $T_a\ket b=\ket{a+b}$. Every binary address satisfies $a+a=0$, so each translation is an involution. In particular, the local operator changes precisely the addressed bit:
30 \[
31  X_j\ket a=\ket{a\text{ with coordinate }j\text{ replaced by }a_j+1}.
32 \]
33 The selected factor at $j$ equals translation by the address supported at $j$ with value $a_j$. Induction on a list proves that the product of translations is translation by their sum. Each of these addresses contributes one coordinate, and their sum is $a$. Thus $W_a=T_a$ and $W_a\psi_0=\ket a$.
34 
35 Lean identifies the resulting family with \lean{Pi.basisFun} over $\C$. Its standard basis theorems supply linear independence and full span. The finite function-space cardinality gives $|A_n|=2^n$.
36 \phantomsection\label{supp2:proof:001:end}\end{proof}
37 
38 \textbf{Formal scope.} The proof constructs the sequence of gates that produces each addressed state and then identifies the resulting family with the standard coordinate basis. It includes the empty circuit for $n=0$. Orthogonality belongs to the usual computational basis interpretation. The formal endpoint records the basis identification, together with separate explicit theorems for span and linear independence.
39 
40 
41 
42 
43 
44 \section{Tensor and polyphase refinement}\label{supp2:section:002}
45 \textbf{Manuscript item 3.2.}\quad \lean{TensorRefinement.lean}\hfill 11 declarations
46 
47 Let $F$ be an arbitrary finite set of factors and let $D_i$ be a finite coordinate index for factor $i$. For matrix families $A_i$, define the coordinate tensor product on the product index space by
48 \[
49  \mathsf T(A)(x,y)=\prod_{i\in F} A_i(x_i,y_i).
50 \]
51 The proof first establishes the laws for multiplication, identity, adjoints, and finite sums. These laws apply to any finite number of factors with the stated finite coordinate sets.
52 
53 Suppose $N>0$ and each factor has a complete orthogonal self-adjoint projector family $(P^{(i)}_j)_{j\in\mathbb Z/N\mathbb Z}$. For a fine address $a:F\to\mathbb Z/N\mathbb Z$, set
54 \[
55  Q_a=\mathsf T\bigl(i\mapsto P^{(i)}_{a_i}\bigr),
56  \qquad
57  C_r=\sum_{\sum_i a_i=r}Q_a.
58 \]
59 
60 \begin{statement}\label{supp2:statement:002}
61 The fine and coarse families are complete orthogonal self-adjoint projector systems. In particular,
62 \[
63  C_rC_s=\delta_{rs}C_r,\qquad
64  \sum_r C_r=I,\qquad C_r^*=C_r.
65 \]
66 Each coarse projector is exactly the displayed sum of its fine descendants.
67 \end{statement}
68 
69 \begin{proof}\phantomsection\label{supp2:proof:002}
70 Expanding the finite product of sums gives
71 \[
72  \mathsf T(A)\mathsf T(B)=\mathsf T(i\mapsto A_iB_i).
73 \]
74 Consequently, if two fine addresses differ in any coordinate, the corresponding product contains a zero factor. If the addresses agree, the product is the same fine projector. The adjoint passes through the finite coordinate product, so $Q_a^*=Q_a$. Summing over all address functions and using the same expansion yields
75 \[
76  \sum_a Q_a=\mathsf T\left(i\mapsto\sum_jP^{(i)}_j\right)=I.
77 \]
78 A separate algebraic regrouping theorem applies to any finite orthogonal family and any address map into a finite set. In the double sum for $C_rC_s$, orthogonality removes all terms with different fine addresses. A surviving address can lie in both classes only when $r=s$. Completeness follows by summing each fine projector exactly once. Adjoint preservation follows term by term. Specializing the address map to total residue proves the claim.
79 \phantomsection\label{supp2:proof:002:end}\end{proof}
80 
81 \textbf{Formal scope.} Residue grouping is proved for every positive modulus and arbitrary finite factor dimensions. It assumes the supplied local projector laws. Constructing those local projectors from cyclic characters, as in item 3.1, requires the separate proof in the next supplement.
82 
83 
84 
85 
86 
87 \section{Differentiated moving coordinates}\label{supp2:section:003}
88 \textbf{Manuscript item 6.1.}\quad \lean{MovingFrames.lean}\hfill 9 declarations
89 
90 Fix a real time $t$ and a finite complex coordinate space. Let $U(s)$ be a unitary matrix curve, differentiable entrywise at $t$, and let $\psi(s)$ be differentiable componentwise at $t$. Write $\dot U$ and $\dot\psi$ for those derivatives. Suppose
91 \[
92  i\dot\psi=H\psi(t).
93 \]
94 Only the value of the Hamiltonian at the chosen time is needed. No derivative of $H$ is assumed.
95 
96 \begin{statement}\label{supp2:statement:003}
97 The explicitly defined coordinate curve
98 \[
99  y(s)=U(s)^*\psi(s)
100 \]
101 is differentiable at $t$, with
102 \[
103  \dot y=\dot U^*\psi(t)+U(t)^*\dot\psi.
104 \]
105 It satisfies
106 \[
107  \boxed{\quad i\dot y=H_{\mathrm{eff}}y(t),\qquad
108  H_{\mathrm{eff}}=U(t)^*HU(t)-iU(t)^*\dot U.\quad}
109 \]
110 The connection term $-iU(t)^*\dot U$ is Hermitian. If $H^*=H$, then $H_{\mathrm{eff}}^*=H_{\mathrm{eff}}$.
111 \end{statement}
112 
113 \begin{proof}\phantomsection\label{supp2:proof:003}
114 Applying the product rule entry by entry proves the differentiation formulas for matrix products and for matrices acting on vectors. Since the parameter is real, conjugation commutes with differentiation, giving the stated derivative of $U^*$ and hence of $y$.
115 
116 Differentiate $U^*U=I$ using those rules and uniqueness of derivatives:
117 \[
118  \dot U^*U+U^*\dot U=0.
119 \]
120 Thus $(U^*\dot U)^*=-U^*\dot U$, so multiplication by $-i$ produces a Hermitian matrix.
121 
122 The identity $UU^*=I$ gives $\psi=Uy$ for the constructed coordinate curve. Differentiating and inserting the original equation yields
123 \[
124  i\dot U y+iU\dot y=HUy.
125 \]
126 Multiplying by $U^*$ and using $U^*U=I$ gives the transformed equation, with the negative sign on the connection term. Finally, conjugation by $U$ preserves Hermiticity of $H$, and the sum of the two Hermitian terms is Hermitian.
127 \phantomsection\label{supp2:proof:003:end}\end{proof}
128 
129 \textbf{Formal scope.} The main certificate constructs $y$ and its derivative rather than assuming a separate derivative witness for the desired answer. Both unitary identities are explicit. The proofs are pointwise and apply at any time where the stated hypotheses hold. They do not assert existence of a global solution to an evolution equation.
130 
131 
132 
133 
134 
135 \section{The canonical packet connection}\label{supp2:section:004}
136 \textbf{Manuscript item 6.3.}\quad \lean{CanonicalConnection.lean}\hfill 9 declarations
137 
138 Let $P_a(s)$ be a finite family in a normed real algebra with a continuous compatible adjoint. Assume actual derivatives $D_a=\dot P_a(t)$ exist and, for all parameter values under consideration,
139 \[
140  P_aP_b=\delta_{ab}P_a,\qquad \sum_aP_a=I,\qquad P_a^*=P_a.
141 \]
142 In the supplied Lean theorem, the curves are defined on $\R$ and the projector laws hold at every real parameter. The algebraic formulation applies to matrices and bounded operators whenever they satisfy the stated typeclass hypotheses.
143 
144 \begin{statement}\label{supp2:statement:004}
145 Define $C=\sum_aD_aP_a(t)$. Then
146 \[
147  \boxed{\quad C=\frac12\sum_a\comm{D_a}{P_a(t)},\qquad C^*=-C,\quad}
148 \]
149 and, for every $b$,
150 \[
151  \boxed{\comm{C}{P_b(t)}=D_b.}
152 \]
153 \end{statement}
154 
155 \begin{proof}\phantomsection\label{supp2:proof:004}
156 The derivative product rule and uniqueness of derivatives give
157 \[
158  D_aP_b+P_aD_b=\delta_{ab}D_a.
159 \]
160 Differentiating completeness and adjoint invariance gives
161 \[
162  \sum_aD_a=0,\qquad D_a^*=D_a.
163 \]
164 These are proved derivative consequences, not additional axioms supplied in place of differentiation.
165 
166 On the diagonal, $D_aP_a+P_aD_a=D_a$. Summing shows
167 \[
168  \sum_aP_aD_a=-\sum_aD_aP_a=-C.
169 \]
170 This proves the formula involving half the sum of commutators, together with $C^*=-C$.
171 
172 Orthogonality directly yields $CP_b=D_bP_b$. For the left product, multiply the differentiated identity for $(b,a)$ on the right by $P_a$ and sum over $a$. Completeness reduces the result to
173 \[
174  D_b+P_bC=D_bP_b.
175 \]
176 Subtracting this equation from the identity for multiplication on the right gives $CP_b-P_bC=D_b$.
177 \phantomsection\label{supp2:proof:004:end}\end{proof}
178 
179 \textbf{Formal scope.} The proof derives the differentiated identities before using their algebraic consequences, so the role of the derivative hypotheses remains explicit. It establishes the canonical connection identity for one parameter. The range bundle over a parameter manifold, the exterior differential calculus, and the curvature theorem of item 6.4 are developed in the later supplements.
180 
181 
182 
183 
184 
185 \section{Finite Kraus channels and full amplification}\label{supp2:section:005}
186 \textbf{Manuscript item 7.2.}\quad \lean{KrausChannels.lean}\hfill 7 declarations
187 
188 For a finite family of complex matrices $K_a$, define
189 \[
190  \Phi(\rho)=\sum_a K_a\rho K_a^*.
191 \]
192 The formalization constructs this as a complex-linear map and proves the following properties directly in the finite matrix representation.
193 
194 \begin{statement}\label{supp2:statement:005}
195 The map $\Phi$ is completely positive. If
196 \[
197  \sum_aK_a^*K_a=I,
198 \]
199 then $\tr\Phi(\rho)=\tr\rho$ for every matrix $\rho$. In particular, positive semidefinite matrices of trace one are mapped to positive semidefinite matrices of trace one.
200 \end{statement}
201 
202 \begin{proof}\phantomsection\label{supp2:proof:005}
203 Matrix multiplication distributes across addition and scalar multiplication, which gives complex linearity. If $\rho\succeq0$, each term $K_a\rho K_a^*$ is positive semidefinite, hence so is their finite sum.
204 
205 To prove complete positivity rather than positivity alone, let $J$ be an arbitrary finite auxiliary index set. For a matrix $X$ indexed by $J\times n$, define its blockwise amplification by
206 \[
207  [\Phi^{(J)}(X)]_{(i,u),(j,v)}
208  =\Phi\bigl(X_{(i,\cdot),(j,\cdot)}\bigr)_{u,v}.
209 \]
210 The explicit index calculation proves the identity
211 \[
212  \boxed{\quad
213  \Phi^{(J)}(X)=\sum_a (I_J\otimes K_a)X(I_J\otimes K_a)^*.
214  \quad}
215 \]
216 The displayed identity identifies the defined amplification with tensoring by the identity, which is the operation needed for complete positivity. Every summand on the right is positive when $X$ is positive, and this holds for every finite $J$.
217 
218 Finally, cyclicity and linearity of the trace give
219 \begin{align*}
220  \tr\Phi(\rho)
221  &=\sum_a\tr(K_a\rho K_a^*)\\
222  &=\tr\left(\left(\sum_aK_a^*K_a\right)\rho\right)
223  =\tr\rho.
224 \end{align*}
225 Positivity together with trace preservation gives the stated conclusion for density matrices.
226 \phantomsection\label{supp2:proof:005:end}\end{proof}
227 
228 \textbf{Formal scope.} Complete positivity is proved for every finite auxiliary dimension. Normalization is required only for trace preservation and the conclusion about density matrices. The converse representation theorem for arbitrary completely positive maps lies outside this argument.
229 
230 
231 
232 
233 

Back to source controls

Back to Realization Calculus