A_atlas.tex

COS Method

A_atlas.tex

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

Skip source text

1 \chapter{Visual studies}\label{app:atlas}
2 \begingroup\small
3 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.
4 
5 {\displayface\fontsize{27}{30}\selectfont\color{ink}From a factor to a justified tail\par}
6 \vspace{3pt}
7 \begin{center}\includegraphics[width=\linewidth]{figures_production/00_pipeline.pdf}\end{center}
8 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.
9 
10 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~\ref{app:lean} identifies formal coverage, and the final study separates algebraic, analytic, and numerical evidence.
11 
12 \studyresult{Preserve exact identities where possible. Expose every approximation at the point where it enters.}
13 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:synthesis}.}
14 \clearpage
15 \atlasheading{01}{Factor and law}{A spectrum is the distributional interface}
16 \vspace{3pt}
17 \begin{center}\includegraphics[width=\linewidth]{figures_production/01_factor_spectrum.pdf}\end{center}
18 {\small\color{navy}Two numerically evaluated nonzero Gram spectra for the declared integer factor. Their matching points use distinct markers.}
19 
20 \[X=\Sigma^{1/2}Z,\quad Z\sim N(0,I),\quad H=\Sigma^{1/2}M\Sigma^{1/2}.\]
21 \[X^{\mathsf T}MX\overset d=\sum_{j=1}^{r}\lambda_jZ_j^2,\qquad \lambda_j\in\operatorname{spec}(H)\setminus\{0\}.\]
22 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.
23 
24 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.
25 
26 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.
27 
28 \studyresult{Representation equivalence is exact mathematics. Certifying computed eigenvalues is a further numerical obligation.}
29 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:gaussian}.}
30 \clearpage
31 \atlasheading{02}{Storage partition}{Column blocks add their Gram operators exactly}
32 \vspace{3pt}
33 \begin{center}\includegraphics[width=\linewidth]{figures_production/02_block_gram.pdf}\end{center}
34 {\small\color{navy}All block Gram contributions use the same color scale. Their exact sum is the full sample kernel.}
35 
36 \[A=[A_1\ \cdots\ A_B],\qquad AA^{\mathsf T}=\sum_{b=1}^B A_bA_b^{\mathsf T}.\]
37 \[KV=\sum_b A_b(A_b^{\mathsf T}V),\qquad A_b\in\mathbb R^{n\times c_b},\quad V\in\mathbb R^{n\times s}.\]
38 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.
39 
40 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.
41 
42 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.
43 
44 \studyresult{Execution partitions determine residence and I/O. Keeping all blocks preserves the operator.}
45 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:streaming}.}
46 \clearpage
47 \atlasheading{03}{Algebraic sizing}{Memory depends on the resident width}
48 \vspace{3pt}
49 \begin{center}\includegraphics[width=\linewidth]{figures_production/03_memory.pdf}\end{center}
50 {\small\color{navy}An explicitly counted binary64 payload with fixed resident width. Total-factor storage grows linearly in $m$.}
51 
52 \[\text{working storage}=O(nc+ns+cs+np).\]
53 \[\text{illustrated payload}=8\,(nc+2ns+cs+np)\ \text{bytes}.\]
54 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$.
55 
56 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.
57 
58 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.
59 
60 \studyresult{Separate algebraic payload, implementation workspace, and persistent output when planning memory.}
61 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:streaming}.}
62 \clearpage
63 \atlasheading{04}{Weighted-feature specialization}{Residualization is an orthogonal projection}
64 \vspace{3pt}
65 \begin{center}\includegraphics[width=\linewidth]{figures_production/04_residualization.pdf}\end{center}
66 {\small\color{navy}An exact two-coordinate projection splits a feature into removed and retained components.}
67 
68 \[Q_X^{\mathsf T}Q_X=I,\quad M_X=I-Q_XQ_X^{\mathsf T},\quad M_X^2=M_X=M_X^{\mathsf T}.\]
69 \[A=M_XGW^{1/2},\qquad K=AA^{\mathsf T}.\]
70 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.
71 
72 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.
73 
74 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.
75 
76 \studyresult{The general engine operates on factors. Residualized weighted features provide one important factor construction.}
77 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:streaming}.}
78 \clearpage
79 \atlasheading{05}{Structural locality}{Exact zeros create a finite phase cone}
80 \vspace{3pt}
81 \begin{center}\includegraphics[width=\linewidth]{figures_production/05_phase_cone.pdf}\end{center}
82 {\small\color{navy}Exact integer phase support for depths zero through four. A colored entry is genuinely nonzero.}
83 
84 \[\sum_hP_h=I,\qquad g\to h\iff P_hHP_g\ne0.\]
85 \[\operatorname{dist}(g,h)>k\quad\Longrightarrow\quad P_hH^kP_g=0.\]
86 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.
87 
88 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.
89 
90 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.
91 
92 \studyresult{A certified zero allows exact omission. A merely small coupling needs an error bound.}
93 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:phases}.}
94 \clearpage
95 \atlasheading{06}{Approximate locality}{Weak edges need a transfer envelope}
96 \vspace{3pt}
97 \begin{center}\includegraphics[width=\linewidth]{figures_production/06_approximate_cone.pdf}\end{center}
98 {\small\color{navy}One declared weak-edge control. A symmetric-log axis keeps exact zeros at zero rather than assigning a positive display floor.}
99 
100 \[\rho(X)_h=\|P_hX\|_F,\qquad \mathcal B_{hg}=\|P_hHP_g\|_2.\]
101 \[\rho(H^kX)\le\mathcal B^k\rho(X),\qquad\rho((H^k-H_0^k)X)\le(\mathcal B^k-\mathcal B_0^k)\rho(X).\]
102 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$.
103 
104 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.
105 
106 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.
107 
108 \studyresult{Approximate locality produces a budgeted leakage quantity, not an exact support assertion.}
109 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:phases}.}
110 \clearpage
111 \atlasheading{07}{Core and residual}{The unresolved range has positive structure}
112 \vspace{3pt}
113 \begin{center}\includegraphics[width=\linewidth]{figures_production/07_residual.pdf}\end{center}
114 {\small\color{navy}Positive residual coefficients and their invariants for a declared coordinate-range control.}
115 
116 \[A=UB+F,\quad U^{\mathsf T}F=0,\quad A^{\mathsf T}A=B^{\mathsf T}B+F^{\mathsf T}F.\]
117 \[t=\operatorname{tr}R=\|F\|_F^2,\quad v=\operatorname{tr}(R^2),\quad \rho_R=\|R\|_2.\]
118 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.
119 
120 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.
121 
122 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.
123 
124 \studyresult{Unresolved spectral mass is an explicit object with its own trace, concentration, and cap.}
125 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:spectrum}.}
126 \clearpage
127 \atlasheading{08}{Exact completion}{A small remaining range can be completed}
128 \vspace{3pt}
129 \begin{center}\includegraphics[width=\linewidth]{figures_production/08_completion.pdf}\end{center}
130 {\small\color{navy}Completed and full singular spectra coincide in the integer factor control. The captured core is incomplete.}
131 
132 \[U^{\mathsf T}W=0,\qquad A=[U\ W]\begin{bmatrix}B\\D\end{bmatrix}.\]
133 \[\left\lceil\max\{t/\rho_R,t^2/v\}\right\rceil\le\operatorname{rank}F\le n-d\quad(F\ne0).\]
134 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.
135 
136 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.
137 
138 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.
139 
140 \studyresult{When the remaining rank is affordable, exact completion can replace further approximate iteration.}
141 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:spectrum}.}
142 \clearpage
143 \atlasheading{09}{Probability reweighting}{Tilting moves the query into the bulk}
144 \vspace{3pt}
145 \begin{center}\includegraphics[width=\linewidth]{figures_production/09_tilt.pdf}\end{center}
146 {\small\color{navy}The threshold becomes central under the tilted law. The likelihood-ratio weight restores the original tail.}
147 
148 \[\kappa(s)=-\frac12\sum_j\log(1-2s\lambda_j),\qquad 0<\theta<\frac1{2\lambda_{\max}}.\]
149 \[P(Q\ge q)=e^{\kappa(\theta)-\theta q}\,\mathbb E_\theta[e^{-\theta(Q-q)}\mathbf1_{\{Q\ge q\}}].\]
150 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.
151 
152 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.
153 
154 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.
155 
156 \studyresult{Use the tilt to condition the calculation. Retain the exact reweighting identity to preserve the target probability.}
157 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:packets}.}
158 \clearpage
159 \atlasheading{10}{Local transform representation}{A spectral packet stores centered moments}
160 \vspace{3pt}
161 \begin{center}\includegraphics[width=\linewidth]{figures_production/10_packet.pdf}\end{center}
162 {\small\color{navy}Centered storage and the declared-grid remainder ladder for one finite packet.}
163 
164 \[M_{P,m}=\sum_{j\in P}(\lambda_j-\mu_P)^m,\quad\alpha_P(s)=\frac{2s}{1-2s\mu_P},\quad\rho_P(s)=|\alpha_P(s)|\max_{j\in P}|\lambda_j-\mu_P|.\]
165 \[\kappa_P(s)=-\frac{n_P}{2}\log(1-2s\mu_P)+\frac12\sum_{m=1}^{p}\frac{\alpha_P(s)^m M_{P,m}}m+R_{P,p}(s),\]
166 \[|R_{P,p}(s)|\le\frac{n_P}{2}\frac{\rho_P(s)^{p+1}}{(p+1)(1-\rho_P(s))}.\]
167 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.
168 
169 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.
170 
171 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.
172 
173 \studyresult{The local packet representation requires the transform domain, logarithm branch, and printed radius condition.}
174 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:packets}.}
175 \clearpage
176 \atlasheading{11}{Grid-dependent compilation}{The query determines the useful packet}
177 \vspace{3pt}
178 \begin{center}\includegraphics[width=\linewidth]{figures_production/11_query_grid.pdf}\end{center}
179 {\small\color{navy}The same spectral packet has different expansion ratios at tilts zero, two, and four.}
180 
181 \[s_k=\theta+i\frac{k\pi}{b},\qquad\rho_P(s_k)<1\quad\text{on every retained frequency}.\]
182 \[(\Lambda,q,\varepsilon)\longmapsto\mathcal P_{\Lambda,q,\varepsilon}.\]
183 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.
184 
185 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.
186 
187 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.
188 
189 \studyresult{The passport belongs to a spectrum, a query, and an accuracy contract, rather than to the spectrum alone.}
190 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:packets}.}
191 \clearpage
192 \atlasheading{12}{Finite-window transform}{Cosine inversion integrates a weighted tail}
193 \vspace{3pt}
194 \begin{center}\includegraphics[width=\linewidth]{figures_production/12_cos.pdf}\end{center}
195 {\small\color{navy}The weighted payoff and finite-interval basis have different roles. The prime gives half weight to mode zero.}
196 
197 \[J_k=\int_q^be^{-\theta(x-q)}\cos(u_kx)\,dx=\Re\!\left[e^{iu_kq}\frac{1-e^{(-\theta+iu_k)(b-q)}}{\theta-iu_k}\right].\]
198 \[S_N=\frac2b\sum_{k=0}^{N-1}{}^{\prime}\, J_k\,\Re\,\phi_\theta(u_k),\qquad\phi_\theta(t)=e^{\kappa(\theta+it)-\kappa(\theta)}.\]
199 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.
200 
201 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.
202 
203 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.
204 
205 \studyresult{A finite-window, finite-mode transform is an intermediate quantity whose omitted contributions require bounds.}
206 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:inversion}.}
207 \clearpage
208 \atlasheading{13}{Omitted Fourier modes}{Mode decay bounds the infinite remainder}
209 \vspace{3pt}
210 \begin{center}\includegraphics[width=\linewidth]{figures_production/13_mode_decay.pdf}\end{center}
211 {\small\color{navy}Declared equal-coefficient controls illustrate why the number of active coefficients affects high-frequency decay.}
212 
213 \[a_j=\frac{2\lambda_j}{1-2\theta\lambda_j},\quad|\phi_\theta(t)|=\prod_j(1+(a_jt)^2)^{-1/4}\le C_\theta t^{-r/2}.\]
214 \[E_{\rm series}\le\frac{2C_\theta}{b\theta}\left(\frac b\pi\right)^\nu\left[N^{-\nu}+\frac{N^{1-\nu}}{\nu-1}\right],\quad\nu=r/2>1.\]
215 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.
216 
217 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.
218 
219 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.
220 
221 \studyresult{The infinite-mode remainder is a mathematical tail of a series, separate from floating summation error.}
222 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:inversion}.}
223 \clearpage
224 \atlasheading{14}{Analytic and arithmetic budgets}{The error ledger keeps separate causes}
225 \vspace{3pt}
226 \begin{center}\includegraphics[width=\linewidth]{figures_production/14_ledger.pdf}\end{center}
227 {\small\color{navy}Four causes of uncertainty and their natural controls. Every budget must be justified before acceptance.}
228 
229 \[|p-\widehat p|\le E_{\rm packet}+E_{\rm support}+E_{\rm modes}\quad\text{(analytic packet path)}.\]
230 \[S_\theta(q)\in\boldsymbol S_N+[-E,E],\qquad E=E_{\rm support}+E_{\rm series}\quad\text{(exact-spectrum interval path)}.\]
231 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.
232 
233 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.
234 
235 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.
236 
237 \studyresult{Name the uncertainty before refining it. The same scalar tolerance can hide different unresolved causes.}
238 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:inversion}.}
239 \clearpage
240 \atlasheading{15}{Requested accuracy}{Acceptance is a logarithmic interval test}
241 \vspace{3pt}
242 \begin{center}\includegraphics[width=\linewidth]{figures_production/15_acceptance.pdf}\end{center}
243 {\small\color{navy}An illustrative tolerance of $10^{-8}$ determines the permitted log width. The plotted curve is numerical.}
244 
245 \[\log_{10}p\in[d_-,d_+],\quad w=d_+-d_-,\quad\frac{p_+}{p_-}-1=\operatorname{expm1}(\log(10)w).\]
246 \[\operatorname{expm1}(\log(10)w)\le\varepsilon\quad\Longrightarrow\quad\text{requested enclosure width is met}.\]
247 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.
248 
249 For validated acceptance, compute the width and $\operatorname{expm1}(\log(10)w)$ with directed interval arithmetic. Compare the ratio interval\textquotesingle s upper endpoint to the exact tolerance enclosure\textquotesingle s lower endpoint. Preserve the literal outer endpoints throughout parsing and conversion. High precision alone does not prove this decision.
250 
251 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.
252 
253 \studyresult{The decision logic and input semantics are part of certification, just as the transform arithmetic is.}
254 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:accuracy}.}
255 \clearpage
256 \atlasheading{16}{Independent control family}{An exact-law control reaches deep logarithms}
257 \vspace{3pt}
258 \begin{center}\includegraphics[width=\linewidth]{figures_production/16_exact_control.pdf}\end{center}
259 {\small\color{navy}An independently evaluable exact-law family. The plot is regenerated from a positive finite sum in decimal arithmetic.}
260 
261 \[z=q/0.04,\qquad P(Q\ge q)=e^{-z}\sum_{k=0}^{39}\frac{z^k}{k!}.\]
262 \[\log_{10}P(Q\ge q)=\frac{-z+\log\!\left(\sum_{k=0}^{39}z^k/k!\right)}{\log(10)}.\]
263 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.
264 
265 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.
266 
267 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.
268 
269 \studyresult{Choose a reference with a different mathematical route. Report its arithmetic scope alongside the result.}
270 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Chapter~\ref{ch:intervals}.}
271 \clearpage
272 \atlasheading{17}{Publication and evidence map}{Read each evidence layer on its own terms}
273 \vspace{3pt}
274 \vspace{5pt}\begin{center}\small\renewcommand{\arraystretch}{1.3}\begin{tabular}{@{}>{\raggedright\arraybackslash}P{.25\linewidth}>{\raggedright\arraybackslash}P{.33\linewidth}>{\raggedright\arraybackslash}P{.36\linewidth}@{}}\toprule
275 Representation layer & Evidence to inspect & Scope to preserve\\
276 \midrule
277 Block / projector algebra & Exact identities. Selected Lean sources & All required hypotheses and finite dimensions\\
278 Computed spectrum & Validated matrix-to-spectrum bridge & Input semantics. Residual and rounding enclosures\\
279 Spectral packet transform & Analytic remainders. Executable checks & Complex-grid radius. Arithmetic error\\
280 Positive exact-spectrum tail & Directed-rounding interval. Analytic bounds & Admissible tilt. Positive support. Active rank\\
281 Controller decision & Enclosure-width test. Precision and parsing tests & Requested tolerance. Explicit failure status\\
282 \bottomrule\end{tabular}\end{center}
283 \[\text{matrix input}\ \longrightarrow\ \text{spectral enclosure}\ \longrightarrow\ \text{tail enclosure}\ \longrightarrow\ \text{accepted width}.\]
284 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.
285 
286 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.
287 
288 The accompanying package preserves executable sources and verification records. Rebuild the figures with \decl{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.
289 
290 \studyresult{A complete result carries its assumptions, representation semantics, numerical enclosure, and formal scope.}
291 \vfill{\footnotesize\color{navy}\textbf{Reading connection.} Appendix~\ref{app:lean}.}
292 
293 \endgroup

Back to source controls

Other PDFs for this work

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: f91916706a1ac06cfb629d5349542b8303189c6e220e278fcf78c73b823b92e2

Original source on GitHub

Back to COS Method