Realization Calculus

Download original file

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

Included manuscript sections

• visual_atlas.tex

Read the typeset paper

1 \section{Notation and convention ledger}
2 \begin{multicols}{2}
3 \begin{description}[style=nextline,font=\normalfont\bfseries]
4 \item[Address.] An operator word applied to a seed.
5 \item[Analysis.] The map sending an object to all packet coordinates.
6 \item[Block support.] The set of packet pairs \((\beta,\alpha)\) for which \(P_\beta TP_\alpha\neq0\).
7 \item[Collapsed realization.] The direct sum of all typed vertex spaces.
8 \item[Condensation graph.] The acyclic graph obtained by collapsing strongly connected components.
9 \item[Generated hull.] The submodule generated by a seed family, or its declared closure.
10 \item[Grammar.] A typed quiver and relation ideal describing legal operator words.
11 \item[Packet.] The range of one idempotent in a complete annihilating family.
12 \item[Packet pure.] Supported in at most one packet.
13 \item[Preservation profile.] The operations a realization functor is required to preserve.
14 \item[Realized algebra.] The image of the grammar algebra in the endomorphism algebra of a realization.
15 \item[Seed rank.] The smallest cardinality of a generating family. For a finite value, this is the minimum number of seeds.
16 \item[Source component.] A strongly connected component with no incoming edge in the condensation graph.
17 \item[Synthesis.] The map adding packet coordinates into the original object.
18 \item[Transfer block.] The map from one packet space to another obtained by sandwiching an operator between packet projectors.
19 \item[Transfer graph.] The directed graph formed from nonzero blocks of a declared algebra generating family.
20 \end{description}
21 \end{multicols}
22 
23 \begin{sectionrecap}[title={How to use the chapter after the first reading}]
24 For a concrete calculation, first reduce the action to the realized algebra.  Next compute or bound seed rank using quotients, the module top, or primary decomposition.  Then declare the packet system and use exact analysis and synthesis.  Finally move all operator equations into transfer blocks, where support, graph, quotient, and functorial constraints become explicit.
25 \end{sectionrecap}
26 
27 
28 \section{Proof dependency spine}
29 
30 \small
31 \begin{longtable}{@{}p{0.42\textwidth}p{0.52\textwidth}@{}}
32 \toprule
33 \textbf{Canonical record} & \textbf{Immediate proof dependencies}\\
34 \midrule
35 \endfirsthead
36 \toprule
37 \textbf{Canonical record} & \textbf{Immediate proof dependencies}\\
38 \midrule
39 \endhead
40 \texttt{PSC-I-T-TYPED-MODULE-EQUIVALENCE} & Typed grammar and path algebra action.\\
41 \texttt{PSC-I-T-FREE-PRESENTATION} & Seed evaluation map and first isomorphism theorem.\\
42 \texttt{PSC-I-T-COMPLETED-PRESENTATION} & Free presentation and uniqueness of completion.\\
43 \texttt{PSC-I-T-QUOTIENT-MONOTONICITY} & Intertwining identity and generated hull.\\
44 \texttt{PSC-I-T-EXACT-SEQUENCE-BOUNDS} & Quotient monotonicity and lifting generators.\\
45 \texttt{PSC-I-T-MODULE-TOP} & Nakayama lemma.\\
46 \texttt{PSC-I-T-SEMISIMPLE-SEED-RANK} & Module top theorem and regular module multiplicities.\\
47 \texttt{PSC-I-T-SINGLE-OPERATOR} & Primary decomposition, local formula, and product action.\\
48 \texttt{PSC-I-T-EXACT-PACKET-COORDINATES} & Complete finite idempotent family.\\
49 \texttt{PSC-I-T-COUNTABLE-}\newline\texttt{UNCONDITIONAL-PACKETS} & Completeness of the unconditional coordinate space.\\
50 \texttt{PSC-I-T-BLOCK-ALGEBRA} & Reconstruction and block multiplication.\\
51 \texttt{PSC-I-T-SUPPORT-PATTERN-ALGEBRA} & Block multiplication and rank one necessity tests.\\
52 \texttt{PSC-I-T-PREORDER-}\newline\texttt{ALGEBRA-DECOMPOSITION} & Preorder support criterion and finite chain nilpotence.\\
53 \texttt{PSC-I-T-ALGEBRA-}\newline\texttt{REACHABILITY-SUPPORT} & Generator word packet expansion.\\
54 \texttt{PSC-I-T-SOURCE-COMPONENT-SEED-RANK} & Reachability obstruction and edge surjective propagation.\\
55 \texttt{PSC-I-T-NATURALITY} & Intertwining and packet aggregation.\\
56 \texttt{PSC-I-T-PACKET-EXACT-SEQUENCE} & Invariant packet projectors and first isomorphism theorem.\\
57 \texttt{PSC-I-T-DENSE-REALIZATION} & Continuity and naturality of hulls.\\
58 \texttt{PSC-I-T-REALIZATION-EXPORT} & Additive functor axioms and preserved universal constructions.\\
59 \bottomrule
60 \end{longtable}
61 \normalsize
62 
63 \clearpage\section{Conclusions and further use}
64 
65 The results establish the following tools for working with a declared operator action and packet system:
66 \begin{enumerate}[label=\textbf{I.\arabic*.},leftmargin=*,itemsep=0.3em,topsep=0.4em]
67 \item The two sided annihilator criterion is proved in \cref{prop:two-sided-annihilator}.
68 \item Generator detection modulo the Jacobson radical is proved in \cref{thm:module-top}.
69 \item The semisimple seed rank formula applies over arbitrary division rings, with the conventions for left and right modules kept explicit in \cref{thm:semisimple-seed-rank}.
70 \item The single operator formula and its cyclic criteria apply over arbitrary fields in \cref{thm:single-operator,cor:cyclic-matrix}.
71 \item The countable unconditional packet theorem is proved in \cref{thm:countable-packets}.
72 \item The classification of support compatible with $*$ is proved in \cref{cor:star-support}.
73 \item The weighted source component formula gives the packet pure generation requirement under the propagation hypotheses in \cref{thm:source-component-rank}.
74 \item Seed system composition, packet exact sequences, quotient block descent, dense realization, quotient completion, and semantic theorem transport are proved in \cref{prop:seed-category,thm:packet-exact-sequence,cor:block-descent,thm:dense-realization,thm:quotient-topology,thm:realization-export}.
75 \item Exact sequence bounds, monotonicity under enlargement of the acting algebra, coordinate stability, projection onto diagonal blocks, and preorder decomposition are established in \cref{thm:exact-sequence-bounds,prop:acting-algebra-monotonicity,prop:conditioned-coordinates,prop:block-diagonal-projection,thm:preorder-decomposition}.
76 \end{enumerate}
77 
78 \clearpage\appendix
79 \section{Stable statement concordance}\label{app:stable-concordance}
80 These identifiers preserve the expanded foundation's namespace of 108 records. The display numbers refer to Chapter I. The identifiers track mathematical statements, and their count does not measure how many theorems have been verified in Lean. Statements in the worked models retain their source labels and are mapped separately by the Lean guide.
81 \small\begin{longtable}{@{}p{.44\textwidth}p{.07\textwidth}p{.41\textwidth}@{}}
82 \toprule Stable identifier & No. & Statement\\\midrule\endhead
83 \nolinkurl{PSC-I-D-COEFFICIENT-REGIME} & \ref{def:coefficient-regime} & Coefficient and module regimes \\
84 \nolinkurl{PSC-I-D-THEOREM-RECORD} & \ref{def:theorem-record} & Canonical theorem record \\
85 \nolinkurl{PSC-I-B-SYMBOLIC-SCOPE} & \ref{bnd:symbolic-scope} & Symbolic scope \\
86 \nolinkurl{PSC-I-D-TYPED-GRAMMAR} & \ref{def:typed-grammar} & Typed operator grammar \\
87 \nolinkurl{PSC-I-D-COLLAPSED-REALIZATION} & \ref{def:collapsed-realization} & Collapsed one space realization \\
88 \nolinkurl{PSC-I-T-TYPED-MODULE-EQUIVALENCE} & \ref{thm:typed-module-equivalence} & Typed realization and module equivalence \\
89 \nolinkurl{PSC-I-D-REALIZED-ALGEBRA} & \ref{def:realized-algebra} & Realized operator algebra \\
90 \nolinkurl{PSC-I-P-ACTION-FACTORIZATION} & \ref{prop:action-factorization} & Action factorization and hull invariance \\
91 \nolinkurl{PSC-I-D-SEED-SYSTEM} & \ref{def:seed-system} & Linear seed system \\
92 \nolinkurl{PSC-I-D-GENERATED-HULL} & \ref{def:generated-hull} & Generated hull \\
93 \nolinkurl{PSC-I-D-NATURAL-PRESENTATION} & \ref{def:natural-presentation} & Natural presentation \\
94 \nolinkurl{PSC-I-P-ALGEBRA-MODULE-GENERATION} & \ref{prop:algebra-module-generation} & Algebra generation and module generation are distinct \\
95 \nolinkurl{PSC-I-B-TARGET-DEPENDENT-OPERATORS} & \ref{bnd:target-dependent-operators} & Target dependent operators \\
96 \nolinkurl{PSC-I-D-SEED-EVALUATION} & \ref{def:seed-evaluation} & Seed evaluation map \\
97 \nolinkurl{PSC-I-T-FREE-PRESENTATION} & \ref{thm:free-presentation} & Finite free presentation \\
98 \nolinkurl{PSC-I-C-MINIMAL-FREE-COVER} & \ref{cor:minimal-free-cover} & Minimal free cover characterization \\
99 \nolinkurl{PSC-I-C-ONE-SEED-PRESENTATION} & \ref{cor:one-seed-presentation} & One seed presentation \\
100 \nolinkurl{PSC-I-P-ANNIHILATOR-TWO-SIDED} & \ref{prop:two-sided-annihilator} & Two sided annihilator criterion \\
101 \nolinkurl{PSC-I-T-COMPLETED-PRESENTATION} & \ref{thm:completed-presentation} & Completion of a dense free presentation \\
102 \nolinkurl{PSC-I-D-SEED-RANK} & \ref{def:seed-rank} & Seed rank \\
103 \nolinkurl{PSC-I-P-CYCLIC-CHARACTERIZATION} & \ref{prop:cyclic-characterization} & Cyclic characterization \\
104 \nolinkurl{PSC-I-P-ACTING-ALGEBRA-MONOTONICITY} & \ref{prop:acting-algebra-monotonicity} & Monotonicity under enlargement of the acting algebra \\
105 \nolinkurl{PSC-I-T-QUOTIENT-MONOTONICITY} & \ref{thm:quotient-monotonicity} & Quotient monotonicity \\
106 \nolinkurl{PSC-I-C-ISOMORPHISM-INVARIANCE} & \ref{cor:isomorphism-invariance} & Isomorphism invariance \\
107 \nolinkurl{PSC-I-T-EXACT-SEQUENCE-BOUNDS} & \ref{thm:exact-sequence-bounds} & Short exact sequence bounds \\
108 \nolinkurl{PSC-I-P-SHARED-DIRECT-SUM} & \ref{prop:shared-direct-sum} & Shared direct sum bounds \\
109 \nolinkurl{PSC-I-T-INDEPENDENT-DIRECT-SUM} & \ref{thm:independent-direct-sum} & Independent direct sum formula \\
110 \nolinkurl{PSC-I-P-TENSOR-BOUND} & \ref{prop:tensor-bound} & Tensor product bound \\
111 \nolinkurl{PSC-I-B-TENSOR-NONEQUALITY} & \ref{bnd:tensor-nonequality} & Tensor rank is not generally multiplicative \\
112 \nolinkurl{PSC-I-P-SCALAR-EXTENSION-MONOTONICITY} & \ref{prop:scalar-extension} & Scalar extension monotonicity \\
113 \nolinkurl{PSC-I-D-SEED-RANK-WITNESS} & \ref{def:seed-rank-witness} & Seed rank witness \\
114 \nolinkurl{PSC-I-P-SCALAR-QUOTIENT-WITNESS} & \ref{prop:scalar-quotient} & Scalar quotient witness \\
115 \nolinkurl{PSC-I-CI-NAKAYAMA} & \ref{ci:nakayama} & Nakayama lemma \\
116 \nolinkurl{PSC-I-T-MODULE-TOP} & \ref{thm:module-top} & Generator number is detected modulo the Jacobson radical \\
117 \nolinkurl{PSC-I-C-LOCAL-ALGEBRA-FORMULA} & \ref{cor:local-algebra-formula} & Local algebra formula \\
118 \nolinkurl{PSC-I-CI-WEDDERBURN-ARTIN} & \ref{ci:wedderburn} & Wedderburn and Artin decomposition \\
119 \nolinkurl{PSC-I-L-REGULAR-MODULE-MULTIPLICITIES} & \ref{lem:regular-multiplicities} & Regular module multiplicities \\
120 \nolinkurl{PSC-I-T-SEMISIMPLE-SEED-RANK} & \ref{thm:semisimple-seed-rank} & Semisimple seed rank formula over arbitrary division rings \\
121 \nolinkurl{PSC-I-C-ALGEBRAICALLY-CLOSED-FORMULA} & \ref{cor:algebraically-closed-formula} & Algebraically closed multiplicity formula \\
122 \nolinkurl{PSC-I-C-FULL-MATRIX} & \ref{cor:full-matrix} & Full matrix algebra \\
123 \nolinkurl{PSC-I-C-MULTIPLICITY-OBSTRUCTION} & \ref{cor:multiplicity-obstruction} & Multiplicity obstruction \\
124 \nolinkurl{PSC-I-CI-PID-PRIMARY-DECOMPOSITION} & \ref{ci:primary-decomposition} & Primary decomposition for polynomial modules \\
125 \nolinkurl{PSC-I-T-SINGLE-OPERATOR} & \ref{thm:single-operator} & Single operator seed rank \\
126 \nolinkurl{PSC-I-C-INVARIANT-FACTOR-COUNT} & \ref{cor:invariant-factor-count} & Invariant factor count \\
127 \nolinkurl{PSC-I-C-ALGEBRAICALLY-CLOSED-SINGLE-OPERATOR} & \ref{cor:geometric-multiplicity} & Geometric multiplicity formula \\
128 \nolinkurl{PSC-I-C-CYCLIC-MATRIX} & \ref{cor:cyclic-matrix} & Cyclic matrix criterion \\
129 \nolinkurl{PSC-I-D-PACKET-SYSTEM} & \ref{def:packet-system} & Finite packet system \\
130 \nolinkurl{PSC-I-D-PACKET-SUPPORT} & \ref{def:packet-support} & Packet support and packet pure vectors \\
131 \nolinkurl{PSC-I-L-PACKET-AGGREGATION} & \ref{lem:packet-aggregation} & Finite packet aggregation \\
132 \nolinkurl{PSC-I-D-ANALYSIS-SYNTHESIS} & \ref{def:analysis-synthesis} & Packet analysis and synthesis \\
133 \nolinkurl{PSC-I-T-EXACT-PACKET-COORDINATES} & \ref{thm:exact-packet-coordinates} & Exact packet coordinate isomorphism \\
134 \nolinkurl{PSC-I-C-PACKETWISE-EQUALITY} & \ref{cor:packetwise-equality} & Packetwise equality \\
135 \nolinkurl{PSC-I-C-PACKET-UNIVERSAL-PROPERTY} & \ref{cor:packet-universal-property} & Universal mapping property of finite packet coordinates \\
136 \nolinkurl{PSC-I-T-TENSOR-PACKET-SYSTEM} & \ref{thm:tensor-packet-system} & Tensor product packet systems \\
137 \nolinkurl{PSC-I-P-DUAL-PACKET-SYSTEM} & \ref{prop:dual-packet-system} & Dual packet systems \\
138 \nolinkurl{PSC-I-T-BANACH-PACKET-ISOMORPHISM} & \ref{thm:banach-packets} & Finite Banach packet isomorphism \\
139 \nolinkurl{PSC-I-D-PACKET-CONDITION-NUMBER} & \ref{def:packet-condition-number} & Packet coordinate condition number \\
140 \nolinkurl{PSC-I-P-CONDITIONED-COORDINATES} & \ref{prop:conditioned-coordinates} & Conditioned coordinate transport \\
141 \nolinkurl{PSC-I-C-COMPLETION-PACKET-SPLIT} & \ref{cor:completion-packet-split} & Completion preserves a finite packet split \\
142 \nolinkurl{PSC-I-D-UNCONDITIONAL-PACKET-SPACE} & \ref{def:unconditional-packet-space} & Unconditional packet sum space \\
143 \nolinkurl{PSC-I-L-UNCONDITIONAL-COMPLETENESS} & \ref{lem:unconditional-completeness} & Completeness of the unconditional packet sum \\
144 \nolinkurl{PSC-I-T-COUNTABLE-UNCONDITIONAL-PACKETS} & \ref{thm:countable-packets} & Countable unconditional packet isomorphism \\
145 \nolinkurl{PSC-I-R-UNIFORM-BOUNDEDNESS} & \ref{rem:uniform-boundedness} & Uniform boundedness \\
146 \nolinkurl{PSC-I-B-INFINITE-PACKET-TOPOLOGY} & \ref{bnd:infinite-packet-topology} & Infinite packet sums \\
147 \nolinkurl{PSC-I-D-TRANSFER-BLOCK} & \ref{def:transfer-block} & Transfer block \\
148 \nolinkurl{PSC-I-T-OPERATOR-RECONSTRUCTION} & \ref{thm:operator-reconstruction} & Exact operator reconstruction \\
149 \nolinkurl{PSC-I-T-BLOCK-MULTIPLICATION} & \ref{thm:block-multiplication} & Packet matrix multiplication \\
150 \nolinkurl{PSC-I-C-BLOCK-POWERS} & \ref{cor:block-powers} & Packet powers and paths \\
151 \nolinkurl{PSC-I-C-ADJOINT-REVERSAL} & \ref{cor:adjoint-reversal} & Adjoint reversal \\
152 \nolinkurl{PSC-I-C-TENSOR-TRANSFER-BLOCKS} & \ref{cor:tensor-transfer-blocks} & Tensor product transfer blocks \\
153 \nolinkurl{PSC-I-T-BLOCK-INTERTWINING} & \ref{thm:block-intertwining} & Blockwise intertwining equations \\
154 \nolinkurl{PSC-I-T-BLOCK-ALGEBRA} & \ref{thm:block-algebra} & Full block algebra representation \\
155 \nolinkurl{PSC-I-C-PACKET-SUPPORT-PROPAGATION} & \ref{cor:packet-support-propagation} & Propagation of packet support \\
156 \nolinkurl{PSC-I-C-DIMENSION-COUNT} & \ref{cor:dimension-count} & Dimension count \\
157 \nolinkurl{PSC-I-P-BLOCK-DIAGONAL-COMMUTANT} & \ref{prop:block-diagonal-projection} & Block diagonal projection and packet commutant \\
158 \nolinkurl{PSC-I-D-SUPPORT-RELATION} & \ref{def:support-relation} & Support relation and support space \\
159 \nolinkurl{PSC-I-T-SUPPORT-PATTERN-ALGEBRA} & \ref{thm:support-pattern} & Support pattern algebra criterion \\
160 \nolinkurl{PSC-I-C-SUPPORT-PATTERN-STAR} & \ref{cor:star-support} & Bounded support patterns closed under $*$ \\
161 \nolinkurl{PSC-I-T-PREORDER-ALGEBRA-DECOMPOSITION} & \ref{thm:preorder-decomposition} & Preorder support algebra decomposition \\
162 \nolinkurl{PSC-I-D-TRANSFER-GRAPH} & \ref{def:transfer-graph} & Transfer graph of an algebra generating family \\
163 \nolinkurl{PSC-I-T-ALGEBRA-REACHABILITY-SUPPORT} & \ref{thm:algebra-reachability-support} & Reachability support of the generated algebra \\
164 \nolinkurl{PSC-I-P-REACHABILITY-OBSTRUCTION} & \ref{prop:reachability-obstruction} & Reachability obstruction for generated hulls \\
165 \nolinkurl{PSC-I-D-DIRECTED-SEED-RANK} & \ref{def:directed-seed-rank} & Packet pure seed rank \\
166 \nolinkurl{PSC-I-P-PACKET-PURE-RANK-BOUNDS} & \ref{prop:packet-pure-rank-bounds} & Basic packet pure rank bounds \\
167 \nolinkurl{PSC-I-D-EDGE-SURJECTIVE} & \ref{def:edge-surjective} & Edge surjective packet system \\
168 \nolinkurl{PSC-I-T-SOURCE-COMPONENT-SEED-RANK} & \ref{thm:source-component-rank} & Source component formula for packet pure seed rank \\
169 \nolinkurl{PSC-I-D-PACKET-PROPAGATING} & \ref{def:packet-propagating} & Packet propagating system \\
170 \nolinkurl{PSC-I-C-SOURCE-COMPONENT-COUNT} & \ref{cor:source-component-count} & Unweighted source component count \\
171 \nolinkurl{PSC-I-B-PACKET-PURE-BOUNDARY} & \ref{bnd:packet-pure-boundary} & Mixed support seeds can merge source requirements \\
172 \nolinkurl{PSC-I-T-COORDINATE-TRANSPORT} & \ref{thm:coordinate-transport} & Coordinate transport \\
173 \nolinkurl{PSC-I-D-PACKET-MORPHISM} & \ref{def:packet-morphism} & Packet compatible operator morphism \\
174 \nolinkurl{PSC-I-D-SEED-MORPHISM} & \ref{def:seed-morphism} & Morphism of seeded systems \\
175 \nolinkurl{PSC-I-T-NATURALITY} & \ref{thm:naturality} & Naturality of generated hulls and transfer blocks \\
176 \nolinkurl{PSC-I-P-SEED-SYSTEM-CATEGORY} & \ref{prop:seed-category} & Category of seeded packet systems \\
177 \nolinkurl{PSC-I-T-PACKET-EXACT-SEQUENCE} & \ref{thm:packet-exact-sequence} & Packet exact sequence for an invariant subspace \\
178 \nolinkurl{PSC-I-T-QUOTIENT-PACKET-DESCENT} & \ref{thm:quotient-packet-descent} & Packet descent through an invariant quotient \\
179 \nolinkurl{PSC-I-C-QUOTIENT-PACKET-DESCENT} & \ref{cor:block-descent} & Restriction and quotient of transfer blocks \\
180 \nolinkurl{PSC-I-C-TOPOLOGICAL-PACKET-EXACT-SEQUENCE} & \ref{cor:topological-packet-exact-sequence} & Topological packet exact sequence \\
181 \nolinkurl{PSC-I-T-DENSE-REALIZATION} & \ref{thm:dense-realization} & Dense realization theorem \\
182 \nolinkurl{PSC-I-T-QUOTIENT-TOPOLOGY-COMPLETION} & \ref{thm:quotient-topology} & Quotient topology and completed realization \\
183 \nolinkurl{PSC-I-B-TOPOLOGICAL-QUOTIENT} & \ref{bnd:topological-quotient} & Continuous surjections and quotient topology \\
184 \nolinkurl{PSC-I-D-REALIZATION-FUNCTOR} & \ref{def:realization-functor} & Realization functor and preservation profile \\
185 \nolinkurl{PSC-I-T-REALIZATION-EXPORT} & \ref{thm:realization-export} & Equational realization principle \\
186 \nolinkurl{PSC-I-P-REALIZATION-EXPORT} & \ref{prop:realization-export} & Realization export principle \\
187 \nolinkurl{PSC-I-D-SEMANTIC-REALIZATION} & \ref{def:semantic-realization} & Semantic realization criterion \\
188 \nolinkurl{PSC-I-ALG-EXAMPLE-SLOTS} & \ref{def:reserved-example-slots} & Worked realization interface \\
189 \nolinkurl{PSC-I-EXPORT} & \ref{def:paper-one-export} & Chapter I export object \\
190 \nolinkurl{PSC-I-B-FINAL-CLAIM-BOUNDARY} & \ref{bnd:final-claim-boundary} & Exact limits of Chapter I \\
191 \bottomrule\end{longtable}\normalsize
192 \clearpage\section{Visual atlas}\label{app:visual-atlas}
193 The following twenty-two plates present exact finite models, explanatory diagrams, and one analytic density example. Each plate follows a calculation, identity, or obstruction from the main text. All graphics are generated from mathematical source, and the cross-references refer to the mathematical text.
194 
195 \medskip
196 \begin{longtable}{@{}p{.08\textwidth}p{.82\textwidth}@{}}
197 \toprule Plate & Route through the examples\\\midrule\endhead
198 1, 2 & Fixed grammars, seed power, and the objects of the calculus.\\
199 3, 4 & Two linked chains and a quotient proving the minimum seed count.\\
200 5, 6 & Left ideal relations and typed reachability with a missing direction.\\
201 7, 8 & Oblique exact coordinates and complete transfer block multiplication.\\
202 9, 10 & Cancellation along paths and the algebra of admissible zero patterns.\\
203 11, 12 & Coordinate transport, shared action, and independent control.\\
204 13, 14 & Semisimple multiplicity budgets and primary extraction polynomials.\\
205 15, 16 & Path endpoints and the cycle's two dimensional quotient obstruction.\\
206 17 & A coordinate ring relation as a two packet product rule.\\
207 18, 19 & Dense shift generation, residue coordinates, and address carry.\\
208 20, 21 & Exact orbit hull stabilization and all tensor cross terms.\\
209 22 & The scope of mathematical, formal, and computational evidence.\\
210 \bottomrule\end{longtable}
211 
212 The seed examples can be read consecutively. The packet and graph plates also provide entry points for readers interested in coordinates or propagation. The displayed matrices are exact. Numerical illustrations in the earlier figures retain their explicitly stated finite ranges. Each diagram is accompanied by the equation or obstruction it represents, so it can be read alongside the relevant proof.
213 \begingroup\fontsize{9.9}{11.2}\selectfont\setstretch{1.0}\setlength{\parindent}{0pt}\setlength{\parskip}{2pt}\setlength{\abovedisplayskip}{7pt}\setlength{\belowdisplayskip}{7pt}\input{visual_atlas.tex}\endgroup
214 
215 \clearpage
216 \begin{thebibliography}{99}
217 
218 \bibitem{assemSimsonSkowronski2006}
219 I.~Assem, D.~Simson, and A.~Skowro{\'n}ski,
220 \emph{Elements of the Representation Theory of Associative Algebras, Volume 1: Techniques of Representation Theory},
221 London Mathematical Society Student Texts 65,
222 Cambridge University Press, Cambridge, 2006.
223 \href{https://doi.org/10.1017/CBO9780511614309}{doi:10.1017/CBO9780511614309}.
224 
225 \bibitem{brouwerHaemers2012}
226 A.~E.~Brouwer and W.~H.~Haemers,
227 \emph{Spectra of Graphs},
228 Universitext, Springer, New York, 2012.
229 \href{https://doi.org/10.1007/978-1-4614-1939-6}{doi:10.1007/978-1-4614-1939-6}.
230 
231 \bibitem{conway1990}
232 J.~B.~Conway,
233 \emph{A Course in Functional Analysis},
234 second edition, Graduate Texts in Mathematics 96,
235 Springer, New York, 1990.
236 \href{https://doi.org/10.1007/978-1-4757-4383-8}{doi:10.1007/978-1-4757-4383-8}.
237 
238 \bibitem{hornJohnson2012}
239 R.~A.~Horn and C.~R.~Johnson,
240 \emph{Matrix Analysis},
241 second edition, Cambridge University Press, Cambridge, 2012.
242 \href{https://doi.org/10.1017/CBO9781139020411}{doi:10.1017/CBO9781139020411}.
243 
244 \bibitem{lam2001noncommutative}
245 T.~Y.~Lam,
246 \emph{A First Course in Noncommutative Rings},
247 second edition, Graduate Texts in Mathematics 131,
248 Springer, New York, 2001.
249 \href{https://doi.org/10.1007/978-1-4419-8616-0}{doi:10.1007/978-1-4419-8616-0}.
250 
251 \bibitem{lam1999modules}
252 T.~Y.~Lam,
253 \emph{Lectures on Modules and Rings},
254 Graduate Texts in Mathematics 189,
255 Springer, New York, 1999.
256 \href{https://doi.org/10.1007/978-1-4612-0525-8}{doi:10.1007/978-1-4612-0525-8}.
257 
258 \bibitem{roman2008}
259 S.~Roman,
260 \emph{Advanced Linear Algebra},
261 third edition, Graduate Texts in Mathematics 135,
262 Springer, New York, 2008.
263 \href{https://doi.org/10.1007/978-0-387-72831-5}{doi:10.1007/978-0-387-72831-5}.
264 
265 \bibitem{schaeferWolff1999}
266 H.~H.~Schaefer and M.~P.~Wolff,
267 \emph{Topological Vector Spaces},
268 second edition, Graduate Texts in Mathematics 3,
269 Springer, New York, 1999.
270 \href{https://doi.org/10.1007/978-1-4612-1468-7}{doi:10.1007/978-1-4612-1468-7}.
271 
272 \bibitem{silverman2009}
273 J.~H.~Silverman,
274 \emph{The Arithmetic of Elliptic Curves},
275 second edition, Graduate Texts in Mathematics 106,
276 Springer, New York, 2009.
277 \href{https://doi.org/10.1007/978-0-387-09494-6}{doi:10.1007/978-0-387-09494-6}.
278 
279 
280 \bibitem{demouraUllrich2021}
281 L. de Moura and S. Ullrich,
282 \emph{The Lean 4 Theorem Prover and Programming Language},
283 in Automated Deduction---CADE 28, Lecture Notes in Computer Science 12699,
284 Springer, Cham, 2021, pp. 625--635.
285 \href{https://doi.org/10.1007/978-3-030-79876-5_37}{doi:10.1007/978-3-030-79876-5\_37}.
286 
287 \bibitem{mathlib2020}
288 The mathlib Community,
289 \emph{The Lean Mathematical Library},
290 in Proceedings of the 9th ACM SIGPLAN International Conference on Certified
291 Programs and Proofs, ACM, 2020, pp. 367--381.
292 \href{https://doi.org/10.1145/3372885.3373824}{doi:10.1145/3372885.3373824}.
293 
294 \end{thebibliography}

Back to source controls

Back to Realization Calculus