21 Notation and convention ledger
On this page · Permalink · Source line 1
- Address.
An operator word applied to a seed.
- Analysis.
The map sending an object to all packet coordinates.
- Block support.
The set of packet pairs \((\beta,\alpha)\) for which \(P_\beta TP_\alpha\neq0\).
- Collapsed realization.
The direct sum of all typed vertex spaces.
- Condensation graph.
The acyclic graph obtained by collapsing strongly connected components.
- Generated hull.
The submodule generated by a seed family, or its declared closure.
- Grammar.
A typed quiver and relation ideal describing legal operator words.
- Packet.
The range of one idempotent in a complete annihilating family.
- Packet pure.
Supported in at most one packet.
- Preservation profile.
The operations a realization functor is required to preserve.
- Realized algebra.
The image of the grammar algebra in the endomorphism algebra of a realization.
- Seed rank.
The smallest cardinality of a generating family. For a finite value, this is the minimum number of seeds.
- Source component.
A strongly connected component with no incoming edge in the condensation graph.
- Synthesis.
The map adding packet coordinates into the original object.
- Transfer block.
The map from one packet space to another obtained by sandwiching an operator between packet projectors.
- Transfer graph.
The directed graph formed from nonzero blocks of a declared algebra generating family.
How to use the paper after the first reading
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.
22 Proof dependency spine
On this page · Visual guide: What the pictures certify · Permalink · Source line 28
| Canonical record | Immediate proof dependencies |
|---|---|
PSC-I-T-TYPED-MODULE-EQUIVALENCE | Typed grammar and path algebra action. |
PSC-I-T-FREE-PRESENTATION | Seed evaluation map and first isomorphism theorem. |
PSC-I-T-COMPLETED-PRESENTATION | Free presentation and uniqueness of completion. |
PSC-I-T-QUOTIENT-MONOTONICITY | Intertwining identity and generated hull. |
PSC-I-T-EXACT-SEQUENCE-BOUNDS | Quotient monotonicity and lifting generators. |
PSC-I-T-MODULE-TOP | Nakayama lemma. |
PSC-I-T-SEMISIMPLE-SEED-RANK | Module top theorem and regular module multiplicities. |
PSC-I-T-SINGLE-OPERATOR | Primary decomposition, local formula, and product action. |
PSC-I-T-EXACT-PACKET-COORDINATES | Complete finite idempotent family. |
PSC-I-T-COUNTABLE-UNCONDITIONAL-PACKETS | Completeness of the unconditional coordinate space. |
PSC-I-T-BLOCK-ALGEBRA | Reconstruction and block multiplication. |
PSC-I-T-SUPPORT-PATTERN-ALGEBRA | Block multiplication and rank one necessity tests. |
PSC-I-T-PREORDER-ALGEBRA-DECOMPOSITION | Preorder support criterion and finite chain nilpotence. |
PSC-I-T-ALGEBRA-REACHABILITY-SUPPORT | Generator word packet expansion. |
PSC-I-T-SOURCE-COMPONENT-SEED-RANK | Reachability obstruction and edge surjective propagation. |
PSC-I-T-NATURALITY | Intertwining and packet aggregation. |
PSC-I-T-PACKET-EXACT-SEQUENCE | Invariant packet projectors and first isomorphism theorem. |
PSC-I-T-DENSE-REALIZATION | Continuity and naturality of hulls. |
PSC-I-T-REALIZATION-EXPORT | Additive functor axioms and preserved universal constructions. |
23 Conclusions and further use
On this page · Permalink · Source line 63
The results establish the following tools for working with a declared operator action and packet system:
- I.1.
The two sided annihilator criterion is proved in Proposition 3.5.
- I.2.
Generator detection modulo the Jacobson radical is proved in Theorem 5.2.
- I.3.
The semisimple seed rank formula applies over arbitrary division rings, with the conventions for left and right modules kept explicit in Theorem 5.6.
- I.4.
The single operator formula and its cyclic criteria apply over arbitrary fields in Theorem 6.2 and Corollary 6.5.
- I.5.
The countable unconditional packet theorem is proved in Theorem 7.16.
- I.6.
The classification of support compatible with \(*\) is proved in Corollary 8.14.
- I.7.
The weighted source component formula gives the packet pure generation requirement under the propagation hypotheses in Theorem 9.7.
- I.8.
Seed system composition, packet exact sequences, quotient block descent, dense realization, quotient completion, and semantic theorem transport are proved in Proposition 10.5, Theorem 10.6, Corollary 10.8, Theorem 10.10, Theorem 10.11, and Theorem 11.2.
- I.9.
Exact sequence bounds, monotonicity under enlargement of the acting algebra, coordinate stability, projection onto diagonal blocks, and preorder decomposition are established in Theorem 4.6, Proposition 4.3, Proposition 7.12, Proposition 8.11, and Theorem 8.15.
A Stable statement concordance
On this page · Visual guide: What the pictures certify · Permalink · Source line 79
These identifiers preserve the expanded foundation's namespace of 108 records. The display numbers refer to this edition. 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.
| Stable identifier | No. | Statement |
|---|---|---|
PSC-I-D-COEFFICIENT-REGIME | Definition 1.1 | Coefficient and module regimes |
PSC-I-D-THEOREM-RECORD | Definition 1.2 | Canonical theorem record |
PSC-I-B-SYMBOLIC-SCOPE | Boundary 1.3 | Symbolic scope |
PSC-I-D-TYPED-GRAMMAR | Definition 2.1 | Typed operator grammar |
PSC-I-D-COLLAPSED-REALIZATION | Definition 2.2 | Collapsed one space realization |
PSC-I-T-TYPED-MODULE-EQUIVALENCE | Theorem 2.3 | Typed realization and module equivalence |
PSC-I-D-REALIZED-ALGEBRA | Definition 2.4 | Realized operator algebra |
PSC-I-P-ACTION-FACTORIZATION | Proposition 2.5 | Action factorization and hull invariance |
PSC-I-D-SEED-SYSTEM | Definition 2.6 | Linear seed system |
PSC-I-D-GENERATED-HULL | Definition 2.7 | Generated hull |
PSC-I-D-NATURAL-PRESENTATION | Definition 2.8 | Natural presentation |
PSC-I-P-ALGEBRA-MODULE-GENERATION | Proposition 2.9 | Algebra generation and module generation are distinct |
PSC-I-B-TARGET-DEPENDENT-OPERATORS | Boundary 2.10 | Target dependent operators |
PSC-I-D-SEED-EVALUATION | Definition 3.1 | Seed evaluation map |
PSC-I-T-FREE-PRESENTATION | Theorem 3.2 | Finite free presentation |
PSC-I-C-MINIMAL-FREE-COVER | Corollary 3.3 | Minimal free cover characterization |
PSC-I-C-ONE-SEED-PRESENTATION | Corollary 3.4 | One seed presentation |
PSC-I-P-ANNIHILATOR-TWO-SIDED | Proposition 3.5 | Two sided annihilator criterion |
PSC-I-T-COMPLETED-PRESENTATION | Theorem 3.6 | Completion of a dense free presentation |
PSC-I-D-SEED-RANK | Definition 4.1 | Seed rank |
PSC-I-P-CYCLIC-CHARACTERIZATION | Proposition 4.2 | Cyclic characterization |
PSC-I-P-ACTING-ALGEBRA-MONOTONICITY | Proposition 4.3 | Monotonicity under enlargement of the acting algebra |
PSC-I-T-QUOTIENT-MONOTONICITY | Theorem 4.4 | Quotient monotonicity |
PSC-I-C-ISOMORPHISM-INVARIANCE | Corollary 4.5 | Isomorphism invariance |
PSC-I-T-EXACT-SEQUENCE-BOUNDS | Theorem 4.6 | Short exact sequence bounds |
PSC-I-P-SHARED-DIRECT-SUM | Proposition 4.7 | Shared direct sum bounds |
PSC-I-T-INDEPENDENT-DIRECT-SUM | Theorem 4.8 | Independent direct sum formula |
PSC-I-P-TENSOR-BOUND | Proposition 4.9 | Tensor product bound |
PSC-I-B-TENSOR-NONEQUALITY | Boundary 4.10 | Tensor rank is not generally multiplicative |
PSC-I-P-SCALAR-EXTENSION-MONOTONICITY | Proposition 4.11 | Scalar extension monotonicity |
PSC-I-D-SEED-RANK-WITNESS | Definition 4.12 | Seed rank witness |
PSC-I-P-SCALAR-QUOTIENT-WITNESS | Proposition 4.13 | Scalar quotient witness |
PSC-I-CI-NAKAYAMA | Classical input 5.1 | Nakayama lemma |
PSC-I-T-MODULE-TOP | Theorem 5.2 | Generator number is detected modulo the Jacobson radical |
PSC-I-C-LOCAL-ALGEBRA-FORMULA | Corollary 5.3 | Local algebra formula |
PSC-I-CI-WEDDERBURN-ARTIN | Classical input 5.4 | Wedderburn and Artin decomposition |
PSC-I-L-REGULAR-MODULE-MULTIPLICITIES | Lemma 5.5 | Regular module multiplicities |
PSC-I-T-SEMISIMPLE-SEED-RANK | Theorem 5.6 | Semisimple seed rank formula over arbitrary division rings |
PSC-I-C-ALGEBRAICALLY-CLOSED-FORMULA | Corollary 5.7 | Algebraically closed multiplicity formula |
PSC-I-C-FULL-MATRIX | Corollary 5.8 | Full matrix algebra |
PSC-I-C-MULTIPLICITY-OBSTRUCTION | Corollary 5.9 | Multiplicity obstruction |
PSC-I-CI-PID-PRIMARY-DECOMPOSITION | Classical input 6.1 | Primary decomposition for polynomial modules |
PSC-I-T-SINGLE-OPERATOR | Theorem 6.2 | Single operator seed rank |
PSC-I-C-INVARIANT-FACTOR-COUNT | Corollary 6.3 | Invariant factor count |
PSC-I-C-ALGEBRAICALLY-CLOSED-SINGLE-OPERATOR | Corollary 6.4 | Geometric multiplicity formula |
PSC-I-C-CYCLIC-MATRIX | Corollary 6.5 | Cyclic matrix criterion |
PSC-I-D-PACKET-SYSTEM | Definition 7.1 | Finite packet system |
PSC-I-D-PACKET-SUPPORT | Definition 7.2 | Packet support and packet pure vectors |
PSC-I-L-PACKET-AGGREGATION | Lemma 7.3 | Finite packet aggregation |
PSC-I-D-ANALYSIS-SYNTHESIS | Definition 7.4 | Packet analysis and synthesis |
PSC-I-T-EXACT-PACKET-COORDINATES | Theorem 7.5 | Exact packet coordinate isomorphism |
PSC-I-C-PACKETWISE-EQUALITY | Corollary 7.6 | Packetwise equality |
PSC-I-C-PACKET-UNIVERSAL-PROPERTY | Corollary 7.7 | Universal mapping property of finite packet coordinates |
PSC-I-T-TENSOR-PACKET-SYSTEM | Theorem 7.8 | Tensor product packet systems |
PSC-I-P-DUAL-PACKET-SYSTEM | Proposition 7.9 | Dual packet systems |
PSC-I-T-BANACH-PACKET-ISOMORPHISM | Theorem 7.10 | Finite Banach packet isomorphism |
PSC-I-D-PACKET-CONDITION-NUMBER | Definition 7.11 | Packet coordinate condition number |
PSC-I-P-CONDITIONED-COORDINATES | Proposition 7.12 | Conditioned coordinate transport |
PSC-I-C-COMPLETION-PACKET-SPLIT | Corollary 7.13 | Completion preserves a finite packet split |
PSC-I-D-UNCONDITIONAL-PACKET-SPACE | Definition 7.14 | Unconditional packet sum space |
PSC-I-L-UNCONDITIONAL-COMPLETENESS | Lemma 7.15 | Completeness of the unconditional packet sum |
PSC-I-T-COUNTABLE-UNCONDITIONAL-PACKETS | Theorem 7.16 | Countable unconditional packet isomorphism |
PSC-I-R-UNIFORM-BOUNDEDNESS | Remark 7.17 | Uniform boundedness |
PSC-I-B-INFINITE-PACKET-TOPOLOGY | Boundary 7.18 | Infinite packet sums |
PSC-I-D-TRANSFER-BLOCK | Definition 8.1 | Transfer block |
PSC-I-T-OPERATOR-RECONSTRUCTION | Theorem 8.2 | Exact operator reconstruction |
PSC-I-T-BLOCK-MULTIPLICATION | Theorem 8.3 | Packet matrix multiplication |
PSC-I-C-BLOCK-POWERS | Corollary 8.4 | Packet powers and paths |
PSC-I-C-ADJOINT-REVERSAL | Corollary 8.5 | Adjoint reversal |
PSC-I-C-TENSOR-TRANSFER-BLOCKS | Corollary 8.6 | Tensor product transfer blocks |
PSC-I-T-BLOCK-INTERTWINING | Theorem 8.7 | Blockwise intertwining equations |
PSC-I-T-BLOCK-ALGEBRA | Theorem 8.8 | Full block algebra representation |
PSC-I-C-PACKET-SUPPORT-PROPAGATION | Corollary 8.9 | Propagation of packet support |
PSC-I-C-DIMENSION-COUNT | Corollary 8.10 | Dimension count |
PSC-I-P-BLOCK-DIAGONAL-COMMUTANT | Proposition 8.11 | Block diagonal projection and packet commutant |
PSC-I-D-SUPPORT-RELATION | Definition 8.12 | Support relation and support space |
PSC-I-T-SUPPORT-PATTERN-ALGEBRA | Theorem 8.13 | Support pattern algebra criterion |
PSC-I-C-SUPPORT-PATTERN-STAR | Corollary 8.14 | Bounded support patterns closed under \(*\) |
PSC-I-T-PREORDER-ALGEBRA-DECOMPOSITION | Theorem 8.15 | Preorder support algebra decomposition |
PSC-I-D-TRANSFER-GRAPH | Definition 9.1 | Transfer graph of an algebra generating family |
PSC-I-T-ALGEBRA-REACHABILITY-SUPPORT | Theorem 9.2 | Reachability support of the generated algebra |
PSC-I-P-REACHABILITY-OBSTRUCTION | Proposition 9.3 | Reachability obstruction for generated hulls |
PSC-I-D-DIRECTED-SEED-RANK | Definition 9.4 | Packet pure seed rank |
PSC-I-P-PACKET-PURE-RANK-BOUNDS | Proposition 9.5 | Basic packet pure rank bounds |
PSC-I-D-EDGE-SURJECTIVE | Definition 9.6 | Edge surjective packet system |
PSC-I-T-SOURCE-COMPONENT-SEED-RANK | Theorem 9.7 | Source component formula for packet pure seed rank |
PSC-I-D-PACKET-PROPAGATING | Definition 9.8 | Packet propagating system |
PSC-I-C-SOURCE-COMPONENT-COUNT | Corollary 9.9 | Unweighted source component count |
PSC-I-B-PACKET-PURE-BOUNDARY | Boundary 9.10 | Mixed support seeds can merge source requirements |
PSC-I-T-COORDINATE-TRANSPORT | Theorem 10.1 | Coordinate transport |
PSC-I-D-PACKET-MORPHISM | Definition 10.2 | Packet compatible operator morphism |
PSC-I-D-SEED-MORPHISM | Definition 10.3 | Morphism of seeded systems |
PSC-I-T-NATURALITY | Theorem 10.4 | Naturality of generated hulls and transfer blocks |
PSC-I-P-SEED-SYSTEM-CATEGORY | Proposition 10.5 | Category of seeded packet systems |
PSC-I-T-PACKET-EXACT-SEQUENCE | Theorem 10.6 | Packet exact sequence for an invariant subspace |
PSC-I-T-QUOTIENT-PACKET-DESCENT | Theorem 10.7 | Packet descent through an invariant quotient |
PSC-I-C-QUOTIENT-PACKET-DESCENT | Corollary 10.8 | Restriction and quotient of transfer blocks |
PSC-I-C-TOPOLOGICAL-PACKET-EXACT-SEQUENCE | Corollary 10.9 | Topological packet exact sequence |
PSC-I-T-DENSE-REALIZATION | Theorem 10.10 | Dense realization theorem |
PSC-I-T-QUOTIENT-TOPOLOGY-COMPLETION | Theorem 10.11 | Quotient topology and completed realization |
PSC-I-B-TOPOLOGICAL-QUOTIENT | Boundary 10.12 | Continuous surjections and quotient topology |
PSC-I-D-REALIZATION-FUNCTOR | Definition 11.1 | Realization functor and preservation profile |
PSC-I-T-REALIZATION-EXPORT | Theorem 11.2 | Equational realization principle |
PSC-I-P-REALIZATION-EXPORT | Proposition 11.3 | Realization export principle |
PSC-I-D-SEMANTIC-REALIZATION | Definition 11.4 | Semantic realization criterion |
PSC-I-ALG-EXAMPLE-SLOTS | Definition 12.1 | Worked realization interface |
PSC-I-EXPORT | Definition 12.2 | Paper I export object |
PSC-I-B-FINAL-CLAIM-BOUNDARY | Boundary 12.3 | Exact limits of Paper I |
B Visual atlas
On this page · Permalink · Source line 192
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 match this edition.
| Plate | Route through the examples |
|---|---|
| 1, 2 | Fixed grammars, seed power, and the objects of the calculus. |
| 3, 4 | Two linked chains and a quotient proving the minimum seed count. |
| 5, 6 | Left ideal relations and typed reachability with a missing direction. |
| 7, 8 | Oblique exact coordinates and complete transfer block multiplication. |
| 9, 10 | Cancellation along paths and the algebra of admissible zero patterns. |
| 11, 12 | Coordinate transport, shared action, and independent control. |
| 13, 14 | Semisimple multiplicity budgets and primary extraction polynomials. |
| 15, 16 | Path endpoints and the cycle's two dimensional quotient obstruction. |
| 17 | A coordinate ring relation as a two packet product rule. |
| 18, 19 | Dense shift generation, residue coordinates, and address carry. |
| 20, 21 | Exact orbit hull stabilization and all tensor cross terms. |
| 22 | The scope of mathematical, formal, and computational evidence. |
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. Explore all 22 worked atlas plates in HTML
References
assemSimsonSkowronski2006
I. Assem, D. Simson, and A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume 1: Techniques of Representation Theory, London Mathematical Society Student Texts 65, Cambridge University Press, Cambridge, 2006. doi:10.1017/CBO9780511614309.
brouwerHaemers2012
A. E. Brouwer and W. H. Haemers, Spectra of Graphs, Universitext, Springer, New York, 2012. doi:10.1007/978-1-4614-1939-6.
conway1990
J. B. Conway, A Course in Functional Analysis, second edition, Graduate Texts in Mathematics 96, Springer, New York, 1990. doi:10.1007/978-1-4757-4383-8.
hornJohnson2012
R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, Cambridge, 2012. doi:10.1017/CBO9781139020411.
lam2001noncommutative
T. Y. Lam, A First Course in Noncommutative Rings, second edition, Graduate Texts in Mathematics 131, Springer, New York, 2001. doi:10.1007/978-1-4419-8616-0.
lam1999modules
T. Y. Lam, Lectures on Modules and Rings, Graduate Texts in Mathematics 189, Springer, New York, 1999. doi:10.1007/978-1-4612-0525-8.
roman2008
S. Roman, Advanced Linear Algebra, third edition, Graduate Texts in Mathematics 135, Springer, New York, 2008. doi:10.1007/978-0-387-72831-5.
schaeferWolff1999
H. H. Schaefer and M. P. Wolff, Topological Vector Spaces, second edition, Graduate Texts in Mathematics 3, Springer, New York, 1999. doi:10.1007/978-1-4612-1468-7.
silverman2009
J. H. Silverman, The Arithmetic of Elliptic Curves, second edition, Graduate Texts in Mathematics 106, Springer, New York, 2009. doi:10.1007/978-0-387-09494-6.
demouraUllrich2021
L. de Moura and S. Ullrich, The Lean 4 Theorem Prover and Programming Language, in Automated Deduction—CADE 28, Lecture Notes in Computer Science 12699, Springer, Cham, 2021, pp. 625–635. doi:10.1007/978-3-030-79876-5_37.
mathlib2020
The mathlib Community, The Lean Mathematical Library, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, pp. 367–381. doi:10.1145/3372885.3373824.