Reading orientation
Part I. The twenty-result formal core develops exact polyphase reconstruction, filter transfers, Hilbert packet operators, finite adaptive trees, edge error bounds, and Smith coordinates.
Part II. The complete extended development treats lattice coordinates, stable banks, singular packets, separated jump recovery, geometric error bounds, and multiscale localization.
Visual atlas. Forty worked plates close the volume. The separate visual guide provides the same examples, and the Lean guide gives the precise released formal contract.
Reading this edition
On this page · Permalink · Source line 227
The two branches of Paper V answer related questions at different levels. Part I preserves the twenty results and twenty proofs of the later v1.1.0 manuscript. Part II preserves the broader standalone development with its sixty-three proofs and E-prefixed section numbers. Their overlap is intentional. The combined eighty-three proofs are a record of the two complete branches, rather than eighty-three independent or novel results.
For a first reading, follow Part I Sections 1–7. These sections establish the coordinate maps, filter transfers, exact reconstruction, and the separation of packet error from smooth approximation error. Section 11 develops finite adaptive selection. Sections 13–14 give the cyclic Smith realization. Continue with Part II Sections E2–E6 for lattice and stability generalizations, E7–E11 for singular packets and recovery, and E12–E14 for nonlinear and Cayley coordinates. Each visual plate identifies the corresponding manuscript result.
The inherited September 2026 release records 225 Lean theorem targets across 23 proof modules supporting all twenty Part I results. This scope does not extend automatically to Part II. The E-prefixed development has prose proofs and retains the mathematical corrections recorded in the prior edition's exact change ledger. No fresh Lean compilation is claimed for this monograph. The current computation review reran twenty exact-model tests with 305,933 counted assertions and sixteen verifier controls. The current companion suite passed thirty-three tests, with twenty-seven overlapping tests from the earlier snapshot also checked. The extended suite passed 11,052 checks in thirteen groups. Fifty-two saved floating-point metrics and eighteen discrete leaves reproduced exactly, and all eighteen companion figure pairs were regenerated. The visual examples passed their own symbolic checks and controls. These checks have finite scopes and are recorded separately in the accompanying verification files. Historical counts in Part I's reproducibility appendix keep their September provenance.
The two broad edge recovery conjectures remain open. Part II proves recovery for a declared one dimensional separated jump class under its sampling, contrast, and noise assumptions. These results do not supply universal image segmentation or infinite-tree consistency. Numerical illustrations keep the finite interpretation stated in their captions.
Part I: The released formal core
On this page · Permalink · Source line 242
Coordinates first, decisions second
A residue decomposition changes the coordinates of a signal without changing its information. Filtering then acts between those coordinates. Approximation enters when an operator compresses a component or when a decision discards coefficients. The formal core follows these operations in that order.
Abstract
This paper develops the signal realization of the projector-resolved seed calculus. The impulse \(\delta_0\) is taken as a primitive signal seed and its shift orbit supplies the address system. Residue projectors split a sequence into exact polyphase channels, nested divisibility gives exact refinement, and every finite impulse-response operator becomes a matrix of packet transfers. The standard perfect-reconstruction condition for a filter bank is therefore an analysis–synthesis identity in the common operator language of the series. Haar analysis and every finite-depth wavelet-packet transform are treated on complex \(\ell^2\), together with concrete finite-signal models and a predict–update lifting step. The edge problem is separated into two statements. When a discontinuity packet is known and retained exactly, approximation error is exactly the approximation error of the remaining smooth packet. No spectral approximation of the jump is performed. When the packet is estimated, a symmetric-difference bound isolates mask error, amplitude error, and smooth-background error. Numerical studies compare global Fourier truncation, exact known-packet reconstruction, and a deliberately narrow positive-contrast estimator in one and two dimensions, including curved boundaries, corners, and multiple amplitudes. The same cyclic phase action is then placed on the Smith reflection disk. Its pullback through the Cayley transform is a Möbius action on impedance, and the two-phase case is precisely impedance–admittance inversion. Nonlinear coefficient products obey cyclic packet convolution. The preserved September 2026 release integrates a Lean formalization of all twenty theorem-like statements under the hypotheses stated below: 225 supporting theorem targets in 23 modules. Eighteen regenerated figures, machine-readable numerical results, the 33-test original companion suite, and 36 additional exact-model and verifier tests accompany the paper. Exact signal theorems, limited numerical estimators, classical constructions, and open recovery problems are kept distinct throughout.
Scope and claim boundary
The paper proves exact polyphase reconstruction, exact finite filter-transfer identities, perfect reconstruction for the stated filter banks, the conditional known-edge theorem, mask and amplitude perturbation bounds, nonlinear residue-convolution laws, and the Smith-coordinate phase action. It does not claim that every discontinuity can be detected automatically, that every form of Gibbs ringing has been eliminated, or that the simple two-class estimator supplied with the release is a universal segmentation method. The estimator is included as one reproducible finite example. For every finite packet refinement tree, the paper now proves existence of a globally optimal complete pruning, an exact dynamic-programming selector for additive costs, and a deterministic margin-stability certificate. Wavelets, filter banks, the Cayley transform, and the classical Smith grid are treated as classical inputs organized in the common seed–packet–refinement language.
Verification convention. “Lean-checked” refers to the explicitly scoped theorem statements and their supporting declarations, accepted by the pinned Lean kernel. It does not certify the English text automatically, the floating-point Python implementation, physical modelling choices, or the two conjectures. The manuscript-to-declaration correspondence has been reviewed manually. Appendix Section D records it result by result. The September 2026 release records a rerun of the numerical experiments. The current final-edition checks are distinguished in the opening reading note.