COS Method

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

1 \chapter{Spectral uncertainty and exact completion}\label{ch:spectrum}
2 \chapterlead{A useful operator approximation is not automatically a useful tail
3 approximation. This chapter transports phase-pruning error to eigenvalue
4 intervals, measures unresolved range through trace information, and completes
5 small residual ranges exactly. A separate post-verification theorem connects
6 stored binary64 factors to rigorous spectral intervals.}
7 \section{From phase pruning to certified quadratic-form tails}\label{sec:final-22}
8 
9 The previous sections certify the effect of phase pruning on Krylov
10 propagation.  A SKAT-like test ultimately depends on the spectrum itself, so
11 one more bridge is needed:
12 \[
13 \text{phase pruning}
14 \longrightarrow
15 \text{operator error}
16 \longrightarrow
17 \text{spectral error}
18 \longrightarrow
19 \text{tail-probability error}.
20 \]
21 
22 \subsection{Block-norm operator domination}
23 
24 Let
25 \[
26 E=H-H_0
27 \]
28 be the self-adjoint error introduced by phase pruning.  Using the same
29 orthogonal phase projectors \(P_h\), define
30 \[
31 \mathcal C_{hg}
32 =
33 \|P_hEP_g\|_2.
34 \]
35 
36 \begin{theorem}[Block-norm operator certificate]\label{claim:final-22-1}
37 \[
38 \boxed{
39 \|E\|_2
40 \le
41 \|\mathcal C\|_2.
42 }
43 \]
44 \end{theorem}
45 
46 \begin{proof}
47 For any vector \(x\), let
48 \[
49 r_g=\|P_gx\|_2.
50 \]
51 Then
52 \[
53 \|P_hEx\|_2
54 \le
55 \sum_g
56 \|P_hEP_g\|_2\,\|P_gx\|_2
57 =
58 (\mathcal C r)_h.
59 \]
60 Orthogonality of the phase decomposition gives
61 \[
62 \|Ex\|_2^2
63 =
64 \sum_h\|P_hEx\|_2^2
65 \le
66 \|\mathcal C r\|_2^2
67 \le
68 \|\mathcal C\|_2^2\|r\|_2^2
69 =
70 \|\mathcal C\|_2^2\|x\|_2^2.
71 \]
72 Taking the supremum over unit vectors proves the claim.
73 \end{proof}
74 
75 The important computational point is that \(\mathcal C\) is only a
76 phase-by-phase matrix.  The same block norms already used to construct the
77 polyphase scheduler therefore provide a global operator certificate.
78 
79 \subsection{Weyl enclosure of the quadratic-form coefficients}
80 
81 Assume
82 \[
83 H\succeq0
84 \]
85 and let the eigenvalues of \(H\) and \(H_0\), in decreasing order, be
86 \[
87 \lambda_i
88 \qquad\text{and}\qquad
89 \mu_i.
90 \]
91 If
92 \[
93 \|H-H_0\|_2\le\varepsilon,
94 \]
95 Weyl's inequality gives
96 \[
97 |\lambda_i-\mu_i|\le\varepsilon.
98 \]
99 
100 \begin{corollary}[Positive spectral interval]\label{claim:final-22-2}
101 For every \(i\),
102 \[
103 \boxed{
104 \ell_i
105 =
106 \max\{0,\mu_i-\varepsilon\}
107 \le
108 \lambda_i
109 \le
110 u_i
111 =
112 \max\{0,\mu_i+\varepsilon\}.
113 }
114 \]
115 \end{corollary}
116 
117 This remains valid even if symmetric phase pruning makes \(H_0\) slightly
118 indefinite.
119 
120 \subsection{Certified generalized-\texorpdfstring{\(\chi^2\)}{chi-square} tail bracket}
121 
122 For independent standard normal variables \(Z_i\), define
123 \[
124 Q_-=\sum_i\ell_iZ_i^2,
125 \qquad
126 Q=\sum_i\lambda_iZ_i^2,
127 \qquad
128 Q_+=\sum_i u_iZ_i^2.
129 \]
130 
131 \begin{theorem}[Stochastic tail enclosure]\label{claim:final-22-3}
132 For every threshold \(q\),
133 \[
134 \boxed{
135 \Pr(Q_-\ge q)
136 \le
137 \Pr(Q\ge q)
138 \le
139 \Pr(Q_+\ge q).
140 }
141 \]
142 \end{theorem}
143 
144 \begin{proof}
145 Couple all three quadratic forms using the same normal variables \(Z_i\).
146 Since
147 \[
148 0\le\ell_i\le\lambda_i\le u_i
149 \]
150 for every \(i\),
151 \[
152 Q_-\le Q\le Q_+
153 \]
154 almost surely.  Taking upper-tail events yields the result.
155 \end{proof}
156 
157 The endpoint probabilities are separate tail queries. Each must satisfy the
158 hypotheses of the numerical backend used to evaluate it. In particular, zero
159 lower coefficients can reduce the active rank below the directed backend's
160 coverage. The stochastic enclosure remains valid in that case, but it does
161 not by itself supply a supported numerical evaluation. Numerical error is
162 separate from the spectral uncertainty above.
163 
164 \subsection{A dual-budget pruning rule}
165 
166 The local Krylov certificate from the previous section and the global spectral
167 certificate answer different questions.  The former asks whether omitted
168 couplings matter to the current Krylov query. The latter asks whether they can
169 move the spectrum enough to matter to the final test.
170 
171 An execution schedule should therefore enforce
172 \[
173 \boxed{
174 \sum_{e\in\mathcal O}\beta_e^{(k)}
175 \le
176 \tau_K,
177 \qquad
178 \|\mathcal C_{\mathcal O}\|_2
179 \le
180 \tau_\lambda.
181 }
182 \]
183 
184 The implementation uses a conservative greedy rule: phase pairs are considered
185 in increasing query-risk order, and a pair is omitted only when adding it
186 preserves both inequalities.  The rule is certified but is not claimed to be
187 globally optimal under the two simultaneous constraints.
188 
189 \begin{figure}[htbp]
190 \centering
191 \includegraphics[width=\linewidth]{figures_production/figure_14_dual_budget_tail_bridge.pdf}
192 \caption{Tail brackets under a fixed query budget and varying operator budgets. The dotted reference is at $\log_{10}p=-8$. A sufficiently loose operator budget admits a strong coupling and widens the bracket even though the query-local constraint still passes.}
193 \label{fig:dual-budget-tail}
194 \end{figure}
195 
196 In the deterministic ten-phase experiment, fixing the query budget at
197 \(0.05\) and the operator budget at \(0.005\) removed \(23\) of \(45\)
198 undirected phase pairs.  At a reference probability near \(10^{-8}\), the analytic
199 tail bracket was
200 \[
201 10^{-8.11143}
202 \le
203 p
204 \le
205 10^{-7.89036},
206 \]
207 a width of about \(0.221\) decades. These endpoints summarize the
208 real-arithmetic error analysis evaluated in floating point, not a directed
209 rounding enclosure. With an operator budget of \(0.0075\),
210 \(34\) pairs were removed and the interval widened to about \(0.320\)
211 decades.  By contrast, allowing a strong coupling to be removed under a very
212 loose operator budget produced a multi-decade interval.
213 
214 \subsection{Certify after prune}
215 
216 There is a second route that does not use the pruned operator as the final
217 spectral approximation.  Let \(U\) be any orthonormal sample-space basis,
218 possibly generated cheaply from a pruned or approximate Krylov process, and
219 define
220 \[
221 B=U^\top A,
222 \qquad
223 F=(I-UU^\top)A,
224 \qquad
225 \delta=\|F\|_2.
226 \]
227 
228 \begin{theorem}[Range-core singular-value certificate]\label{claim:final-22-4}
229 For $A\in\mathbb R^{n\times m}$, list the singular values of $A$ and
230 $B$ in decreasing order and pad both lists with zeros to length $n$.
231 Write these lists as $\sigma_i(A)$ and $\widetilde\sigma_i(B)$,
232 respectively. They are the square roots of the $n$ eigenvalues of
233 $AA^\top$ and $(UB)(UB)^\top$. Then, for $1\le i\le n$,
234 \[
235 \boxed{
236 \left|
237 \sigma_i(A)
238 -
239 \widetilde\sigma_i(B)
240 \right|
241 \le
242 \delta.
243 }
244 \]
245 Consequently,
246 \[
247 \max\{0,\widetilde\sigma_i(B)-\delta\}^2
248 \le
249 \lambda_i(AA^\top)
250 \le
251 \left(
252 \widetilde\sigma_i(B)+\delta
253 \right)^2.
254 \]
255 \end{theorem}
256 
257 \begin{proof}
258 Because \(U\) has orthonormal columns,
259 \[
260 A=UB+F
261 \]
262 and
263 \[
264 \|A-UB\|_2=\|F\|_2=\delta.
265 \]
266 The nonzero singular values of $UB$ and $B$ agree, with multiplicity,
267 and their zero-padded lists agree in the stated ambient convention.
268 The standard singular-value perturbation inequality gives the stated bound.
269 Squaring the nonnegative endpoints gives the eigenvalue interval.
270 \end{proof}
271 
272 This provides a useful architecture:
273 \[
274 \boxed{
275 \begin{gathered}
276 \text{pruned operator for basis discovery}\\
277 \longrightarrow\ \text{exact streamed factor check}\\
278 \longrightarrow\ \text{certified spectral core}
279 \end{gathered}
280 }
281 \]
282 
283 \subsection{A retained negative result}
284 
285 The preceding theorem is exact, but a correct interval need not be useful.
286 
287 In a full-rank \(50\times50\) stress test, a pruned Krylov basis of dimensions
288 \(12\) through \(48\) left range residuals between roughly \(0.87\) and
289 \(0.99\) times the leading singular value.  The corresponding \(10^{-8}\)
290 tail intervals were therefore vacuous or thousands of decades wide.  At
291 dimension \(50\), the range residual fell to approximately
292 \(1.2\times10^{-15}\), and the tail interval collapsed to the exact value.
293 
294 \begin{figure}[htbp]
295 \centering
296 \includegraphics[width=\linewidth]{figures_production/figure_15_range_core_certification.pdf}
297 \caption{Range residual measured against the original factor after basis discovery. Increasing captured dimension reduces unresolved action in this control, but a useful deep-tail bracket still requires a sufficiently small residual. Basis discovery and certification remain separate steps.}
298 \label{fig:range-core-cert}
299 \end{figure}
300 
301 The practical lesson is that range-core certification is a stopping test, not
302 a promise that a severely incomplete basis automatically yields a useful
303 full-spectrum tail bound.
304 
305 
306 
307 \section{Trace-aware residual certification and exact completion}\label{sec:final-23}
308 
309 The spectral bridge in the preceding section used an operator-norm residual as
310 if every unresolved coefficient could move independently by the same amount.
311 That is rigorous but unnecessarily pessimistic once a nontrivial range basis
312 has already been captured.  The residual has considerably more structure.
313 
314 Let \(U\in\mathbb R^{n\times r}\) have orthonormal columns and define
315 \[
316 B=U^\top A,
317 \qquad
318 F=(I-UU^\top)A.
319 \]
320 Then
321 \[
322 A=UB+F,
323 \qquad
324 U^\top F=0.
325 \]
326 
327 \begin{theorem}[Exact core--residual decomposition]\label{claim:final-23-1}
328 \[
329 \boxed{
330 A^\top A
331 =
332 B^\top B+F^\top F.
333 }
334 \]
335 In particular the unresolved spectral term
336 \[
337 R=F^\top F
338 \]
339 is positive semidefinite.
340 \end{theorem}
341 
342 \begin{proof}
343 Expand \((UB+F)^\top(UB+F)\).  The two cross terms vanish because
344 \(U^\top F=0\), while \(U^\top U=I\).
345 \end{proof}
346 
347 This changes the certification problem.  Instead of an arbitrary Hermitian
348 error, the missing term is a positive residual with measurable spectral
349 moments.  Define
350 \[
351 t=\operatorname{tr}R,
352 \qquad
353 v=\operatorname{tr}(R^2),
354 \qquad
355 \rho=\|R\|_2.
356 \]
357 Then
358 \[
359 \boxed{
360  t=\|F\|_F^2,
361  \qquad
362  v=\|FF^\top\|_F^2,
363  \qquad
364  \rho=\|F\|_2^2.
365 }
366 \]
367 The first quantity is the exact missing mean of the Gaussian quadratic form.
368 The second records how concentrated the residual spectrum is. The third is
369 its largest coefficient.
370 
371 \subsection{A trace--Frobenius--cap MGF envelope}
372 
373 Set
374 \[
375 C=B^\top B,
376 \qquad
377 H=C+R,
378 \qquad
379 c=\lambda_{\max}(C).
380 \]
381 For \(0<2\theta(c+\rho)<1\), put
382 \[
383 \alpha=(1-2\theta c)^{-1}.
384 \]
385 
386 \begin{theorem}[Trace--Frobenius--cap log-MGF certificate]\label{claim:final-23-2}
387 For the Gaussian quadratic form with coefficient matrix \(H\),
388 \[
389 \kappa_H(\theta)
390 =-\frac12\log\det(I-2\theta H)
391 \]
392 satisfies
393 \[
394 \boxed{
395 \kappa_H(\theta)
396 \le
397 \kappa_C(\theta)
398 +
399 \theta\alpha t
400 +
401 \frac{\theta^2\alpha^2v}
402      {1-2\theta\alpha\rho}.
403 }
404 \]
405 \end{theorem}
406 
407 \begin{proof}
408 Factor the determinant through the known core:
409 \[
410 I-2\theta(C+R)
411 =
412 (I-2\theta C)^{1/2}
413 (I-2\theta T)
414 (I-2\theta C)^{1/2},
415 \]
416 where
417 \[
418 T=(I-2\theta C)^{-1/2}
419 R
420 (I-2\theta C)^{-1/2}.
421 \]
422 Since
423 \[
424 \|(I-2\theta C)^{-1/2}\|_2^2=\alpha,
425 \]
426 we have
427 \[
428 \operatorname{tr}T\le\alpha t,
429 \qquad
430 \operatorname{tr}(T^2)\le\alpha^2v,
431 \qquad
432 \|T\|_2\le\alpha\rho.
433 \]
434 For every eigenvalue \(x\) of \(T\),
435 \[
436 -\frac12\log(1-2\theta x)
437 \le
438 \theta x
439 +
440 \frac{\theta^2x^2}
441      {1-2\theta\alpha\rho}.
442 \]
443 The scalar inequality follows from the power series of \(-\log(1-u)\) and a
444 geometric bound on all terms of degree at least two.  Summing over the
445 eigenvalues of \(T\) proves the result.
446 \end{proof}
447 
448 \begin{corollary}[Trace-aware Chernoff upper tail]\label{claim:final-23-3}
449 For \(Q=Z^\top HZ\) with \(Z\sim N(0,I)\),
450 \[
451 \boxed{
452 \Pr(Q\ge q)
453 \le
454 \inf_{0<2\theta(c+\rho)<1}
455 \exp\{\widehat\kappa_H(\theta)-\theta q\},
456 }
457 \]
458 where \(\widehat\kappa_H\) is the preceding MGF upper bound.
459 \end{corollary}
460 
461 A complementary lower endpoint is immediate from
462 \[
463 H=C+R\succeq C.
464 \]
465 Using the same normal vector,
466 \[
467 Z^\top HZ\ge Z^\top CZ
468 \]
469 almost surely, and therefore
470 \[
471 \boxed{
472 \Pr(Z^\top CZ\ge q)
473 \le
474 \Pr(Z^\top HZ\ge q).
475 }
476 \]
477 The lower endpoint can be evaluated by K-COS on the captured core spectrum,
478 while the upper endpoint is obtained from the optimized trace-aware Chernoff
479 bound.
480 
481 \subsection{Finite stress test}
482 
483 The previous coefficient-wise Weyl interval was intentionally conservative.
484 On the same full-rank, 50-dimensional stress test used in the preceding
485 section, its \(10^{-8}\) tail interval remained thousands of decades wide
486 until essentially the complete range had been captured.  Preserving the exact
487 residual trace and higher residual moments changes that behavior substantially.
488 
489 \begin{table}[htbp]
490 \centering
491 \caption{Tail-bracket width in decades at a reference probability near \(10^{-8}\).
492 The trace/moment bound is conservative but substantially narrower than
493 coefficient-wise Weyl inflation before full range capture.}
494 \begin{tabular}{rrrr}
495 \toprule
496 Krylov depth & basis dimension & Weyl width & moment width\\
497 \midrule
498 4 & 24 & 90,097 & 11.86\\
499 5 & 30 & 16,511 & 9.76\\
500 6 & 36 & 3,747 & 7.67\\
501 7 & 42 & 2,275 & 5.70\\
502 8 & 48 & 1,165 & 3.39\\
503 \bottomrule
504 \end{tabular}
505 \end{table}
506 
507 \begin{figure}[htbp]
508 \centering
509 \includegraphics[width=\linewidth]{figures_production/figure_16_trace_moment_vs_weyl.pdf}
510 \caption{Range-dependent tail-bracket widths. The symmetric-log scale retains the recorded zero at full range capture. Residual moments preserve the amount and concentration of unresolved spectral mass, instead of assigning every coefficient the same worst-case radius. The first two Weyl widths are infinite and are explicitly marked by arrows rather than plotted as finite data.}
511 \label{fig:trace-moment-vs-weyl}
512 \end{figure}
513 
514 A separate random implementation audit used 120 random factor/range pairs and
515 four admissible positive tilts per pair, for 480 MGF comparisons.  Both the
516 trace/cap and trace--Frobenius--cap envelopes dominated the exact log MGF in
517 every tested case.  The trace--Frobenius--cap form was at least as tight as the
518 trace/cap form in approximately 83.5\% of those comparisons.  This finite
519 sweep audits the implementation. The theorem above supplies the universal
520 argument.
521 
522 \subsection{Residual rank from moments}
523 
524 The same invariants determine when it is better to stop approximating the
525 missing spectrum and complete it exactly.  Let
526 \[
527 s=\operatorname{rank}F=\operatorname{rank}R.
528 \]
529 If the nonzero eigenvalues of \(R\) are \(r_1,\ldots,r_s\), then
530 \[
531 t=\sum_i r_i,
532 \qquad
533 v=\sum_i r_i^2,
534 \qquad
535 r_i\le\rho.
536 \]
537 
538 \begin{theorem}[Residual-rank bracket]\label{claim:final-23-4}
539 \[
540 \boxed{
541 \left\lceil
542 \max\left\{
543 \frac{t}{\rho},
544 \frac{t^2}{v}
545 \right\}
546 \right\rceil
547 \le
548 \operatorname{rank}F
549 \le
550 n-r.
551 }
552 \]
553 The zero-residual case is interpreted separately as rank zero.
554 \end{theorem}
555 
556 \begin{proof}
557 The inequality \(t\le s\rho\) gives \(s\ge t/\rho\).  Cauchy--Schwarz gives
558 \[
559 t^2
560 =
561 \left(\sum_{i=1}^s r_i\right)^2
562 \le
563 s\sum_{i=1}^s r_i^2
564 =sv,
565 \]
566 so \(s\ge t^2/v\).  Finally, every column of \(F\) lies in
567 \(\operatorname{range}(U)^\perp\), whose dimension is \(n-r\).
568 \end{proof}
569 
570 Whenever the integer lower bound equals \(n-r\), the missing rank is certified
571 exactly without computing a residual SVD.
572 
573 \begin{figure}[htbp]
574 \centering
575 \includegraphics[width=\linewidth]{figures_production/figure_17_residual_rank_completion.pdf}
576 \caption{Moment lower bounds, complement upper bounds, and observed residual rank in the full-rank control. From depth three onward the bounds coincide. At depth eight only two residual directions remain, permitting a small exact completion.}
577 \label{fig:residual-rank-completion}
578 \end{figure}
579 
580 \subsection{Exact residual completion}
581 
582 Suppose a compact factorization of the residual is
583 \[
584 F=WD,
585 \]
586 where the columns of $W$ form an orthonormal basis of
587 $\operatorname{range}(F)$. Zero residual directions are omitted.
588 Since this range lies in the orthogonal complement of $U$,
589 \[
590 U^\top W=0.
591 \]
592 
593 \begin{theorem}[Exact residual completion]\label{claim:final-23-5}
594 \[
595 \boxed{
596 A
597 =
598 [U\;W]
599 \begin{bmatrix}
600 B\\D
601 \end{bmatrix}.
602 }
603 \]
604 Consequently, the nonzero singular values of $A$ are exactly the nonzero
605 singular values, with multiplicity, of the stacked completion core
606 \[
607 \mathcal C_{\rm complete}
608 =
609 \begin{bmatrix}
610 B\\D
611 \end{bmatrix}.
612 \]
613 \end{theorem}
614 
615 \begin{proof}
616 The decomposition $A=UB+F$ and the identity $F=WD$ give the factorization.
617 The matrix $[U\;W]$ has orthonormal columns, so
618 $A^\top A=\mathcal C_{\rm complete}^\top\mathcal C_{\rm complete}$.
619 The nonzero singular values therefore agree with multiplicity. If the
620 combined basis contains directions outside $\operatorname{range}(A)$,
621 its row Gram may include additional zeros. Its entire spectrum is the
622 nonzero spectrum of $AA^\top$ only when the combined basis spans exactly
623 $\operatorname{range}(A)$.
624 \end{proof}
625 
626 This identity admits a column-streamed implementation.  For each residual
627 column block, project against the residual basis accumulated so far, append
628 only genuinely new directions through rank-revealing QR or SVD, and extend the
629 coordinate matrices of earlier blocks with zero rows.  New residual directions
630 are orthogonal to every earlier residual block by construction, so no earlier
631 data block must be revisited.
632 
633 In the deterministic stress test, exact residual completion reproduced the
634 full singular spectrum at relative errors between approximately
635 \(2\times10^{-16}\) and \(6\times10^{-16}\) for all tested incomplete bases.
636 The resulting \(10^{-8}\) tail differed from the full-spectrum reference by
637 less than \(10^{-14}\) decades.  At depth 8 the candidate range had dimension
638 48, the missing rank was certified as exactly two, and appending those two
639 residual directions closed the spectrum without another approximate Krylov
640 stage.
641 
642 \subsection{Hybrid stopping rule}
643 
644 Residual information supplies a stopping rule for approximate iteration and
645 a handoff to exact completion:
646 \[
647 \boxed{
648 \begin{array}{c}
649 \text{streamed / pruned Krylov}\\[2mm]
650 \downarrow\\[-1mm]
651 \text{residual moments }(t,v,\rho)\\[2mm]
652 \downarrow\\[-1mm]
653 \begin{cases}
654 \text{continue Krylov}, & \text{residual range still large},\\
655 \text{exact streamed residual completion}, & \text{completion rank affordable}.
656 \end{cases}
657 \end{array}
658 }
659 \]
660 
661 The trace-aware tail certificate remains useful as a rigorous intermediate
662 bound and as a stopping diagnostic.  Once only a small number of residual
663 directions remain, exact completion is mathematically preferable to forcing a
664 worst-case tail envelope to become artificially sharp.
665 
666 
667 \section{Verified matrix-to-spectrum bridge}\label{sec:final-6}
668 
669 A tail enclosure is conditional on the spectrum supplied to it. To certify a
670 matrix-defined problem, the spectrum itself must be enclosed. This section
671 post-verifies a candidate eigensystem against the exact Gram matrix defined
672 by the stored factor entries. Chapter~\ref{ch:intervals} supplies the
673 positive-tail backend used at the endpoint of this construction.
674 
675 \subsection{Binary64 input semantics}
676 
677 Let
678 \[
679 A\in\mathbb R^{n\times m}
680 \]
681 be supplied as an IEEE binary64 array.  Each stored entry is treated as its
682 exact dyadic rational value.  The target operator is therefore the exact Gram
683 matrix
684 \[
685 H=AA^T
686 \]
687 defined by those binary64 values, not an unspecified nearby real matrix.
688 
689 A high-precision symmetric eigensolver is used only to generate candidate
690 quantities
691 \[
692 Q\in\mathbb R^{n\times n},
693 \qquad
694 D=\operatorname{diag}(d_1,\ldots,d_n),
695 \qquad
696 d_1\ge\cdots\ge d_n\ge0.
697 \]
698 No correctness claim depends on trusting this eigensolver.
699 
700 \subsection{Post-certified spectral enclosure theorem}
701 
702 \begin{theorem}[Candidate eigensystem post-certification]\label{claim:final-6-1}
703 Let
704 \[
705 B=QDQ^T.
706 \]
707 Suppose directed-rounding computation proves
708 \[
709 \|Q^TQ-I\|_2\le\eta<1
710 \]
711 and
712 \[
713 \|H-B\|_2\le\rho.
714 \]
715 Then the ordered eigenvalues of the positive semidefinite matrix \(H\) satisfy
716 \[
717 \boxed{
718 \max\{0,(1-\eta)d_i-\rho\}
719 \le
720 \lambda_i(H)
721 \le
722 (1+\eta)d_i+\rho
723 }
724 \]
725 for every \(i\).
726 \end{theorem}
727 
728 \begin{proof}
729 Set
730 \[
731 S=Q^TQ.
732 \]
733 The first hypothesis gives the Loewner inequalities
734 \[
735 (1-\eta)I\preceq S\preceq(1+\eta)I.
736 \]
737 The eigenvalues of
738 \[
739 B=(QD^{1/2})(QD^{1/2})^T
740 \]
741 are the same as those of
742 \[
743 D^{1/2}SD^{1/2}.
744 \]
745 Hence
746 \[
747 (1-\eta)D
748 \preceq
749 D^{1/2}SD^{1/2}
750 \preceq
751 (1+\eta)D,
752 \]
753 and eigenvalue monotonicity yields
754 \[
755 (1-\eta)d_i
756 \le
757 \lambda_i(B)
758 \le
759 (1+\eta)d_i.
760 \]
761 Weyl's perturbation inequality and
762 \(\|H-B\|_2\le\rho\) then give
763 \[
764 |\lambda_i(H)-\lambda_i(B)|\le\rho.
765 \]
766 Combining the two bounds and using \(H\succeq0\) proves the claim.
767 \end{proof}
768 
769 The implementation does not attempt to evaluate the spectral norms above
770 exactly.  Instead it encloses every entry of
771 \[
772 Q^TQ-I
773 \quad\text{and}\quad
774 H-QDQ^T
775 \]
776 with directed-rounding interval arithmetic and uses
777 \[
778 \|M\|_2\le\|M\|_F.
779 \]
780 Thus the reported \(\eta\) and \(\rho\) are conservative certified upper
781 bounds.
782 
783 \subsection{Monotone propagation into the tail}
784 
785 Let the spectral theorem produce
786 \[
787 \ell_i\le\lambda_i(H)\le u_i.
788 \]
789 Using the same independent standard normals in all three sums gives
790 \[
791 \sum_i\ell_iZ_i^2
792 \le
793 \sum_i\lambda_iZ_i^2
794 \le
795 \sum_i u_iZ_i^2
796 \qquad\text{almost surely}.
797 \]
798 Therefore
799 \[
800 \boxed{
801 P\!\left(\sum_i\ell_iZ_i^2\ge q\right)
802 \le
803 P(Q\ge q)
804 \le
805 P\!\left(\sum_i u_iZ_i^2\ge q\right).
806 }
807 \]
808 The lower endpoint is evaluated by the rigorous positive-tail backend on the
809 lower spectrum, and the upper endpoint by the same backend on the upper
810 spectrum.  The controller requires more than two strictly positive
811 coefficients in each endpoint spectrum and a threshold above both endpoint
812 means.  An endpoint spectrum outside these implemented conditions is rejected
813 or reported as unsupported. Monotone coupling itself remains valid.  The final matrix-defined probability interval is accepted only when
814 its multiplicative ratio satisfies the requested accuracy.
815 
816 \subsection{Random dense spectral-containment audit}
817 
818 Three unrelated dense binary64 factors were tested against independently
819 recomputed high-precision eigenvalues of their exact dyadic Gram matrices:
820 
821 \begin{center}
822 \begin{tabular}{@{}rrrr@{}}
823 \toprule
824 factor size & all eigenvalues contained & maximum relative width & time (s)\\
825 \midrule
826 $12\times18$ & yes & $3.36\times10^{-58}$ & 0.09\\
827 $20\times30$ & yes & $1.44\times10^{-57}$ & 0.35\\
828 $28\times36$ & yes & $1.20\times10^{-56}$ & 0.80\\
829 \bottomrule
830 \end{tabular}
831 \end{center}
832 
833 No reference eigenvalue fell outside its certified interval.
834 
835 \subsection{End-to-end matrix-defined tail near \texorpdfstring{\(10^{-16}\)}{1e-16}}
836 
837 A dense \(64\times64\) exact-binary factor was constructed from a normalized
838 Hadamard basis with four singular-value groups.  The stored binary64 entries
839 are exact dyadic rationals.  The spectral postcheck returned
840 \[
841 \eta\le1.65\times10^{-49},
842 \qquad
843 \rho\le9.18\times10^{-50}.
844 \]
845 The leading coefficient, whose exact value is one in this control,
846 was enclosed with a width of order $10^{-49}$. The full outward-rounded
847 endpoints are preserved in the spectral record. Ellipsized decimal strings
848 are not used as interval endpoints.
849 
850 At
851 \[
852 q=131.33201485100517,
853 \]
854 the tail lies near \(10^{-16}\).  Starting from the factor matrix itself:
855 
856 \begin{center}
857 \begin{tabular}{@{}rrr@{}}
858 \toprule
859 requested relative accuracy & achieved ratio minus one & certified\\
860 \midrule
861 $10^{-10}$ & $2.60\times10^{-12}$ & yes\\
862 $10^{-12}$ & $4.09\times10^{-15}$ & yes\\
863 \bottomrule
864 \end{tabular}
865 \end{center}
866 
867 For the \(10^{-12}\) request, the final enclosure was approximately
868 \[
869 \log_{10}p
870 \in
871 [-15.99999999999996625,
872  -15.99999999999996447].
873 \]
874 
875 This closes the basic numerical chain
876 \[
877 \boxed{
878 \text{binary64 factor}
879 \longrightarrow
880 \text{certified spectrum}
881 \longrightarrow
882 \text{certified deep-tail interval}
883 }
884 \]
885 at moderate matrix dimension.
886 
887 \subsection{Scalability boundary}
888 
889 The theorem applies in every finite dimension, but the present verifier forms a full candidate
890 basis \(Q\) and postchecks dense matrices.  It therefore closes the correctness
891 boundary before it closes the large-scale memory boundary.  For very large streamed factors, a memory-bounded guarantee would require a
892 verified range-core/residual certificate and an interval completion step in
893 place of the full-basis postcheck. Those extensions are not part of the
894 implemented dense verifier.
895 
896 
897 

Back to source controls

Back to COS Method