13 Implementation and verification
On this page · Visual guide: What this edition certifies · Permalink · Source line 2030
The release contains a small reference implementation of the exact operators and optimization algorithms used in the paper. The mathematical interface is deliberately narrow. This Python implementation is a numerical prototype, not extracted Lean code. Its stored-key support can retain zero-valued blocks, whereas the exact support graph uses nonzero blocks. Its reduced numerical QR is not the exact rank-compact range construction proved in Appendix F. Prototype tests and theorem proofs therefore have different targets.
A packet layout records dimensions and coordinate slices.
A packet operator stores active blocks and evaluates them without materializing inactive blocks.
BDLR factors support exact application, product, solve, and small core recompression.
Graph utilities compute support products, path closure, Schur fill inclusion, and topological levels.
Tree dynamic programs solve the Lagrangian and quantized budget models.
A multiple choice dynamic program assigns discrete precision options.
Benchmark utilities audit case identity, output contracts, timing scopes, and retained negative controls.
The strengthened release records a deterministic verifier with \(37392\) checks in nine groups. It covers packet evaluation, adjoints, composition, structured primitives, recompression optimality, product chain error, graph support, Schur fill, tree compilation, precision assignment, and the benchmark corpus. The strengthened release records eleven passing unit tests and twenty three passing original-source tests for BDLR operations, Krylov methods, mixed precision, measured data schema, and figure generation.
| Layer | Verification target |
|---|---|
| Packet semantics | materialization, application, adjoint, composition |
| Low rank algebra | exact product, Woodbury solve, optimal core recompression |
| Graph algorithms | path support, topological levels, Schur fill inclusion |
| Optimization | Lagrangian tree compiler, budget compiler, precision assignment |
| Numerical bounds | product chain error, block perturbation, clipped allocation |
| Empirical corpus | row count, suite count, device split, status, error ceiling |
| Document | proofs, labels, citations, figures, font embedding, render audit |