Reading orientation
The complete finite manuscript comes first. All six supplementary proof developments follow as Appendices A–F. A worked visual atlas closes the volume. The separate visual and Lean companions provide another reading route and an explicit evidence register.
Reading this edition
On this page · Permalink · Source line 119
An operator representation determines what a computation means before it determines how a device executes it. Paper VIII develops that distinction through packet blocks, low rank corrections, graph support, preconditioning, precision, and finite compilation. Three exact examples introduce the main choices. The manuscript then gives their general statements and proofs.
All seven retrieved mathematical source parts are preserved byte for byte. The main manuscript retains all 85 numbered mathematical records, including all 56 explicit theorem, proposition, and corollary proof bodies. Its section and item numbers remain unchanged. Appendices A–F retain the complete substantive mathematics of six formal supplements, including constructions that strengthen the shorter manuscript arguments. Overlapping statements and derivations are retained because their hypotheses and uses differ. These counts do not measure distinct discoveries.
The selected v0.6.0 formal checkpoint records coverage of all 56 finite manuscript-proved items under its stated hypotheses. It contains 392 named theorem declarations in 40 modules, with 373 Paper VIII declarations and 19 reused quantum-packet declarations. The 66 construction audits and four classical inputs are different evidence units. This monograph carries the inherited compiler evidence and does not claim a fresh Lean compilation. The Lean companion records the actual hypotheses, declarations, hashes, and replay boundaries.
The source already includes positive precision budgets and caps, nonempty allocation sets, positive physical denominators and transform orders, valid band widths, actual positive square roots, reflexive reachability, and the empty-graph depth-zero case. Its arithmetic counts describe declared event models. Compiler stability uses solved child scores, and local recompilation assumes correct unaffected sibling caches. These hypotheses are part of the results.
The small-core recompression result starts from supplied ordered thin-SVD equations and handles arbitrary ambient competitors by compression. It does not establish SVD existence, a floating-point QR/SVD algorithm, or a canonical singular-values API identification. The other three classical inputs concern exact-arithmetic conjugate gradients, a stated floating-point model, and simultaneous spectral decomposition. A rounded action on varying inputs requires a uniform certificate before it can be treated as one fixed linear operator.
Representation, output, model, observation
A compressed action and an explicit matrix are different outputs. An additive cost model and an observed execution time are different evidence. A finite compiler optimum and unrestricted structure discovery are different problems. Keep the representation, output contract, mathematical model, and recorded measurement together when using a result.
Every hardware time and speed ratio remains an inherited observation from the archived corpus. No fresh GPU run is reported. Missing source-value hashes and explicit correctness-reference fields limit the historical comparisons. Cross-scope CPU, graph-replay, and two-stream rows retain their qualifications. In the negative-control figure, “matched baseline” means the baseline recorded for that comparison. It does not certify the full fairness contract set out in the benchmark discussion.
The historical pending statements in Appendices A–E describe their dated checkpoints. Appendix F completes the finite register. Three broader targets remain open: unrestricted discovery, compilation with nonlocal overlapping models, and a packet-native communication theorem for a specified architecture. The new exact examples and the visual atlas illustrate finite mathematics. They add no hardware performance claim and do not replace the proofs.
Abstract
On this page · Permalink · Source line 144
A packet operator is a linear map written between the members of a finite direct sum. We study the resulting computational representation before choosing a processor or kernel. Exact formulas are given for block sparse application, block diagonal plus low rank algebra, Woodbury inversion, support propagation, block preconditioning, and packetwise perturbation. Products of low rank corrections admit optimal recompression through a small singular value problem, with explicit error propagation through a product chain. A rooted candidate decomposition supports an exact compiler when representation cost and error are additive. Dynamic programming gives the optimal Lagrangian pruning, an exact quantized error budget algorithm, and a local update rule. Discrete precision assignment becomes a multiple choice budget problem. Arithmetic, storage, data movement, launch count, discovery, transfer, and materialization are kept as separate costs. A preserved corpus of 154 recorded CPU and GPU measurements illustrates regular packet gains, precision frontiers, crossover behavior, and retained negative controls. Its largest reported structured ratio is 14.89 against a device resident dense GPU calculation, with archived matching-metadata limitations stated explicitly. The paper proves finite algebraic and optimization statements. Hardware measurements remain specific to their recorded environment, and no generic dense matrix exponent or universal discovery algorithm is claimed.
The finite manuscript
The main reading path follows exact packet semantics, algebra, support, numerical certificates, and optimization before reaching the archived measurement corpus. The cost and error assumptions determine where each algorithm is exact.
Read a. exact semantics, support, and low-rank identities Read b. exact compilation, continuous precision, and explicit costs Read c. product chains, krylov spaces, and integer budgets Read d. structured transforms and clipped precision Read e. constructed graph schedules, support, and preconditioning Read f. global small-core recompression from ordered thin svd data
Worked visual atlas
On this page · Permalink · Source line 162
References
On this page · Permalink · Source line 166