A Visual studies
On this page · Permalink · Source line 1
These studies follow declared finite examples from an exact factor to a probability enclosure. Their Python sources and inputs accompany the volume. They are explanatory calculations, not additional production benchmarks.
From a factor to a justified tail
On this page · Permalink · Source line 5
The four layers answer different questions: what must reside in memory, what can propagate, what range remains unresolved, and how the tail calculation meets its accuracy contract.
Integer controls check block identities and phase zeros. Floating calculations illustrate compression and analytic bounds. A finite positive sum supplies an independent deep-tail control. The main chapters supply the proofs, Appendix B identifies formal coverage, and the final study separates algebraic, analytic, and numerical evidence.
Study result
Preserve exact identities where possible. Expose every approximation at the point where it enters.
Reading connection. Chapter 12.
Study 01 / Factor and law: A spectrum is the distributional interface
On this page · Permalink · Source line 15
Two numerically evaluated nonzero Gram spectra for the declared integer factor. Their matching points use distinct markers.
For a central Gaussian vector with covariance \(\Sigma\succeq0\) and symmetric \(M\), the quadratic form becomes a weighted sum of independent standard-normal squares after whitening and orthogonal diagonalization. The operator may originate in a kernel, a signal model, or another symmetric construction. Once its spectrum has been correctly obtained, the tail layer sees those coefficients.
The nonzero eigenvalues of the two Gram matrices coincide. The small integer factor in this guide has six sample coordinates and nine feature coordinates. One Gram matrix therefore has six eigenvalues. The other has the same six nonzero eigenvalues plus three zeros. The figure compares their floating evaluations.
Positive coefficients give support on the nonnegative half-line. Signed coefficients define a different support problem. The exact reduction extends to symmetric indefinite forms, while the positive-support interval backend developed later has narrower hypotheses.
Study result
Representation equivalence is exact mathematics. Certifying computed eigenvalues is a further numerical obligation.
Reading connection. Chapter 1.
Study 02 / Storage partition: Column blocks add their Gram operators exactly
On this page · Permalink · Source line 31
All block Gram contributions use the same color scale. Their exact sum is the full sample kernel.
Partition a factor by columns and keep every block. Horizontal concatenation turns the sample-space Gram matrix into a sum of block Gram matrices. Changing the block widths or the order in which blocks are read preserves the represented operator.
The figure splits the declared \(6\times9\) integer factor into three blocks of width three. Every matrix entry in the displayed identity is an integer, and the regeneration script checks equality exactly. Block storage introduces no statistical approximation.
A streamed action need not store each block kernel. It first multiplies by the block transpose, then by the block itself, and accumulates the sample-space result. The dimensions explain why the operator can remain exact even when the whole factor cannot reside at once.
Study result
Execution partitions determine residence and I/O. Keeping all blocks preserves the operator.
Reading connection. Chapter 2.
Study 03 / Algebraic sizing: Memory depends on the resident width
On this page · Permalink · Source line 47
An explicitly counted binary64 payload with fixed resident width. Total-factor storage grows linearly in \(m\).
A full factor holds \(nm\) scalar entries. A streamed action with resident width \(c\) and block-vector width \(s\) keeps a factor block and a small number of action buffers. Residualization against a covariate basis of rank \(p\) adds \(np\) entries. At fixed \(c,s,p\), this algebraic working set does not grow with total column count \(m\).
The sizing curve is an illustration, not a measured memory profile. It uses \(n=2000\), \(c=512\), \(s=32\), \(p=3\), and binary64 entries. The plotted streamed payload counts one resident factor, two sample buffers, one block intermediate, and the covariate basis.
Backend workspace, I/O buffers, saved outputs, and spectral-solver storage require their own accounting. A two-dimensional sample/feature tile also needs its tile-local covariate data. An algebraic storage bound does not promise a device-specific allocation total.
Study result
Separate algebraic payload, implementation workspace, and persistent output when planning memory.
Reading connection. Chapter 2.
Study 04 / Weighted-feature specialization: Residualization is an orthogonal projection
On this page · Permalink · Source line 63
An exact two-coordinate projection splits a feature into removed and retained components.
For a covariate range basis \(Q_X\) with orthonormal columns, the residualizer \(M_X=I-Q_XQ_X^{\mathsf T}\) removes the component in the covariate span. It is symmetric and idempotent. Applying it to the weighted feature factor restricts the kernel to variation left after the null-model covariates have been removed.
The two-coordinate control draws the exact split \((4,3)=(4,0)+(0,3)\). The horizontal axis represents the covariate span and the vertical axis its orthogonal complement. This picture explains the geometry. The general projector acts in the full sample space.
The factor \(A=M_XGW^{1/2}\) is one specialization of the domain-independent engine. A correct range basis must represent the actual covariate span. Rank deficiency cannot be handled by silently treating extra QR columns as covariate directions.
Study result
The general engine operates on factors. Residualized weighted features provide one important factor construction.
Reading connection. Chapter 2.
Study 05 / Structural locality: Exact zeros create a finite phase cone
On this page · Permalink · Source line 79
Exact integer phase support for depths zero through four. A colored entry is genuinely nonzero.
Choose a complete orthogonal family of phase projectors on feature space and form \(H=A^{\mathsf T}A\). An edge from phase \(g\) to phase \(h\) exists when the transfer block \(P_hHP_g\) is nonzero. Each operator application follows one graph edge. An iterate of depth \(k\) cannot reach a phase farther than \(k\) edges away.
The finite control is a nine-phase chain with \(H=2I+S+S^{\mathsf T}\) and a unit start in phase five. The printed entries are exact integers in \(H^kx\), and the shaded support expands by one phase at each step. The script checks every zero outside the cone.
These exact zeros justify omitting inactive phases for that finite-depth query. Storage blocks may still subdivide each active phase arbitrarily. The phase graph answers propagation questions, while the storage partition answers residence questions.
Study result
A certified zero allows exact omission. A merely small coupling needs an error bound.
Reading connection. Chapter 3.
Study 06 / Approximate locality: Weak edges need a transfer envelope
On this page · Permalink · Source line 95
One declared weak-edge control. A symmetric-log axis keeps exact zeros at zero rather than assigning a positive display floor.
A weak nonzero coupling destroys the exact-zero conclusion. Record the spectral norm of every phase block in a nonnegative transfer matrix \(\mathcal B\). The phase-norm profile of any block vector is dominated componentwise by multiplication with \(\mathcal B\).
For a retained operator \(H_0\), let \(\mathcal B_0\) keep the corresponding entries. Telescoping the two operator powers gives a phasewise bound on the omitted action. Symmetric block retention preserves self-adjointness. The power estimate itself does not require the retained operator to be positive.
The toy chain receives a signed weak edge of weight \(-0.035\) between phases one and nine. Starting in phase five, that edge has no effect through depth four. At later depths the figure compares floating observed error with the transfer-envelope evaluation. The theorem supplies the general bound. The plot checks this finite instance.
Study result
Approximate locality produces a budgeted leakage quantity, not an exact support assertion.
Reading connection. Chapter 3.
Study 07 / Core and residual: The unresolved range has positive structure
On this page · Permalink · Source line 111
Positive residual coefficients and their invariants for a declared coordinate-range control.
Let \(U\) contain \(d\) orthonormal sample-space directions. Project the factor into its captured range coordinates \(B=U^{\mathsf T}A\) and residual \(F=(I-UU^{\mathsf T})A\). Orthogonality eliminates the cross terms in the feature-space Gram matrix.
The missing term is the positive operator \(R=F^{\mathsf T}F\). Its trace is the missing mean of the Gaussian quadratic form. Its square trace measures concentration, and its spectral norm caps any unresolved coefficient. These invariants convey more information than one generic operator-norm error.
The control captures the first three coordinate directions of the integer factor. Its Gram decomposition is checked exactly. Residual eigenvalues and the cap are floating diagnostics. A small residual norm alone does not prove that an extreme-tail probability has the requested relative accuracy.
Study result
Unresolved spectral mass is an explicit object with its own trace, concentration, and cap.
Reading connection. Chapter 5.
Study 08 / Exact completion: A small remaining range can be completed
On this page · Permalink · Source line 127
Completed and full singular spectra coincide in the integer factor control. The captured core is incomplete.
If the residual admits \(F=WD\) with orthonormal columns of \(W\), its range lies orthogonal to \(U\). Appending \(W\) therefore creates an orthonormal synthesis factor, and stacking the two coordinate cores recovers the full factor.
The nonzero singular values of the completed core equal those of the original factor. The figure compares the incomplete captured core with the completed core in the declared integer example. Exact reconstruction of that factor is checked before numerical singular values are plotted.
Residual moments also provide a rank lower bound. Together with the orthogonal-complement dimension they can identify the missing rank when the two integers agree. A completion procedure must retain all genuine residual directions. A floating rank threshold has a separate error obligation.
Study result
When the remaining rank is affordable, exact completion can replace further approximate iteration.
Reading connection. Chapter 5.
Study 09 / Probability reweighting: Tilting moves the query into the bulk
On this page · Permalink · Source line 143
The threshold becomes central under the tilted law. The likelihood-ratio weight restores the original tail.
For a positive spectrum, the cumulant generating function is a sum of logarithms. A real tilt inside its domain defines a normalized reweighted law. The original upper tail becomes an exponential prefactor times a bounded weighted expectation under that law.
For an upper-tail planner query \(q>\mathbb E Q\), the saddlepoint solves \(\kappa'(\theta)=q\). It centers the tilted law at the threshold and often improves numerical efficiency. The enclosure identity holds for any admissible positive tilt. Certification does not require solving the saddlepoint exactly.
The figure uses \(Q=0.02\chi^2_{80}\) and \(q=4\). Its original mean is \(1.6\), while the tilted mean is \(4\) at \(\theta=15\). The plotted densities follow the same exact gamma family with different scales. No approximation to the probability law is introduced by tilting.
Study result
Use the tilt to condition the calculation. Retain the exact reweighting identity to preserve the target probability.
Reading connection. Chapter 6.
Study 10 / Local transform representation: A spectral packet stores centered moments
On this page · Permalink · Source line 159
Centered storage and the declared-grid remainder ladder for one finite packet.
The packet stores nearby eigenvalues through their mean \(\mu_P\) and centered power sums \(M_{P,m}\), with \(M_{P,1}=0\). It expands the log transform rather than substituting a surrogate distribution.
Use a nonempty positive packet, integer order \(p\ge0\), and \(\Re s<1/(2\lambda_{\max})\). The factor logarithms use their principal branches and sum to the analytic \(\kappa\) normalized at zero. For \(\rho_P(s)<1\), the series has the stated remainder, which decreases geometrically when the radius ratio stays away from one.
The five-eigenvalue control uses \(0.09,0.095,0.10,0.105,0.11\), a tilt of one, and 220 frequencies from zero to eighteen. The figure compares floating transform errors with the analytic remainder at orders one through eight. These computations illustrate the bound. They do not enclose library rounding.
Study result
The local packet representation requires the transform domain, logarithm branch, and printed radius condition.
Reading connection. Chapter 6.
Study 11 / Grid-dependent compilation: The query determines the useful packet
On this page · Permalink · Source line 176
The same spectral packet has different expansion ratios at tilts zero, two, and four.
A distance between eigenvalues is insufficient to decide whether a packet is useful. The expansion must be controlled at the actual complex arguments \(s_k=\theta+i k\pi/b\) selected by the tail query. The tilt, support endpoint, and retained mode count all change that grid.
The figure holds the same five eigenvalues and packet center fixed while changing the tilt. Near the transform singularity the low-frequency radius can grow sharply. At high frequency the radius approaches the relative packet half-width. Neither effect is captured by inspecting raw eigenvalue spacing alone.
The compiled representation may retain large spikes exactly and packetize a smooth spectral bulk. Split a packet or raise its order when its propagated error exceeds budget. A plan can be reused only after checking that its stored conditions and grid remain applicable to the new request.
Study result
The passport belongs to a spectrum, a query, and an accuracy contract, rather than to the spectrum alone.
Reading connection. Chapter 6.
Study 12 / Finite-window transform: Cosine inversion integrates a weighted tail
On this page · Permalink · Source line 192
The weighted payoff and finite-interval basis have different roles. The prime gives half weight to mode zero.
On a positive-support interval \([0,b]\), the cosine frequencies are \(u_k=k\pi/b\). The payoff is zero below the threshold and decays exponentially above it. Integrating each cosine mode against that payoff gives an explicit coefficient.
The finite sum uses the tilted characteristic function rather than a CDF value close to one. Multiplying by the likelihood-ratio prefactor returns the original tail scale. This avoids subtracting two almost equal numbers, but it does not remove the need to bound discarded support and omitted modes.
The picture uses \(q=4\), \(b=7\), and \(\theta=15\). The payoff and three cosine modes share one coordinate system, with distinct line styles and an explicit payoff discontinuity. Correctness of the positive-support backend requires \(q\ge0\) and \(b>q\). The saddlepoint planner additionally selects upper-tail queries above the original mean.
Study result
A finite-window, finite-mode transform is an intermediate quantity whose omitted contributions require bounds.
Reading connection. Chapter 7.
Study 13 / Omitted Fourier modes: Mode decay bounds the infinite remainder
On this page · Permalink · Source line 208
Declared equal-coefficient controls illustrate why the number of active coefficients affects high-frequency decay.
The modulus of the normalized tilted characteristic function has a positive product formula. Its decay is controlled by the actual transformed coefficients. More active positive coefficients increase the asymptotic decay exponent.
The figure compares eight and eighty equal coefficients at the same admissible tilt. It evaluates the exact modulus formula in ordinary floating arithmetic. A rapidly falling curve is useful for choosing modes, but acceptance depends on a proved bound for the entire omitted series.
The rigorous interval backend uses a simple envelope \(C_\theta t^{-r/2}\) and the payoff bound \(|J_k|\le1/\theta\). Its resulting series bound requires \(r>2\). The packetized analytic path has a sharper frequency-dependent decay-rate bound. Those are distinct formulas with distinct implementation scopes.
Study result
The infinite-mode remainder is a mathematical tail of a series, separate from floating summation error.
Reading connection. Chapter 7.
Study 14 / Analytic and arithmetic budgets: The error ledger keeps separate causes
On this page · Permalink · Source line 224
Four causes of uncertainty and their natural controls. Every budget must be justified before acceptance.
Packet approximation changes the retained-grid transform. Support truncation and cosine periodization change the finite-window functional. Mode truncation removes infinitely many terms. These three mathematical approximation errors have different refinement controls and must be accounted for separately.
Directed-rounding arithmetic introduces a fourth quantity: the width of the computed interval for finite operations. That width is not a substitute for an analytic remainder. Conversely, an analytic bound does not automatically enclose the rounding of logarithms, exponentials, or summation.
For the exact-spectrum interval backend, no packet approximation is used. The finite transform interval is enlarged by support and series bounds, then passed through a positive logarithm and prefactor enclosure. Extending directed-rounding certification to the packet transform requires enclosing its moment construction and remainder propagation as well.
Study result
Name the uncertainty before refining it. The same scalar tolerance can hide different unresolved causes.
Reading connection. Chapter 7.
Study 15 / Requested accuracy: Acceptance is a logarithmic interval test
On this page · Permalink · Source line 240
An illustrative tolerance of \(10^{-8}\) determines the permitted log width. The plotted curve is numerical.
A positive probability enclosure can be stored on a logarithmic scale even when its endpoints are below ordinary floating-point range. If \(d_-\) and \(d_+\) enclose \(\log_{10}p\), the width determines the maximum multiplicative uncertainty.
For validated acceptance, compute the width and \(\operatorname{expm1}(\log(10)w)\) with directed interval arithmetic. Compare the ratio interval’s upper endpoint to the exact tolerance enclosure’s lower endpoint. Preserve the literal outer endpoints throughout parsing and conversion. High precision alone does not prove this decision.
The controller returns an accepted result only after the full enclosure passes the requested tolerance. An unresolved positive lower bound, invalid transform domain, inadequate mode budget, or exhausted precision budget must produce a failure status. A point estimate can still be informative, but it cannot be relabeled as an accepted enclosure.
Study result
The decision logic and input semantics are part of certification, just as the transform arithmetic is.
Reading connection. Chapter 10.
Study 16 / Independent control family: An exact-law control reaches deep logarithms
On this page · Permalink · Source line 256
An independently evaluable exact-law family. The plot is regenerated from a positive finite sum in decimal arithmetic.
For an even-degree chi-square variable, the upper tail has a finite positive-sum formula. The control \(Q=0.02\chi^2_{80}\) is a gamma law of integer shape forty and scale \(0.04\). Its survival probability can therefore be evaluated independently of cosine inversion.
The curve computes the logarithm first. At thresholds from \(1.6\) through \(500\), it evaluates the finite sum with ninety decimal digits and plots its logarithm. The exact law supplies the formula. The numeric points are high-precision evaluations rather than directed-rounding enclosures.
This control can distinguish a transform error from a reference error without relying on another COS run. Its equal-coefficient structure also means that one packet can represent the spectrum exactly. Success on this family does not establish equal performance for heterogeneous spectra, signed laws, or every matrix-to-spectrum bridge.
Study result
Choose a reference with a different mathematical route. Report its arithmetic scope alongside the result.
Reading connection. Chapter 9.
Study 17 / Publication and evidence map: Read each evidence layer on its own terms
On this page · Permalink · Source line 272
| Representation layer | Evidence to inspect | Scope to preserve |
|---|---|---|
| Block / projector algebra | Exact identities. Selected Lean sources | All required hypotheses and finite dimensions |
| Computed spectrum | Validated matrix-to-spectrum bridge | Input semantics. Residual and rounding enclosures |
| Spectral packet transform | Analytic remainders. Executable checks | Complex-grid radius. Arithmetic error |
| Positive exact-spectrum tail | Directed-rounding interval. Analytic bounds | Admissible tilt. Positive support. Active rank |
| Controller decision | Enclosure-width test. Precision and parsing tests | Requested tolerance. Explicit failure status |
The main chapters explain the operator identities, propagation bounds, residual structure, packet construction, and probability enclosures. The atlas makes those mechanisms inspectable through small declared cases. The formalization appendix identifies exactly which finite-algebra or order statements are represented by its source files and what the checked build establishes.
A Lean proof of block matrix algebra does not automatically certify a Python eigensolver, a decimal parser, or a transcendental interval library. A directed-rounding tail computation for exact supplied coefficients does not automatically certify coefficients computed by an unverified SVD. Each interface needs its own evidence.
The accompanying package preserves executable sources and verification records. Rebuild the figures with illustrations/production_figures.py, inspect its input manifest, and compare the formalization guide with its checked sources. All illustrations use declared controls, and no empirical timing or production tail claim is introduced by this atlas.
Study result
A complete result carries its assumptions, representation semantics, numerical enclosure, and formal scope.
Reading connection. Appendix B.