C Computation and reproducibility
On this page · Permalink · Source line 1
C.1 Reference pseudocode
On this page · Permalink · Source line 3
For weighted blocks before residualization, project applies the fixed projector \(M_X\). For already residualized factor blocks, use the identity default. The listing is a binary64 reference implementation of the streamed identity, not an interval-arithmetic proof of that identity. The tail import is available when engine/ is on the Python import path.
import numpy as np
from accuracy_driven import certified_positive_logsf
def stream_KV(block_source, V, project=lambda x: x):
U = project(np.asarray(V, dtype=np.float64))
Y = np.zeros_like(U, dtype=np.float64)
for A_block in block_source:
Y += A_block @ (A_block.T @ U)
return project(Y)
def certified_tail(q, spectrum, relative_accuracy):
# Refines support, COS modes, and interval precision.
# Returns certified=False if the requested accuracy is not proved.
return certified_positive_logsf(
q, spectrum, relative_accuracy=relative_accuracy
)C.2 Executable layers
On this page · Permalink · Source line 31
The accompanying package contains the Python engine, deterministic tests, recorded numerical inputs, and the pinned Lean companion. The programs are research implementations with precisely stated numerical contracts. They are not presented as a measured native GPU production runtime.
| Module | Responsibility |
|---|---|
quadratic_form_engine.py | Central and positive noncentral interfaces. |
accuracy_driven.py | Refinement and fail-closed acceptance. |
interval_kcos.py | Directed positive-spectrum tail enclosures. |
directed_accuracy.py | Directed ratio tests and outward serialization. |
verified_spectrum.py | Dense candidate-eigensystem post-verification. |
generalized_tail.py | Signed and noncentral floating paths. |
residual_completion.py | Completion of unresolved factor range. |
streaming_skat.py | Replayable factor and kernel actions. |
C.3 Names used by the implementation
On this page · Permalink · Source line 53
The analysis uses \(\kappa(s)\), \(b\), \(J_k\), and \(N\). The numerical source retains the names K(s) for the cumulant, U for the support endpoint, I_k for the payoff integral, and K for the integer mode count. These names do not denote additional mathematical objects. The exact inputs and serialized output intervals determine the calculation.
C.4 Replayed numerical controls
On this page · Permalink · Source line 56
The release replay executes all six regression groups on the supplied engine, including the interval-width reporting tests, and runs both independent containment controls. Its record identifies the environment, commands, source hashes, test counts, and outcomes. The engine source was unchanged during this execution. These results are separate from the recorded timing experiments in the main text.
The release records are in verification/closing/. Earlier reports remain as provenance, not as substitutes for this replay.
| Regression group | Tests | Result |
|---|---|---|
| Streaming, phases, pruning, residuals, and case study | 31 | pass |
| Directed positive COS interval backend and width reporting | 5 | pass |
| Accuracy-driven positive controller | 2 | pass |
| Verified dense spectrum and matrix-to-tail bridge | 4 | pass |
| Signed and noncentral analytic-ledger engines | 8 | pass |
| Directed acceptance and endpoint serialization | 10 | pass |
| Total | 60 | pass |
All 60 test methods passed, with no failures, errors, or skips. Test methods can contain multiple subcases, so this is not an assertion count. Source hashes before and after the replay agree.
The exact-spectrum control \(0.02\chi^2_{80}\) near \(10^{-5000}\) met a requested multiplicative tolerance of \(10^{-18}\). Its directed ratio upper bound was less than \(9.202\times10^{-20}\), and an independently evaluated finite Erlang log interval was fully contained in the returned interval.
The dense \(64\times64\) exact-binary64 Hadamard-factor control near \(10^{-16}\) met a requested tolerance of \(10^{-12}\). All 64 known exact eigenvalues were enclosed. The final directed probability ratio upper bound was less than \(2.783\times10^{-15}\). These displayed bounds are rounded upward. The full outward endpoints and literal inputs are in the accompanying control record.
A successful finite replay is evidence about those executions. It is not a proof of all inputs or of the arithmetic library. Directed enclosures rely on the stated interval arithmetic and transcendental implementation. The shared interval-precision context requires sequential calls. Floating summary fields are display values. Widths and multiplicative-ratio summaries are computed before conversion to binary64, avoiding cancellation between rounded endpoint summaries. The outward decimal endpoint strings carry the numerical enclosure, and directed acceptance uses those strings rather than the display fields.
C.5 Why parsing and output are part of the proof obligation
On this page · Permalink · Source line 78
An interval can be valid internally and become invalid when printed. A narrow logarithmic width can also disappear if it is first evaluated in an insufficient point-precision context. The implementation therefore preserves literal interval endpoints, compares an upper bound on the multiplicative ratio with a lower bound on the requested tolerance, and serializes the lower and upper endpoints outward. Unsupported domain inputs are rejected rather than admitted to a formula outside its hypotheses.
C.6 Figure and data provenance
On this page · Permalink · Source line 87
All fifty graphics are supplied as vector PDF and editable SVG files. The plots use recorded measurements, explicit storage models, or declared finite illustrations. Their plotting sources and input hashes are included, and the figure labels distinguish these evidence types. The fixed-resolution interval-width figure is regenerated from full outward endpoint strings, with its exact inputs, computed widths, and plotting code retained in the proofreading record. The visual atlas uses declared finite models and its own reproducible Python generators. These are distinct sources of evidence. A diagram of an exact identity is not a new runtime benchmark, and a replacement layout is not a new numerical experiment.
Two retained empirical illustrations need a particular qualification. The raw singular-value vectors for the phase-rank and QR illustrations were not retained. Their displays use the recorded rank audit and QR discrepancy audit rather than inventing missing samples. The packet illustration in Chapter 6 instead uses a fully declared four-coefficient example with reproducible complex-grid evaluations. The captions identify the available rank and discrepancy evidence.
C.7 Reproducing the running example
On this page · Permalink · Source line 107
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.
python illustrations/worked_example.pyThe 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
python illustrations/production_figures.pyC.8 Rebuilding and replaying
On this page · Permalink · Source line 117
Run the document builder from the package root:
python build.pyIt compiles the editable LaTeX source and writes the monograph PDF. A TeX installation with the packages listed in the source is required.
Run the numerical replay separately:
python replay.py --include-controlsThe replay writes separate logs. The 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.
C.9 Scope of the publication checks
On this page · Permalink · Source line 131
The closing audit checks source correspondence, figure-data provenance, labels and references, navigation, and page geometry. It also records the fresh numerical replay and finite algebra controls. Rendered pages are inspected separately from those programmatic checks. No new hardware benchmark is claimed.
The Lean compiler was unavailable in the closing environment. The formal sources and retained compiler evidence are unchanged, and no new Lean compilation is claimed. Neither a successful finite replay nor a publication audit establishes an end-to-end formal proof of the numerical implementation.
To verify the delivered files and repeat the publication audit, run:
python verify_manifest.py
python audit.py