Paper V: Implementation and reproducibility

16 Implementation and reproducibility

On this page · Permalink · Source line 1301

The companion package is organized by mathematical layer:

Numerical companion modules.
module	implemented content
`polyphase.py`	residue projectors, analysis/synthesis, refinement, exact FIR transfer kernels, polyphase convolution
`filterbanks.py`	Haar analysis/synthesis, complete Haar packet trees, energy accounting, predict–update lifting
`adaptive.py`	complete-pruning enumeration, exact mixed-depth synthesis, dynamic-programming optimization, and stability certificates
`edges.py`	one- and two-dimensional Fourier truncation, known-packet reconstruction, narrow two-class estimators, harmonic filling, error metrics
`smith.py`	Cayley coordinates, cyclic Möbius action, Smith circles, sensitivity weight, coefficient projectors
`nonlinear.py`	coefficient packets, cyclic product convolution, nonlinear shifted packet reconstruction
`experiments.py`	all machine-readable numerical certificates and tabular summaries
`visuals.py`	the eighteen figure pairs used in the paper

Permalink · Source line 1305

The September 2026 release records recovery and rerunning of the original companion source: its 33 tests passed, and all 18 figure pairs and numerical tables were regenerated. The Lean package contributes 20 independent exact-model tests and 16 tests of the verifier itself; these account for another 36 passing tests. The exact-model suites count 305,933 assertions. These counts are separate from the 225 Lean theorem targets.

All numerical computations are CPU-based. Floating-point residuals measure finite implementations and may vary at rounding level with the scientific libraries. The universal mathematical statements are supported by the Lean proofs; the Python modules are not compiled or verified by Lean. The adaptive-tree certificate uses floating-point costs and an exhaustive finite comparison, so its displayed gap is numerical evidence rather than an interval-arithmetic proof about those computed costs. Appendix Section D explains the verification boundary.

Permalink · Source line 1326

Numerical certificate 16.1: Finite numerical residuals

The largest recorded residuals were

\[ \begin{array}{lr} \toprule \text{identity}&\text{residual}\\ \midrule \text{polyphase reconstruction}&0\\ \text{nested refinement}&0\\ \text{polyphase convolution}&4.44\times10^{-16}\\ \text{Haar reconstruction}&8.88\times10^{-16}\\ \text{wavelet-packet reconstruction}&2.22\times10^{-15}\\ \text{adaptive-tree optimum versus exhaustive search}&0\\ \text{adaptive mixed-depth synthesis}&8.88\times10^{-16}\\ \text{lifting reconstruction}&4.44\times10^{-16}\\ \text{Smith rotation conjugacy}&3.34\times10^{-16}\\ \text{Smith impedance--admittance duality}&0\\ \text{nonlinear product-packet reconstruction}&1.33\times10^{-15}\\ \text{nonlinear shifted-filter reconstruction}&0\\ \bottomrule \end{array} \]

The Haar and wavelet energy residuals were \(5.68\times10^{-14}\) and \(2.27\times10^{-13}\), respectively.

Permalink · Source line 1330 · Claim record · Lean coverage · Code · Worked examples

Source and conversion record

Source SHA-256: 5d3c6b2e5709c37ea551eb8fd1d823e5249c5fbc411d36b806241af4df888f36

Unsupported prose commands stop the build. The mathematical expression sequence is checked against the source, with manuscript macros expanded for display.

Conversion records

Read and explore

Proofs and implementation

About this work

Other resources

16 Implementation and reproducibility

Numerical certificate 16.1: Finite numerical residuals