COS Method

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Included manuscript sections

• replay_results.tex

Read the typeset paper

Read this chapter with formatted equations

1 \chapter{Computation and reproducibility}\label{app:reproduction}
2 
3 \section{Reference pseudocode}\label{sec:final-A}
4 
5 For weighted blocks before residualization, \texttt{project} applies the
6 fixed projector $M_X$. For already residualized factor blocks, use the
7 identity default. The listing is a binary64 reference implementation of the
8 streamed identity, not an interval-arithmetic proof of that identity. The
9 tail import is available when \path{engine/} is on the Python import path.
10 
11 \begin{lstlisting}[language=Python]
12 import numpy as np
13 from accuracy_driven import certified_positive_logsf
14 
15 def stream_KV(block_source, V, project=lambda x: x):
16     U = project(np.asarray(V, dtype=np.float64))
17     Y = np.zeros_like(U, dtype=np.float64)
18     for A_block in block_source:
19         Y += A_block @ (A_block.T @ U)
20     return project(Y)
21 
22 def certified_tail(q, spectrum, relative_accuracy):
23     # Refines support, COS modes, and interval precision.
24     # Returns certified=False if the requested accuracy is not proved.
25     return certified_positive_logsf(
26         q, spectrum, relative_accuracy=relative_accuracy
27     )
28 \end{lstlisting}
29 
30 
31 \section{Executable layers}\label{sec:final-B}
32 The accompanying package contains the Python engine, deterministic tests,
33 recorded numerical inputs, and the pinned Lean companion. The programs are
34 research implementations with precisely stated numerical contracts. They are
35 not presented as a measured native GPU production runtime.
36 
37 \begin{longtable}{@{}P{.40\linewidth}P{.55\linewidth}@{}}
38 \toprule
39 Module & Responsibility\\
40 \midrule
41 \endhead
42 \path{quadratic_form_engine.py} & Central and positive noncentral interfaces.\\
43 \path{accuracy_driven.py} & Refinement and fail-closed acceptance.\\
44 \path{interval_kcos.py} & Directed positive-spectrum tail enclosures.\\
45 \path{directed_accuracy.py} & Directed ratio tests and outward serialization.\\
46 \path{verified_spectrum.py} & Dense candidate-eigensystem post-verification.\\
47 \path{generalized_tail.py} & Signed and noncentral floating paths.\\
48 \path{residual_completion.py} & Completion of unresolved factor range.\\
49 \path{streaming_skat.py} & Replayable factor and kernel actions.\\
50 \bottomrule
51 \end{longtable}
52 
53 \section{Names used by the implementation}
54 The analysis uses $\kappa(s)$, $b$, $J_k$, and $N$. The numerical source retains the names \texttt{K(s)} for the cumulant, \texttt{U} for the support endpoint, \texttt{I\_k} for the payoff integral, and \texttt{K} for the integer mode count. These names do not denote additional mathematical objects. The exact inputs and serialized output intervals determine the calculation.
55 
56 \section{Replayed numerical controls}\label{app:fresh-validation}
57 The release replay executes all six regression groups on the supplied
58 engine, including the interval-width reporting tests, and runs both
59 independent containment controls. Its record identifies the environment,
60 commands, source hashes, test counts, and outcomes. The engine source was
61 unchanged during this execution. These results are separate from the
62 recorded timing experiments in the main text.
63 
64 The release records are in \path{verification/closing/}. Earlier reports
65 remain as provenance, not as substitutes for this replay.
66 
67 \input{replay_results.tex}
68 
69 A successful finite replay is evidence about those executions. It is not a
70 proof of all inputs or of the arithmetic library. Directed enclosures rely on
71 the stated interval arithmetic and transcendental implementation. The shared
72 interval-precision context requires sequential calls. Floating summary fields
73 are display values. Widths and multiplicative-ratio summaries are computed
74 before conversion to binary64, avoiding cancellation between rounded endpoint
75 summaries. The outward decimal endpoint strings carry the numerical enclosure,
76 and directed acceptance uses those strings rather than the display fields.
77 
78 \section{Why parsing and output are part of the proof obligation}
79 An interval can be valid internally and become invalid when printed. A narrow
80 logarithmic width can also disappear if it is first evaluated in an
81 insufficient point-precision context. The implementation therefore preserves
82 literal interval endpoints, compares an upper bound on the multiplicative
83 ratio with a lower bound on the requested tolerance, and serializes the lower
84 and upper endpoints outward. Unsupported domain inputs are rejected rather
85 than admitted to a formula outside its hypotheses.
86 
87 \section{Figure and data provenance}\label{app:provenance}
88 All fifty graphics are supplied as vector PDF and editable SVG files. The
89 plots use recorded measurements, explicit storage models, or declared finite
90 illustrations. Their plotting sources and input hashes are included, and
91 the figure labels distinguish these evidence types. The fixed-resolution
92 interval-width figure is regenerated from full outward endpoint strings,
93 with its exact inputs, computed widths, and plotting code retained in the
94 proofreading record. The visual atlas
95 uses declared finite models and its own reproducible Python generators.
96 These are distinct sources of evidence. A diagram of an exact identity is
97 not a new runtime benchmark, and a replacement layout is not a new numerical
98 experiment.
99 
100 Two retained empirical illustrations need a particular qualification. The raw
101 singular-value vectors for the phase-rank and QR illustrations were not retained. Their
102 displays use the recorded rank audit and QR discrepancy audit rather than inventing
103 missing samples. The packet illustration in Chapter~\ref{ch:packets} instead uses a
104 fully declared four-coefficient example with reproducible complex-grid evaluations.
105 The captions identify the available rank and discrepancy evidence.
106 
107 \section{Reproducing the running example}
108 The four-dimensional factor, block actions, Gaussian law, and saddlepoint identity are checked symbolically. The packet comparison is evaluated at high precision. The positive tail is enclosed with directed arithmetic and compared with an independent interval for the closed-form survival probability. A failed fixed-resolution decision is retained, followed by the successful mode refinement.
109 \begin{lstlisting}
110 python illustrations/worked_example.py
111 \end{lstlisting}
112 The script writes its declared figures and machine-readable results. It does not replace the existing test suite or establish performance for larger problems. To regenerate the publication graphics from their declared sources, run
113 \begin{lstlisting}
114 python illustrations/production_figures.py
115 \end{lstlisting}
116 
117 \section{Rebuilding and replaying}
118 Run the document builder from the package root:
119 \begin{lstlisting}
120 python build.py
121 \end{lstlisting}
122 It compiles the editable LaTeX source and writes the monograph PDF. A TeX
123 installation with the packages listed in the source is required.
124 
125 Run the numerical replay separately:
126 \begin{lstlisting}
127 python replay.py --include-controls
128 \end{lstlisting}
129 The replay writes separate logs. The \path{lean/} directory contains the pinned formal source and retained compiler evidence. Compiler and dependency caches are not bundled. Reproduction requires the exact pinned toolchain and dependencies.
130 
131 \section{Scope of the publication checks}
132 The closing audit checks source correspondence, figure-data provenance,
133 labels and references, navigation, and page geometry. It also records the
134 fresh numerical replay and finite algebra controls. Rendered pages are
135 inspected separately from those programmatic checks. No new hardware
136 benchmark is claimed.
137 
138 The Lean compiler was unavailable in the closing environment. The formal
139 sources and retained compiler evidence are unchanged, and no new Lean
140 compilation is claimed. Neither a successful finite replay nor a publication
141 audit establishes an end-to-end formal proof of the numerical implementation.
142 
143 To verify the delivered files and repeat the publication audit, run:
144 \begin{lstlisting}
145 python verify_manifest.py
146 python audit.py
147 \end{lstlisting}

Back to source controls

Back to COS Method