How to read this book

For the complete matrix-to-tail route, read the chapters in order. For a supplied spectrum, read the Gaussian reductions in Chapter 1, then Chapters 6–10. The intervening operator chapters explain what must be established when the spectrum is not already known.

A recurring example begins in Section 1.5 with an exact dyadic factor and spectrum \((1,1,2,2)\). Section 2.9 changes its storage partition. Section 6.3 derives the tilt and packets. Section 9.6 completes the enclosure and compares it with a closed-form probability.

Permalink · Source line 18

A directed calculation returns an outward interval \([p_-,p_+]\). Requested multiplicative tolerance \(\varepsilon>0\) is accepted only if \(p_->0\) and

A plausible point estimate can still fail this test. Failure means that the requested accuracy was not certified. Agreement with an independent value is useful evidence, but cannot replace the interval inequality.

The supplied directed backend requires an exact positive spectrum with rank greater than two, a nonnegative threshold, an admissible positive tilt, and a support endpoint above the threshold. Its automatic planner handles queries above the mean. The analytic packet theory has broader rank coverage, but its binary64 implementation does not inherit a directed-rounding guarantee.

For matrix inputs, certification targets the exact Gram matrix of the stored binary64 factor. Preprocessing and statistical-model validity are separate obligations. Signed and noncentral reductions are exact mathematics, but their supplied numerical paths have narrower guarantees than the positive directed backend.

Appendix B identifies the finite-algebra and order statements represented in Lean. Appendix C gives reproducible computations and their trust assumptions. Neither finite tests nor the limited formal companion establish end-to-end correctness of every layer.

Permalink · Source line 23