Paper VII: Quantum Seed Calculus

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 \section{Exact packets and arbitrary circuit length}\label{supp1:section:001}
2 Let $R$ be a unital ring, not necessarily commutative, and let $I$ be a finite address set. An exact packet family consists of elements $P_a\in R$ satisfying
3 \[
4 P_aP_b=\begin{cases}P_a,&a=b,\\0,&a\ne b,\end{cases}
5 \qquad \sum_{a\in I}P_a=1.
6 \]
7 Adjoint conditions are added when needed. For an operator $U$, define the transfer corner
8 \[
9 U_{ba}=P_bUP_a.
10 \]
11 The target index comes first. Completeness and distributivity give
12 \[
13 \sum_{b,a}U_{ba}=U,\qquad
14 (UV)_{ba}=\sum_c U_{bc}V_{ca}.
15 \]
16 The second identity uses $P_c^2=P_c$ when adjacent transfer corners are multiplied.
17 
18 \subsection{Circuit paths: source Theorem 4.1}
19 For $U=U_m\cdots U_1$, the checked result is
20 \[
21 P_{a_m}UP_{a_0}
22 =\sum_{a_1,\ldots,a_{m-1}}
23 P_{a_m}U_mP_{a_{m-1}}\cdots P_{a_1}U_1P_{a_0}.
24 \]
25 The Lean implementation defines a recursive path sum and proves the identity by induction over an arbitrary finite gate list. It is not restricted to a fixed circuit depth. The empty list has circuit operator $1$ and path value $P_bP_a$. Summing the source and target indices reconstructs the full circuit.
26 
27 
28 
29 \subsection{Adjoint conservation: source Theorem 4.2}
30 Assume a star operation with $P_a^*=P_a$. Then
31 \[
32 (U_{ba})^*=P_aU^*P_b.
33 \]
34 The two checked conservation laws are
35 \begin{align*}
36 U^*U=1&\quad\Longrightarrow\quad
37 \sum_b(U_{ba})^*U_{bc}=\delta_{ac}P_a,\\
38 UU^*=1&\quad\Longrightarrow\quad
39 \sum_aU_{ba}(U_{da})^*=\delta_{bd}P_b.
40 \end{align*}
41 For the first law, expand each corner, collapse $P_b^2$ and sum:
42 \[
43 \sum_bP_aU^*P_bUP_c
44 =P_aU^*\left(\sum_bP_b\right)UP_c=P_aP_c.
45 \]
46 The second law follows by the analogous calculation and has its own formal proof. For complex matrices, the adjoint is the conjugate transpose. The order of the operator products is preserved throughout.
47 
48 
49 
50 
51 
52 \section{Symmetry and measurement}\label{supp1:section:002}
53 \subsection{Exact symmetry: source Theorem 5.1}
54 If $HP_a=P_aH$ for every packet, then
55 \[
56 P_bHP_a=0\quad(b\ne a),\qquad H=\sum_aP_aHP_a.
57 \]
58 In a complex Banach algebra, commutation also propagates to the actual exponential:
59 \[
60 e^{zH}P_a=P_ae^{zH}\qquad(z\in\C).
61 \]
62 Consequently,
63 \[
64 e^{zH}=\sum_aP_ae^{zH}P_a,
65 \qquad P_be^{zH}P_a=0\quad(b\ne a).
66 \]
67 Taking $z=-it$ gives evolution in real time. The Lean proof applies the exponential commutation theorem directly, so invariance of the packets is a proved consequence of commutation. Self-adjointness of $H$ is not needed for the algebraic reducing property, so this result applies more broadly than the Hermitian specialization in the paper.
68 
69 
70 
71 This result describes exact symmetry. The quantitative leakage estimate when symmetry is broken appears in Theorem 5.2 and requires the separate Duhamel and norm arguments developed later.
72 
73 \subsection{Measurements: source Theorem 7.1}
74 For finite complex matrices, define packet dephasing by
75 \[
76 \deph(X)=\sum_aP_aXP_a.
77 \]
78 The code proves idempotence and trace duality:
79 \[
80 \deph(\deph(X))=\deph(X),\qquad
81 \tr\bigl(\deph(E)\rho\bigr)=\tr\bigl(E\deph(\rho)\bigr).
82 \]
83 Trace duality follows term by term from cyclicity:
84 \[
85 \tr(P_aEP_a\rho)=\tr(EP_a\rho P_a).
86 \]
87 Therefore an effect that is diagonal in the packets, $\deph(E)=E$, satisfies
88 \[
89 \boxed{\tr(E\rho)=\tr\bigl(E\deph(\rho)\bigr).}
90 \]
91 The proof holds for arbitrary finite complex matrices $E$ and $\rho$. Density matrices and positive measurement effects are valid specializations rather than assumptions needed for this trace identity. Taking $E=1$ also gives trace preservation of packet dephasing.
92 
93 
94 
95 The full theorem for Kraus channels and the Knill--Laflamme recovery criterion require further arguments about positivity, auxiliary systems, and recovery maps. The trace identity above supplies only the measurement statement.
96 
97 
98 
99 \section{Corrected Feshbach resolvent}\label{supp1:section:003}
100 Write a finite complex matrix in retained and eliminated coordinates:
101 \[
102 H=\begin{pmatrix}A&B\\C&D\end{pmatrix},\qquad
103 zI-H=\begin{pmatrix}zI_P-A&-B\\-C&zI_Q-D\end{pmatrix}.
104 \]
105 Set
106 \[
107 D_z=zI_Q-D,\qquad S_z=zI_P-A-BD_z^{-1}C.
108 \]
109 The effective Hamiltonian is $H_{\mathrm{eff}}(z)=A+BD_z^{-1}C$, so
110 $S_z=zI_P-H_{\mathrm{eff}}(z)$.
111 
112 \subsection{Correct statement: source Theorem 9.1}
113 Assume both $D_z$ and $zI-H$ are invertible. Then $S_z$ is invertible and
114 \[
115 \boxed{\bigl((zI-H)^{-1}\bigr)_{PP}=S_z^{-1}.}
116 \]
117 The left side is the submatrix of the full inverse on the retained coordinates. This matches the paper's compressed operator when written in an orthonormal basis of the retained subspace. The proof is valid for arbitrary complex blocks of compatible sizes and does not require Hermiticity.
118 
119 The checked invertibility criterion is
120 \[
121 D_z\text{ invertible}\quad\Longrightarrow\quad
122 \bigl(zI-H\text{ invertible}\ \Longleftrightarrow\ S_z\text{ invertible}\bigr).
123 \]
124 Thus one may equivalently assume invertibility of $D_z$ and $S_z$.
125 
126 \textbf{Why the original assumption is insufficient.}
127 Take $z=0$ and $H=\diag(0,-1)$, retaining the first coordinate. Then
128 \[
129 D_z=1,\qquad zI-H=\begin{pmatrix}0&0\\0&1\end{pmatrix}.
130 \]
131 The eliminated block is invertible, but the full matrix is singular. Hence the original hypothesis does not ensure the existence of its stated resolvent. The Lean counterexample proves invertibility of the scalar $1$ and noninvertibility of this full $2\times2$ matrix.
132 
133 
134 
135 \subsection{Provenance and limits}
136 The proof of the general block inverse was reused from the checked fifth block of Paper VI and compiled in the Paper VII namespace for the archived formal checkpoint. That formal development also added the counterexample above. The retained checkpoint is dated 6 September 2026. This edition revises the exposition without claiming a new Schur identity or a fresh Lean compilation.
137 
138 The memory equation in the time domain in Section 9.2, resolvent control uniform in the cutoff, and continuum limits require arguments beyond this finite inverse identity. The source amendment makes the two invertibility assumptions explicit without changing the intended effective Hamiltonian.
139 
140 
141 
142 \section{Dispersion with an explicit spacing condition}\label{supp1:section:004}
143 The grid eigenvalue in source Theorem 11.1 is
144 \[
145 \lambda_{k,h}=\frac{4}{h^2}\sin^2\left(\frac{kh}{2}\right).
146 \]
147 The original low-mode condition is $0\le kh/2\le1$. A nonzero spacing is also required for the quotient to have its intended meaning. For a physical grid, one normally takes $h>0$.
148 
149 \subsection{Checked stronger statement}
150 For every $k,h\in\R$ with $h\ne0$,
151 \[
152 \boxed{0\le k^2-\lambda_{k,h}\le\frac{k^4h^2}{12}.}
153 \]
154 The code proves this without the low-mode restriction. The bound may be loose away from the low-mode regime, but it remains valid.
155 
156 The proof begins with an estimate valid for every real argument:
157 \[
158 0\le x^2-\sin^2x\le\frac{x^4}{3}.
159 \]
160 The lower bound follows from $|\sin x|\le|x|$. For the upper bound, use
161 \[
162 |x-\sin x|\le\frac{|x|^3}{6},\qquad
163 |x+\sin x|\le2|x|.
164 \]
165 Factoring the difference of squares gives
166 \[
167 0\le x^2-\sin^2x
168 =|x-\sin x|\,|x+\sin x|
169 \le\frac{x^4}{3}.
170 \]
171 With $x=kh/2$ and $h\ne0$,
172 \begin{align*}
173 k^2-\lambda_{k,h}
174 &=\frac4{h^2}\left(x^2-\sin^2x\right),\\
175 \frac4{h^2}\frac{x^4}{3}
176 &=\frac{k^4h^2}{12}.
177 \end{align*}
178 Every algebraic transformation and inequality in the active source was accepted by Lean.
179 
180 
181 
182 \subsection{What this does not establish}
183 This is an exact deterministic error bound for the displayed dispersion relation. The original paper's numerical convergence experiment and spectral dimension measurements provide a different kind of evidence and were not rerun during this prose revision. The bound alone does not select a physical spacetime geometry.
184 
185 
186 
187 \section{A constraint diagnostic that vanishes automatically}\label{supp1:section:005}
188 Section 12 defines the physical projector using the exact common kernel of the constraints. In finite dimensions this gives $C_aP=0$ for every $a$. Absorb the factor $i$ and any structure coefficient into $f_c$, and write
189 \[
190 \mathcal A_{ab}=C_aC_b-C_bC_a-\sum_cf_cC_c.
191 \]
Statement: Exact common-kernel compression · Go to proof · Read statement and proof side by side192 \begin{proposition}[Exact common-kernel compression]\label{supp1:proposition:001}
193 If $C_cP=0$ for every $c$, then
194 \[
195 \mathcal A_{ab}P=0,\qquad P\mathcal A_{ab}P=0.
196 \]
197 No idempotence or adjoint property of $P$ is needed for this implication.
198 \end{proposition}
Proof block: Exact common-kernel compression · Go to statement · Read statement and proof side by side199 \begin{proof}\phantomsection\label{supp1:proof:001}
200 Associativity gives
201 \[
202 \mathcal A_{ab}P=C_a(C_bP)-C_b(C_aP)-\sum_cf_c(C_cP)=0.
203 \]
204 Left multiplication by $P$ gives the second identity.
205 \phantomsection\label{supp1:proof:001:end}\end{proof}
206 
207 \subsection{Compressed vanishing without operator closure}
208 Over the rationals, take
209 \[
210 P=\begin{pmatrix}1&0&0\\0&0&0\\0&0&0\end{pmatrix},\quad
211 X=\begin{pmatrix}0&0&0\\0&0&1\\0&1&0\end{pmatrix},\quad
212 Z=\begin{pmatrix}0&0&0\\0&1&0\\0&0&-1\end{pmatrix}.
213 \]
214 These displayed matrices are symmetric. The code checks that $P^2=P$, $P\ne0$ and $XP=ZP=0$, but
215 \[
216 [X,Z]=\begin{pmatrix}0&0&0\\0&0&-2\\0&2&0\end{pmatrix}\ne0,
217 \qquad P[X,Z]P=0.
218 \]
219 The commutator therefore violates the closure relation with zero structure coefficients outside the physical range, even though its physical compression vanishes exactly.
220 
221 
222 
223 \subsection{Interpretation for the paper}
224 Vanishing of the compressed anomaly is automatic for the exact finite common kernel. It therefore cannot by itself certify full operator closure. A nonzero computed compression would instead contradict those exact assumptions or expose an approximation or implementation defect.
225 
226 Existence of a nontrivial compatible refinement tower and the broader continuum program remain separate questions. A stronger closure claim must test more than this compression, and unbounded constraints need their operator domains specified. This audit is additional to the six checked source items and is not counted as a seventh original theorem.
227 
228 
229 

Back to source controls

Back to Paper VII: Quantum Seed Calculus