D Formalization and reproducibility record
On this page · Visual guide: An atlas of the objects · Visual guide: What the reader can now verify · Visual guide: What the extended developments add · Permalink · Source line 1479
D.1 What has been checked
On this page · Permalink · Source line 1481
The preserved Part I manuscript has twenty theorem-like statements: Theorems, Propositions, and Corollaries, counted together. The Lean project contains 225 explicit supporting theorem targets in 23 proof modules. All twenty statements have an explicit scope row and principal declaration targets. The September 2026 release records a successful build and axiom audit with warnings treated as errors. No fresh Lean build is asserted for this October final edition. The audit inspected all 827 declarations in the project namespace, including definitions and automatically generated declarations. The latter is an implementation census, not a count of 827 mathematical theorems.
The accepted axiom dependencies are propext, Classical.choice, and Quot.sound. No admitted proof or additional project axiom is permitted. The verifier checks the imported modules, registered theorem inventory, dependency pins, source hashes, and coverage of the twenty-row scope contract. Its successful status is LEAN_CHECKS_PASS. The correspondence between a mathematical sentence in this PDF and its Lean type is a manual mathematical review, not an automated semantic-equivalence test.
The source-level formalization was completed before this manuscript revision. The revision integrates those checked hypotheses and conclusions into the paper itself; it does not increase the Lean theorem count by counting editorial changes as new proofs. Eleven foundational formal-power-series proofs in CyclicSeries are adaptations of Paper IV and are identified as such in the provenance record.
D.2 Result-by-result correspondence
On this page · Permalink · Source line 1489
The following table summarizes the reviewed statement boundary. Full qualified declaration names, source locations, and supplementary targets appear in MANUSCRIPT_TARGET_MAP.md and the machine-readable scope contract. Every row below has supporting kernel-checked declarations; numerical certificates, classical-input paragraphs, remarks, and conjectures are not additional theorem rows.
| Result | Principal modules | Checked mathematical content |
|---|---|---|
| Theorem 1.1 | HilbertPackets | Complex \(\ell^2\) impulse expansion, finite-support identity, unitary shifts, and closed shift-generated span. |
| Theorem 2.1 | HilbertPackets | Bounded self-adjoint residue projectors, pairwise annihilation, completeness, and orthogonal ranges. |
| Corollary 2.2 | IntegerPolyphase; HilbertPackets | Signed quotient/remainder coordinates, both inverse identities, and the joint Hilbert norm of the channels. |
| Theorem 2.3 | HilbertPackets | Literal bounded-projector refinement for positive divisible moduli. |
| Theorem 3.1 | FIRTransfer; ZTransform | Finite-support tap reindexing for all bilateral inputs; numerical channel transforms under weighted absolute summability. |
| Theorem 4.1 | FilterBank; FiniteTransforms | Finite Laurent/FIR bank composition, faithful action on sequences, gain-delay reconstruction criterion, and the \(Nd\) original-sample delay. |
| Corollary 4.2 | HaarChannels; HaarHilbert | Literal even/odd input samples, normalized complex low/detail channels, and \(\ell^2\) energy equality. |
| Theorem 4.3 | Lifting; FiniteTransforms | Predict/update inverse maps, determinant one, and both flat finite-signal inverse identities. |
| Theorem 5.1 | WaveletPackets | Every finite depth of literal Haar packet operators, energy equality, and reconstruction using actual Hilbert adjoints. |
| Theorem 6.1 | KnownEdge | Exact cancellation of one retained packet, and equality of approximation errors. |
| Corollary 6.2 | KnownEdge | Finite families of retained packets, with no geometry assumption on the packets. |
| Theorem 7.1 | MaskPerturbation | Measurable-mask symmetric-difference norm, extended finite-\(p\) error bound, pointwise and essential supremum bounds, and smooth-background error. |
| Theorem 11.2 | CompletePrunings; PruningSums | Recursive cuts correspond to complete covering antichains; literal finite node sums preserve synthesis. |
| Theorem 11.3 | PruningSums | Finite arbitrary-objective minimization, attained positive gap with competitors, strict stability, and the singleton case. |
| Theorem 11.4 | FiniteAdaptive; PruningAlgorithm | Deterministic stop-on-ties selector, global optimum, arbitrary positive finite branching, and the stated unit-operation count. |
| Corollary 11.5 | PruningSums; PruningAlgorithm | Attained maximum error envelope, optimal-value perturbation, strict-gap selector stability, and probability transfer from a joint event. |
| Theorem 12.1 | CyclicSeries | Formal Cauchy-product residue convolution and the finite-tuple power identity, including the empty product at exponent zero. |
| Theorem 13.2 | SmithAction; SmithCyclic | Nonzero homogeneous pairs modulo scaling, Cayley conjugacy, the actual exponential phase, and cyclic composition on the projective line. |
| Corollary 13.3 | SmithCyclic | Two-phase coordinate swap, \(0\leftrightarrow\infty\), and finite impedance inversion when \(z\ne0\). |
| Proposition 14.1 | CRT | Signed integer residue-mask factorization for coprime moduli, including the dyadic–odd case. |
The remaining foundational modules Packets, FiniteSelection, and BinaryAdaptive provide generic coordinate, finite-minimum, and binary-tree lemmas used or retained alongside the concrete constructions. The Hilbert target is the square-summable space on a product of indices; it is not the supremum-norm function space that Lean would otherwise assign to an unqualified finite family of channels.
D.3 Three bridges that matter for the statement
On this page · Permalink · Source line 1528
Finite filters and numerical transforms.
On this page · Permalink · Source line 1530
The filter-bank proof is an algebraic theorem about finite Laurent-polynomial kernels acting faithfully on bilateral sequences. Equality at a single complex value of \(z\) would be insufficient to prove a polynomial identity; the impulse argument avoids that error. The separate transform theorem proves the finite-filter action agrees with evaluation wherever the weighted input series converge absolutely. An arbitrary bilateral \(\ell^2\) sequence need not have an absolutely convergent numerical \(z\)-transform. The all-sequence time-domain theorem makes no such assumption.
Recursive trees and set-valued prunings.
On this page · Permalink · Source line 1533
The formal tree permits any positive finite arity at an internal node, including arity one. A node has a position in the tree, so equal data labels on distinct nodes do not identify the nodes. A recursive cut is either a stop or a collection of child cuts. Its equivalence with a covering antichain is proved in both directions. The cost, envelope, and operator sums are then shown to equal actual finite sums over the selected node set. This connects the recursive optimizer to the manuscript's set-valued definition instead of assuming that connection.
Hilbert operators and finite experiments.
On this page · Permalink · Source line 1536
The coordinate maps, literal Haar channels, and packet operators are constructed on complex \(\ell^2\). Square summability and boundedness are established before adjoints are used. The finite Python experiments separately check indexing, reconstruction, and energy at finite lengths. They illustrate these operators but are not the objects executed by the Lean kernel. Likewise, the Python Smith routine evaluates only finite charts; the Lean projective construction supplies the pole-safe universal statement.
D.4 September 2026 checks and numerical conventions
On this page · Permalink · Source line 1539
| Check family | Accepted count |
|---|---|
| Original numerical companion tests | 33 |
| Independent exact-model tests | 20 |
| Verifier positive and negative controls | 16 |
| Total tests in these three families | 69 |
| Exact assertions inside the independent model suites | 305,933 |
| Registered Lean theorem targets | 225 |
| Lean proof modules | 23 |
| Regenerated figure pairs | 18 |
The September 2026 record states that all scalar entries in the recovered numerical-results JSON reproduced exactly in its environment. This includes the 458,330-pruning depth-five comparison, its selected six-node pruning, the optimum gap, and the reconstruction residuals. The five Fourier sparse-approximation budgets were also checked for conjugate-pair closure. The revised figures and tables use the regenerated data. This exact replay of the stored floating-point numbers is stronger than a visual similarity check, but it is not a promise of bitwise equality on every platform.
For the one-dimensional low-pass experiment, “cutoff 18” means 37 signed frequency bins, not 18 retained coefficients. The disk experiment uses a square \(33\times33\) frequency mask, not a radial cutoff. The sparse comparison uses largest-coefficient budgets instead of either low-pass convention. The full-image and boundary-band RMSEs are normalized by the number of samples in the respective comparison set. The supplied inpainting routines perform a fixed finite number of periodic neighbor-averaging iterations; “harmonic filling” describes that iteration, not a separately proved exact continuum Dirichlet solver.
The independent exact-model suite checks signed polyphase/FIR addresses, exact lifting and normalized Haar arithmetic, mask bounds, and exhaustive finite-tree objectives. Its tree census includes all 626 ordered rooted tree shapes with one through eight nodes and 129,958 node subsets. These finite checks can catch implementation or convention errors; they are not substitutes for the universal Lean proofs. The verifier controls exercise failure paths, including incomplete scope contracts and unregistered proof targets. Mandatory verification conditions use explicit exceptions rather than Python assertions, so optimized Python cannot silently remove them.
D.5 Pinned environment and rerunning the release
On this page · Permalink · Source line 1564
The Lean toolchain is leanprover/lean4:v4.34.0-rc2. The project pins mathlib to aeb72f1e9981b6d35b426b16dca7759be3e7ba06. The Lake manifest records the remaining dependency revisions. The numerical environment versions are recorded in verification/numerical_environment.json. Source and artifact hashes appear in SHA256SUMS.txt. The original manuscript, source, numerical data, and figures remain available under provenance for comparison; the expanded PDF and its TeX are the manuscript of that September 2026 release.
From the preserved release root (source/complete/original_snapshot in the final package), the combined verification entry point is:
python3 VERIFY_PAPER.pyThis runs the Lean verifier, companion tests, numerical regeneration/comparison, and manuscript consistency checks. Lean, Lake, the pinned dependencies, the Python requirements, and a TeX installation must be available for the corresponding full checks. Missing prerequisites or failed checks return failure; static checks alone never report kernel verification. The individual numerical generation command is
cd companion
python3 run_all.py
python3 -m pytest -q testsThe TeX source resolves the eighteen vector figures from the manuscript's figure directory. The checked build uses repeated pdfLaTeX passes, then text, cross-reference, and page-render inspection. Different pdfTeX versions can produce different binary PDF hashes even when the rendered document is unchanged.
In the September 2026 release environment, a disclosed runtime adapter was needed for Lean executable-path discovery: it redirects a read of the current process's numeric /proc executable link to /proc/self/exe. It does not modify the Lean binary, elaborator, kernel, axioms, or proof terms. The adapter source and invocation are retained with the verification evidence; ordinary installations can run the pinned toolchain directly.
D.6 What remains open
On this page · Permalink · Source line 1584
The September 2026 finite theorem scope is complete in the stated sense: all twenty theorem-like statements have reviewed, accepted formal counterparts, and that release records a rerun of the numerical companion. The two edge-recovery conjectures remain open research directions. No universal segmentation theorem, infinite-tree consistency result, minimax rate, or optimal Smith sampling theorem is inferred from the finite results. Classical Smith-grid and transmission-line formulae provide application context; those physical and historical assertions are not additional Lean-certified theorem rows.
Across the available Papers I–V manuscripts there are 168 theorem-like results. Their release maps contain 1,456 raw theorem targets; removing two shared qualified names and eleven known Paper-IV-to-V adaptations leaves 1,443 after those known duplicate removals. This is a source census, not a claim of that many independent or novel mathematical results. Papers I–IV were counted from their release material and bundled audit records; only Paper V was freshly built for that September 2026 release. These historical cross-paper counts are not a current census of the October final companions.