Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates

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{A typed quiver model}
2 
3 A small quiver model shows how the path algebra records a direction that the available seeds cannot reach.
4 
5 Let the quiver have vertices $U,V$ and arrows
6 \[
7 R:U\to U,
8 \qquad
9 A:U\to V,
10 \qquad
11 B:V\to U,
12 \]
13 with the relation in the path algebra
14 \[
15 BA=e_U,
16 \]
17 whose realization is the operator identity $BA=I_U$.
18 Realize
19 \[
20 U=\bbk^2,
21 \qquad
22 V=\bbk^3,
23 \]
24 by
25 \[
26 R=
27 \begin{pmatrix}0&-1\\1&0\end{pmatrix},
28 \qquad
29 A(u_1,u_2)=(u_1,u_2,0),
30 \qquad
31 B(v_1,v_2,v_3)=(v_1,v_2).
32 \]
33 Starting from the seed $e_1\in U$, repeated application of $R$ spans $U$, and $A$ carries that span onto the first two coordinates of $V$. Any path from $U$ to $V$ ends with $A$ and therefore lands in $\im A$. The third coordinate direction, which spans $\ker B$, is unreachable from a seed supported only at $U$. Therefore the generated representation is
34 \[
35 U\oplus\Span\{(1,0,0),(0,1,0)\}
36 \subsetneq U\oplus V.
37 \]
38 Adding the seed $(0,0,1)\in V$ generates the full representation.
39 
40 \begin{proposition}[Typed reachability certificate]
41 \label{prop:typed-reachability}
42 In the preceding quiver realization, no seed supported at $U$ can generate the full representation, whereas the two seeds
43 \[
44 e_1\in U,
45 \qquad
46 e_3\in V
47 \]
48 do generate it.
49 \end{proposition}
50 
51 \begin{proof}
52 The first claim follows because every path that starts at $U$ and ends in $V$ has final arrow $A$, so its image lies in $\im A$. For the second, $e_1$ and $Re_1$ span $U$. Their images under $A$ span $\im A$, and $e_3$ spans $\ker B$, the missing complementary direction in $V$.
53 \end{proof}
54 
55 This example shows why a typed grammar is more than a notational convenience. The obstruction lies in the subspace $\ker B\subset V$, which is unreachable from seeds supported at $U$, and is visible before any coordinate calculation.
56 
57 The arrow from one vertex to another records which type can be reached. Its image records which directions can be reached within that type. Here the first seed reaches both vertices, yet misses one direction at the second vertex. The extra seed supplies that direction directly. This is why reachability of a vertex alone does not settle generation of its entire space.
58 
59 \section{Worked algebraic model: an elliptic coordinate ring}
60 
61 Let $\operatorname{char}\bbk\ne2$ and let
62 \[
63 A=\bbk[x,y]/(y^2-x^3+x).
64 \]
65 The affine equation $y^2=x^3-x$ has classical discriminant $64$, which is nonzero under this hypothesis. Standard algebraic geometry then identifies its smooth projective completion as an elliptic curve \cite{silverman2009}. The Lean development checks the algebraic implication $2\ne0\Rightarrow64\ne0$, the quotient normal form, and the operator identities below. It does not formalize projective smoothness, genus, or the geometric identification of the discriminant. The packet computation itself uses only the displayed relation in the quotient ring.
66 Every class has a unique normal form
67 \[
68 f(x,y)=a(x)+y b(x).
69 \]
70 Indeed, $y^2-(x^3-x)$ is monic of degree two in $y$, so division in $\bbk[x][y]$ gives a unique remainder of degree less than two in $y$. Concretely, every power $y^m$ with $m\ge2$ can be reduced using
71 \[
72 y^2=x^3-x.
73 \]
74 
75 \subsection{One module seed and two address operators}
76 
77 Take the seed
78 \[
79 s=1
80 \]
81 and let $M_x,M_y$ be multiplication by $x$ and $y$. Then
82 \[
83 M_x^iM_y^js=x^iy^j,
84 \]
85 so the algebra, regarded as a module over its multiplication algebra, is generated by one seed.
86 
87 The two packet spaces are
88 \[
89 A_0=\bbk[x],
90 \qquad
91 A_1=y\bbk[x].
92 \]
93 Let
94 \[
95 P_0(a+yb)=a,
96 \qquad
97 P_1(a+yb)=yb.
98 \]
99 These idempotents are linear over $\bbk$, annihilate one another, and satisfy $P_0+P_1=I$. They are not module maps over $A$, because multiplication by $y$ exchanges the two packets.
100 
101 Identify the packet coefficients by
102 \[
103 A_0\oplus A_1\longrightarrow\bbk[x]\oplus\bbk[x],
104 \qquad
105 (a,yb)\longmapsto(a,b).
106 \]
107 In these ordered coefficient coordinates, with $M_x$ and $M_{x^3-x}$ denoting multiplication on $\bbk[x]$,
108 \[
109 {
110 M_x=
111 \begin{pmatrix}
112 M_x&0\\
113 0&M_x
114 \end{pmatrix},
115 \qquad
116 M_y=
117 \begin{pmatrix}
118 0&M_{x^3-x}\\
119 I&0
120 \end{pmatrix}.
121 }
122 \]
123 The two rows of the second matrix record the outgoing packet coefficients. An even input enters the odd packet without an additional factor. An odd input returns to the even packet through the factor imposed by the curve equation. Applying the matrix twice therefore preserves each packet and multiplies its coefficient by that factor.
124 
125 The relation is reconstructed as an operator identity:
126 \[
127 M_y^2=M_x^3-M_x.
128 \]
129 
130 \begin{figure}[htbp]
131 \centering
132 \includegraphics[width=0.96\textwidth]{08_elliptic_packet_transfer.pdf}
133 \caption{Multiplication by $y$ exchanges the even and odd packets. The transfer from the odd packet to the even packet carries the relation weight $x^3-x$.}
134 \label{fig:elliptic-transfer}
135 \end{figure}
136 
137 \subsection{Exact product law}
138 
139 Write
140 \[
141 f=a_0+ya_1,
142 \qquad
143 g=b_0+yb_1.
144 \]
145 Then
146 \[
147 {
148 fg
149 =
150 \bigl(a_0b_0+(x^3-x)a_1b_1\bigr)
151 +
152 y\bigl(a_0b_1+a_1b_0\bigr).
153 }
154 \]
155 This is a convolution law for the two packets. It is already visible at the linear operator level because multiplication by a fixed element is a transfer operator. The even output collects the product of the two even coefficients and the weighted product of the two odd coefficients. The odd output collects the two products with one even and one odd coefficient. The quotient relation is thus retained in the weight rather than discarded during the decomposition.
156 
157 \begin{example}[Worked reduction]
158 Take
159 \[
160 f=x^2+y,
161 \qquad
162 g=x-y.
163 \]
164 Then
165 \[
166 \begin{aligned}
167 fg
168 &=x^3-x^2y+xy-y^2\\
169 &=x^3-x^2y+xy-(x^3-x)\\
170 &=x+(x-x^2)y.
171 \end{aligned}
172 \]
173 Thus
174 \[
175 P_0(fg)=x,
176 \qquad
177 P_1(fg)=(x-x^2)y.
178 \]
179 The symbolic certificate in the companion code performs the same quotient reduction exactly.
180 \end{example}
181 
182 \subsection{What this example establishes}
183 
184 The coordinate ring illustrates four distinct parts of the calculus:
185 \begin{enumerate}[label=(\roman*)]
186 \item the unit is a module seed.
187 \item $M_x$ and $M_y$ are address operators.
188 \item the curve equation is an operator relation.
189 \item parity in $y$ gives exact packet analysis, transfer, and reconstruction.
190 \end{enumerate}
191 It does not imply that every algebra can be presented as an algebra generated by one element. It shows instead that unital algebras are cyclic as modules over their full multiplication algebra.
192 
193 \section{Worked signal model: a bilateral shift}
194 
195 Let $\mathbb{F}\in\{\R,\C\}$ and let
196 \[
197 X=\ell^2(\Z;\mathbb F)
198 \]
199 with a family of bounded reindexing operators indexed by the integers
200 \[
201 (S_mx)[n]=x[n-m]
202 \qquad(m,n\in\Z).
203 \]
204 Thus $S_0=I$, $S_{m+r}=S_mS_r$, and $S_1$ is the usual bilateral shift. We use the standard conventions for Hilbert spaces and bounded operators of \cite{conway1990}.
205 The impulse $\delta_0$ satisfies
206 \[
207 S_m\delta_0=\delta_m
208 \]
209 for every $m\in\Z$. Therefore sequences with finite support lie in its algebraic orbit hull and are dense in $\ell^2(\Z)$.
210 
211 \begin{proposition}[Shift seed]
212 \label{prop:shift-seed}
213 For $n\in\N$, let $G(n)$ mean that some finite seed set with $n$ elements has dense hull under the declared family $\{S_m:m\in\Z\}$. Then
214 \[
215 {
216 1=\min\{n\in\N:G(n)\}.
217 }
218 \]
219 Equivalently, one seed suffices and no empty seed family generates densely.
220 \end{proposition}
221 
222 \begin{proof}
223 The orbit of $\delta_0$ contains every standard basis vector. Their finite linear span is dense, so $G(1)$ holds. The hull of the empty seed set is zero, while $\ell^2(\Z;\mathbb F)$ is nonzero, so $G(0)$ fails. Therefore $1$ is the least admissible finite cardinality.
224 \end{proof}
225 
226 For $N\ge1$, define residue projectors
227 \[
228 (P_{N,j}x)[n]
229 =
230 \begin{cases}
231 x[n],&n\equiv j\pmod N,\\0,&\text{otherwise.}\end{cases}
232 \]
233 They form an orthogonal packet system and satisfy
234 \[
235 S_1P_{N,j}=P_{N,j+1}S_1,
236 \]
237 with indices modulo $N$. The shift is therefore a cyclic transfer between residue packets.
238 
239 The seed claim concerns density, rather than equality with the algebraic hull. Finite linear combinations of shifted impulses give precisely the sequences with finite support. Taking their closure gives the whole Hilbert space. The packet decomposition and the choice of completion answer different questions, and both must be specified for this realization.
240 
241 \begin{figure}[htbp]
242 \centering
243 \includegraphics[width=0.96\textwidth]{07_shift_packet_transfer.pdf}
244 \caption{Support among residue packets in the periodic shift model on 24 coordinates with six packets. Each input residue transfers into the next output residue. The theorem for the infinite bilateral shift is established separately in the text.}
245 \label{fig:shift-transfer}
246 \end{figure}
247 
248 \begin{boundary}
249 This section uses residue packets only to demonstrate the foundational transfer algebra. Nested refinement and structures for filter banks require additional definitions and are outside Paper I.
250 \end{boundary}
251 
252 \section{Worked matrix models}
253 
254 \subsection{The full matrix algebra}
255 
256 Let $X=\bbk^n$ and let $\cA=M_n(\bbk)=\End_{\bbk}(X)$, with the full matrix algebra declared before a seed or target is chosen. By \cref{cor:full-matrix}, every nonzero seed is cyclic. This is the maximal linear grammar on $X$. It does not give a compression result. Under a smaller declared operator algebra, the same vector need not be cyclic.
257 
258 \subsection{Companion operators and repeated blocks}
259 
260 For one operator $T$, \cref{thm:single-operator} turns verified primary data
261 into an exact certificate for the minimum number of seeds.  The numerical companion compares:
262 \begin{enumerate}[label=(\alph*)]
263 \item a nilpotent companion operator with one Jordan chain, for which the Krylov rank is $1,2,\ldots,n$.
264 \item two equal Jordan blocks, for which one diagonal seed produces a chain only as long as one block and then stalls.
265 \end{enumerate}
266 
267 The observed stall is not numerical failure.  The associated
268 scalar quotient of dimension two certifies the lower bound in
269 \cref{thm:single-operator}. Identifying that quotient with the space that
270 measures geometric multiplicity is the classical Jordan input stated above.
271 
272 \section{Worked graph model: adjacency algebras}
273 
274 Let $G$ be a nonempty finite graph with adjacency matrix $A_G$, and regard
275 $\bbk^{V(G)}$ as a module over $\bbk[A_G]$.  The general result applies directly to a spectral certificate. For a symmetric real adjacency matrix, the classical spectral theorem supplies such data.
276 
277 Within one eigenspace, every polynomial in the adjacency operator acts by a scalar. A seed therefore supplies at most one vector direction in that eigenspace. Distinct eigenvalues can be separated by projector polynomials, so the same seed may supply one direction to each of several eigenspaces. With a complete eigenbasis, the largest eigenspace determines how many seeds are needed, rather than the number of distinct eigenvalues.
278 
279 \begin{corollary}[Certified graph seed number]
280 \label{cor:graph-rank}
281 Let $\bbk$ be a field and let $\Lambda$ be a nonempty finite set.  Suppose
282 there are pairwise distinct scalars $a_{\lambda}\in\bbk$, multiplicities
283 $m_{\lambda}\in\N$, and an eigenbasis
284 \[
285 \{b_{\lambda,j}:\lambda\in\Lambda,\ 1\le j\le m_{\lambda}\}
286 \]
287 of $\bbk^{V(G)}$ satisfying
288 \[
289 A_Gb_{\lambda,j}=a_{\lambda}b_{\lambda,j}.
290 \]
291 If $m_{\lambda}\le R$ for all $\lambda$ and
292 $m_{\lambda_*}=R$ for some $\lambda_*$, then $R$ is the least natural number
293 of adjacency seeds:
294 \[
295 {
296 R=\min\left\{r\in\N:
297 \begin{array}{l}
298 \text{there exist }s_1,\ldots,s_r\text{ with}\\[2pt]
299 \bbk^{V(G)}=\Span_{\bbk}
300   \{p(A_G)s_j:p\in\bbk[t],\ 1\le j\le r\}
301 \end{array}
302 \right\}.
303 }
304 \]
305 \end{corollary}
306 
307 \begin{proof}
308 The distinct eigenvalue labels give Lagrange polynomials that project onto
309 the individual eigenspace packets.  Padding one basis vector from every
310 packet into each of $R$ seeds gives the upper bound.  Projection to the
311 $m_{\lambda}$ eigenspace coordinates is a surjective scalar quotient, so any
312 generating family has at least $m_{\lambda}$ members for every $\lambda$.
313 The label $\lambda_*$ gives the matching lower bound $R$.
314 \end{proof}
315 
316 \begin{boundary}[Input from spectral classification]
317 For a finite undirected graph over $\C$, the spectral theorem for real symmetric matrices
318 classically supplies a certificate of the displayed kind, and the numbers
319 $m_{\lambda}$ are the usual eigenvalue multiplicities. See
320 \cite{brouwerHaemers2012}.  The formal declaration verifies the
321 formula for the number of seeds from the supplied eigenbasis and distinct eigenvalue
322 labels.  It does not derive diagonalizability from symmetry or implement an
323 eigensolver.
324 \end{boundary}
325 
326 \subsection{Path graphs}
327 
328 For every field $\bbk$ and every $n\ge1$, an endpoint of $P_n$ is a cyclic
329 vector for the adjacency operator.  Consequently one is the least finite
330 number of adjacency seeds:
331 \[
332 {
333 1=\min\left\{r\in\N:
334 \exists s_1,\ldots,s_r,\quad
335 \bbk^n=\Span_{\bbk}\{p(A_{P_n})s_j:p\in\bbk[t],\ 1\le j\le r\}
336 \right\}.
337 }
338 \]
339 Over $\C$, the familiar spectral description has the distinct eigenvalues
340 \[
341 \lambda_k=2\cos\frac{k\pi}{n+1},
342 \qquad 1\le k\le n,
343 \]
344 and the normalized eigenvectors have endpoint coordinate proportional to
345 \[
346 \sin\frac{k\pi}{n+1}\ne0.
347 \]
348 There is also a combinatorial proof valid over every field.  Let
349 \[
350 K_n=[e_1,Ae_1,\ldots,A^{n-1}e_1].
351 \]
352 Its $(i,j)$ entry counts walks of length $j-1$ from the first vertex to vertex $i$. This entry is zero when $i>j$, while the diagonal entry is one because there is a unique shortest walk of length $i-1$ from vertex $1$ to vertex $i$. Hence $K_n$ is upper triangular with unit diagonal, so
353 \[
354 \det K_n=1
355 \qquad(n\ge1).
356 \]
357 Thus the endpoint is cyclic for every path size, not merely for the tested range.
358 
359 \begin{figure}[htbp]
360 \centering
361 \includegraphics[width=0.96\textwidth]{05_path_graph_seed_rank.pdf}
362 \caption{The endpoint Krylov certificate gives every nonempty path one adjacency seed.}
363 \label{fig:path-rank}
364 \end{figure}
365 
366 \subsection{Cycle graphs}
367 
368 Two adjacent vertex vectors generate the adjacency module of every simple
369 cycle.  Over $\C$, a Fourier quotient built from a primitive root of unity supplies a matching
370 scalar obstruction of dimension two.  Hence, for every $n\ge3$, two is the
371 least finite number of adjacency seeds:
372 \[
373 {
374 2=\min\left\{r\in\N:
375 \exists s_1,\ldots,s_r,\quad
376 \C^n=\Span_{\C}\{p(A_{C_n})s_j:p\in\C[t],\ 1\le j\le r\}
377 \right\}.
378 }
379 \]
380 To see the upper bound directly, index the vertices modulo $n$.
381 The identity $Ae_j=e_{j-1}+e_{j+1}$ recovers successive vertex vectors
382 from $e_0$ and $e_1$, over any field. For the lower bound over $\C$, let
383 $\zeta$ be a primitive $n$th root of unity and define
384 \[
385 q(x)=\left(\sum_{j=0}^{n-1}\zeta^j x_j,
386              \sum_{j=0}^{n-1}\zeta^{-j}x_j\right).
387 \]
388 Then $q(Ax)=(\zeta+\zeta^{-1})q(x)$. The images of $e_0$ and $e_1$
389 are $(1,1)$ and $(\zeta,\zeta^{-1})$, which are independent because
390 $\zeta\ne\zeta^{-1}$ for $n\ge3$. Thus $q$ is a scalar quotient
391 of dimension two, and \cref{prop:scalar-quotient} gives the
392 matching lower bound.
393 
394 The usual spectral description writes the eigenvalues as
395 \[
396 \lambda_k=2\cos\frac{2\pi k}{n},
397 \qquad 0\le k<n.
398 \]
399 The values for $k$ and $n-k$ coincide. Apart from the simple characters at $k=0$ and, for even $n$, $k=n/2$, the remaining Fourier characters occur in pairs. Therefore the maximum eigenspace multiplicity is two, although some eigenspaces have multiplicity one, and
400 the certified minimum above is two.
401 
402 \begin{figure}[htbp]
403 \centering
404 \includegraphics[width=0.96\textwidth]{06_cycle_graph_seed_rank.pdf}
405 \caption{Cycle graphs have maximum eigenspace multiplicity two for the adjacency operator and therefore require two adjacency seeds, although one or two exceptional eigenspaces are simple.}
406 \label{fig:cycle-rank}
407 \end{figure}
408 
409 The path and cycle examples use nearly identical local operators.  Their
410 minimum finite seed numbers differ because the path has an
411 endpoint Krylov basis, whereas the cycle has a Fourier
412 quotient obstruction of dimension two.
413 
414 \section{The common operator language}
415 
416 The preceding examples can be written without changing the foundational notation.
417 
418 \begin{longtable}{L{0.12\textwidth}L{0.13\textwidth}L{0.19\textwidth}L{0.17\textwidth}L{0.16\textwidth}}
419 \caption{Foundational realizations of the common operator language.}\label{tab:dictionary}\\
420 \toprule
421 Realization & Seed & Operator grammar & Packets & Completion or quotient \\
422 \midrule
423 \endfirsthead
424 \toprule
425 Realization & Seed & Operator grammar & Packets & Completion or quotient \\
426 \midrule
427 \endhead
428 Coordinate ring & $1$ & $M_x,M_y$ & even/odd $y$ degree & quotient by $y^2-x^3+x$ \\
429 Shift system & $\delta_0$ & $(S_m)_{m\in\Z}$ & residue classes of $n$ & $\ell^2$ closure \\
430 Full matrix module & $s\ne0$ & $M_n(\bbk)$ & chosen idempotents & finite dimensional \\
431 Single operator & $s_1,\ldots,s_r$ & $\bbk[T]$ & primary or spectral & finite dimensional \\
432 Graph adjacency & vertex seeds & $\bbk[A_G]$ & eigenspaces & finite dimensional \\
433 Typed grammar & vertex seeds & path algebra $\bbk Q/I$ & vertex idempotents & relation quotient \\
434 \bottomrule
435 \end{longtable}
436 
437 \Needspace{16\baselineskip}
438 For a finite ordered seed family $S=(s_1,\ldots,s_r)$, let $\varepsilon_S:\cA^{\oplus r}\to X$ be the seed evaluation map of \cref{def:seed-evaluation}.  Its kernel is the relation module.  The free module modulo that kernel presents the generated hull by \cref{thm:free-presentation}.  The invariant content is:
439 \[
440 {
441 \begin{aligned}
442 &\text{generated hull: }\Hull_{\cA}(S),\\
443 &\text{seed complexity: }\srank_{\cA}(X),\\
444 &\text{packet coordinates: }x\leftrightarrow(P_{\alpha}x)_{\alpha},\\
445 &\text{operator coordinates: }T\leftrightarrow(P_{\beta}TP_{\alpha})_{\beta,\alpha},\\
446 &\text{relation module: }N_S:=\Ker\varepsilon_S\leq\cA^{\oplus r},\\
447 &\text{free presentation: }\cA^{\oplus r}/N_S\cong\Hull_{\cA}(S),\\
448 &\text{coordinate invariance: }P_{\alpha}\mapsto UP_{\alpha}U^{-1},\\
449 &\text{realization: }\Phi A=\varphi(A)\Phi.
450 \end{aligned}
451 }
452 \]
453 
454 \begin{figure}[htbp]
455 \centering
456 \includegraphics[width=0.96\textwidth]{10_theorem_dependency.pdf}
457 \caption{Structural overview of the two proof families. The generator and packet arguments meet in the worked realizations. This diagram is not an exhaustive graph of Lean declaration dependencies.}
458 \label{fig:dependency}
459 \end{figure}
460 
461 \section{Computational certificates}
462 
463 The accompanying Python package is not used as a substitute for proof. It provides exact symbolic checks and finite numerical regression tests for formulas already proved. The computed ranges and random seeds are recorded explicitly. These checks do not extend a theorem beyond its hypotheses or certify an unrestricted numerical implementation. The journal companion also tests integer counts beyond the precision of floating point arithmetic and rejects the unsupported spectral shortcut for complex symmetric matrices.
464 
465 \subsection{Test suite}
466 
467 The test suite checks:
468 \begin{enumerate}[label=(\roman*)]
469 \item projector idempotence, annihilation, and completeness.
470 \item exact vector analysis and synthesis.
471 \item exact operator reconstruction from all transfer blocks.
472 \item coordinate transport under a dense random similarity transform.
473 \item cyclicity of a companion operator.
474 \item the obstruction that requires two seeds for repeated Jordan blocks.
475 \item the semisimple multiplicity formula in representative cases.
476 \item full orbit dimension for two representative nonzero seeds under the full matrix algebra.
477 \item exact reduction and packet multiplication in the elliptic coordinate ring.
478 \item seed ranks of path and cycle adjacency modules over the reported finite ranges.
479 \item the cyclic residue transfer pattern of a finite shift.
480 \end{enumerate}
481 
482 \subsection{Recorded results}
483 
484 \begin{table}[htbp]
485 \centering
486 \caption{Archived representative checks from the v1.3.1 journal edition run. Fresh companion runs are reported separately in the release verification record.}
487 \label{tab:results}
488 \begin{tabular}{L{0.57\textwidth}r}
489 \toprule
490 Quantity & Result \\
491 \midrule
492 Projector idempotence residual & $0$ \\
493 Projector annihilation residual & $0$ \\
494 Projector completeness residual & $0$ \\
495 Operator reconstruction residual & $0$ \\
496 Residual for transported projectors, maximum & $1.85\times10^{-15}$ \\
497 Companion seed rank & $1$ \\
498 Two equal Jordan blocks, seed rank & $2$ \\
499 $M_3(\C)$ acting on seven copies, seed rank & $3$ \\
500 Sampled path graph seed ranks, $2\le n\le12$ & $1$ \\
501 Sampled cycle graph seed ranks, $3\le n\le12$ & $2$ \\
502 Full $M_4(\R)$ orbit dimensions for two sampled nonzero seeds & $4,4$ \\
503 Automated tests & $33/33$ passed \\
504 \bottomrule
505 \end{tabular}
506 \end{table}
507 
508 The finite shift pattern recovered by the experiment is
509 \[
510 \begin{pmatrix}
511 0&0&0&1\\
512 1&0&0&0\\
513 0&1&0&0\\
514 0&0&1&0
515 \end{pmatrix},
516 \]
517 which is the exact packet adjacency of a cyclic transfer among four phases.
518 
519 \subsection{Algorithms}
520 
521 The following finite constructions state mathematical specifications for the companion. Their Lean counterparts and exact scope are listed in the separate guide. They do not assert code extraction or a particular backend's performance.
522 
523 \begin{construction}[Closure specification for the orbit hull]
524 \label{con:orbit-hull-algorithm}
525 Let $V$ have finite dimension, let $(O_i)_{i\in I}$ be a finite operator
526 family, and let $S\subseteq V$.  Define
527 \[
528 W_0=\Span_{\bbk}S,
529 \qquad
530 W_{n+1}=W_n+\sum_{i\in I}O_i(W_n).
531 \]
532 Then there is an $n\in\N$ such that
533 \[
534 W_{n+1}=W_n
535 \qquad\text{and}\qquad
536 W_n=\Hull_{(O_i)}(S),
537 \]
538 where the right side is the least subspace containing $S$ and invariant under
539 every $O_i$.  Thus the ascending subspace iteration terminates and its stable
540 value is exactly the finite operator hull.
541 
542 Each strict enlargement increases dimension, so finite dimension prevents the iteration from continuing indefinitely. Equality at one step means that applying any declared operator keeps every vector in the current subspace. The stable subspace is therefore invariant, while every earlier step belongs to any invariant subspace that contains the seeds.
543 \end{construction}
544 
545 \begin{construction}[Table specification for transfer blocks]
546 \label{con:transfer-block-algorithm}
547 Given finite projector systems $(P_i)_{i\in I}$ and $(Q_j)_{j\in J}$ and a
548 linear map $T$, form the table
549 \[
550 B_{ji}=Q_jTP_i.
551 \]
552 Its assembly reconstructs the input map exactly,
553 \[
554 \sum_{j\in J}\sum_{i\in I}B_{ji}=T,
555 \]
556 and its reported support relation is exactly
557 $\{(i,j):B_{ji}\ne0\}$.  The latter equality is the specification of the
558 transfer graph output. It does not claim that Lean extracts a routine that decides the edge list for every coefficient field.
559 \end{construction}
560 
561 \begin{construction}[Exact graph seed rank from a certificate]
562 \label{con:exact-graph-seed-rank}
563 For a finite square matrix $A$ over a field $K$, define the noncomputable exact
564 spectral quantity
565 \[
566 r_{\mathrm{spec}}(A)
567 =
568 \max_{\mu\in\Spec_K(A)}
569 \dim_K\ker(A-\mu I),
570 \]
571 with value zero for an empty spectrum.  Suppose an exact certificate supplies
572 a finite eigenbasis indexed by labels and multiplicities, the eigenvalue
573 equations, a multiplicity bound attained by one label, projector polynomials
574 that extract the padded eigenbasis generators, coverage of every spectral
575 value by a label, equality of the declared and actual eigenspace dimensions,
576 and membership of the maximizing eigenvalue in the spectrum.  Then
577 $r_{\mathrm{spec}}(A)$ is the least natural number of seeds under polynomial orbits
578 for $A$.
579 
580 This is a verified certificate checker/specification.  It does not construct
581 the eigenbasis, prove that a symmetric matrix is diagonalizable, or implement
582 an exact eigensolver.  The companion Python code performs symbolic
583 computations in the reported finite graph range. The path and cycle
584 results for every size are proved separately above.
585 \end{construction}
586 
587 
588 \section{Reading guide: common confusions and diagnostic questions}
589 
590 \subsection{Common confusions}
591 \begin{center}
592 \begin{longtable}{@{}>{\raggedright\arraybackslash}p{0.26\textwidth}>{\raggedright\arraybackslash}p{0.68\textwidth}@{}}
593 \toprule
594 \textbf{Do not conflate} & \textbf{Correct distinction}\\
595 \midrule
596 \endhead
597 Grammar with realized algebra & The grammar may contain relations or words that act as zero.  Seed rank depends only on the image action.\\
598 Seed with basis vector & A seed is a generator under an algebra action.  One seed may generate a module with large dimension.\\
599 Cyclic vector with eigenvector & A cyclic vector must generate the whole module under operator words.  It is usually not an eigenvector.\\
600 Packet with orthogonal subspace & A packet is the range of an idempotent in a complete annihilating family.  Orthogonality is optional.\\
601 Exact reconstruction with good conditioning & Algebraic inverse identities may coexist with large analysis and synthesis norms.\\
602 Nonzero transfer edge with surjective transfer & A nonzero block can have small rank.  Graph reachability alone does not prove generation.\\
603 Seed rank for single packet seeds with unrestricted seed rank & Seeds supported in several packets may meet several source components simultaneously.\\
604 Continuous surjection with quotient isomorphism & The target topology must agree with the quotient topology.\\
605 Repeated notation with semantic realization & A true realization must preserve a declared collection of operations and identities.\\
606 \bottomrule
607 \end{longtable}
608 \end{center}
609 
610 \subsection{Diagnostic questions for a new application}
611 Before claiming that a new subject is a realization of Paper I, answer the following.
612 \begin{enumerate}
613 \item What is the fixed operator grammar or acting algebra?
614 \item What is the concrete realization space or module?
615 \item Which seeds are declared before the target is chosen?
616 \item Is generation algebraic, topological, probabilistic, or approximate?
617 \item What are the idempotent packets, and in what sense do they sum to the identity?
618 \item Are the packets finite, countable unconditional, or merely formal?
619 \item What are the transfer blocks, and which blocks are known to vanish?
620 \item Which morphisms preserve the packet system?
621 \item Which quotient, completion, tensor, or limit operations must be preserved?
622 \item What exact theorem from Paper I is being specialized, and what new domain theorem remains to be proved?
623 \end{enumerate}
624 
625 \subsection{Theorem spine at a glance}
626 \ConceptChain{
627 \(
628 \begin{array}{c}
629 \text{free seed presentation}\\[0.25em]
630 \Downarrow\\[-0.1em]
631 \text{minimal generator number}\\[0.25em]
632 \Downarrow\\[-0.1em]
633 \text{reduction modulo the Jacobson radical}\\[0.25em]
634 \Downarrow\\[-0.1em]
635 \text{semisimple or primary computation}
636 \end{array}
637 \qquad\qquad
638 \begin{array}{c}
639 \text{packet idempotents}\\[0.25em]
640 \Downarrow\\[-0.1em]
641 \text{exact analysis/synthesis}\\[0.25em]
642 \Downarrow\\[-0.1em]
643 \text{transfer block algebra}\\[0.25em]
644 \Downarrow\\[-0.1em]
645 \text{graphs, quotients, and realization}
646 \end{array}
647 \)
648 }
649 

Back to source controls

Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates