Three worked structures, three distinct kinds of conclusion
| Structure | What is established in the original worked layer |
|---|---|
| Finite signal | Exact signed addressing, filter transfer, Haar reconstruction and energy, sparse coefficient error, and full-tuple nonlinear evaluation. |
| Finite packet tree | All \(26\) complete prunings, actual projector sums, the unique cost-\(9\) optimum, and a strict perturbation-margin certificate. |
| Reflection orbit | Exact rational-complex coordinates, a pole-safe projective action, CRT labels, and finite sensitivity calculations. |
What each evidence layer means
Manuscript theorems. The preserved v1.1.0 release maps twenty theorem-like statements to \(225\) supporting Lean targets in \(23\) proof modules. Its saved compiler and axiom records remain inherited evidence. No fresh Lean run is claimed for this edition. The additional Part II developments remain outside this twenty-result map.
Current exact examples. The symbolic visual suite was rerun for this monograph. All \(181\) rational, algebraic, symbolic, and exhaustive finite checks passed. Seven deliberately false assertions were rejected. Numerical samples draw the continuous Fourier and sensitivity curves; they are not promoted to interval enclosures or universal error bounds.
Current executions. The fresh source-release checker passed 20 exact tests containing 305,933 assertions and passed 16 verifier tests, including positive and negative controls. The expanded-source numerical audit passed 11,052 finite checks, mixing exact and numerical calculations. The new extension examples separately passed 38 grouped exact checks and four false controls. These counts measure different operations and are not combined as theorem counts. Reproducibility. The package preserves the original sources and their reports. Run python3 build.py here for an isolated PDF build. The extension finite checker is checks/verify_extension_examples.py; its contract and raw execution manifest are included. The original visual checker requires the listed optional dependencies. PDF assembly does not run Lean or either mathematical checker.
The remaining boundaries are not decorative disclaimers
Known-edge synthesis requires the correct packet. A finite cost optimum depends on the supplied objective. An infinite packet tree, a universal segmentation procedure, minimax recovery rates, and optimal Smith sampling require additional theorems. The core's broad edge-recovery problems are not resolved by these finite examples. V27 introduces the additional separated-jump recovery results and their explicit hypotheses. The \(16\)-sample running signal is not the \(1024\)-sample manuscript experiment; the \(26\)-pruning example is not its \(458{,}330\)-pruning benchmark. Their smaller sizes allow every relevant number to be inspected exactly.
Read this as
Coordinates, approximation, identification, optimization, and physical interpretation are separate layers. The examples make their interfaces visible without erasing their hypotheses.