Polyphase isomorphism between modular arithmetic and multirate digital signal processing: With formal verification in Lean 4 and computational validation

TL;DR: This repository provides both the rigorous mathematical formalization and the empirical computational validation of the exact isomorphism between the modular decomposition of series in number theory and the polyphase decomposition of discrete-time signals in digital signal processing (DSP). This framework establishes that the projection of an absolutely convergent sequence onto congruence classes modulo $m$ is exactly equivalent to decimating that sequence by a factor $M = m$ within an orthogonal, alias-free perfect reconstruction filter bank. Executive Summary This project bridges two classical disciplines—number theory and digital signal processing—that have developed largely independently for decades. It demonstrates that the core underlying operations of series projection and multirate signal decimation are formally identical. The structural exactness of this correspondence is guaranteed through a dual-validation framework: Axiomatic Rigor: A complete, mechanized formal verification of the underlying algebraic and phase properties using the Lean 4 theorem prover and Mathlib. Numerical Veracity: A highly precise Python/Colab notebook that validates the perfect reconstruction property on the Leibniz series for $\pi$ and on the modular Euler product down to machine precision ($10^{-14}$). By establishing this mathematical bridge, techniques can be shared seamlessly across domains: number theory provides new insights into parallel computational architectures (such as the Shared-Nothing paradigm), while tools from signal processing offer novel methods for analyzing arithmetic series. Key Scientific Contributions 1. The Polyphase Isomorphism Theorem (Section 3) We formalize and prove that for any sequence $\{a_n\}_{n=0}^{\infty}$ of complex numbers where the total sum $S = \sum a_n$ converges absolutely, the modular projection $S_r$ and the polyphase component $E_r(z)$ evaluated at the Z-transform edge ($z = 1$) satisfy: $$S_r = E_r(1), \qquad r = 0, \dots, m-1$$ The orthogonality of these channels in the index domain guarantees that the system is intrinsically perfect reconstruction and alias-free. 2. Mechanized Formal Verification in Lean 4 (Section 4.1) The algebraic pillars of the isomorphism have been formally verified and checked by the Lean 4 kernel, ensuring absolute freedom from human or computational error. The proofs certify: Modular Involution: Proof that $5 \times 5 \equiv 1 \pmod 6$ and $1 + 5 \equiv 0 \pmod 6$, cementing the chiral duality of active channels. Unit Group Isomorphism: Verification that $(\mathbb{Z}/6\mathbb{Z})^{\times} \cong \mathbb{Z}_2$, proving that exactly two resonant prime channels exist ($\mathcal{C}_1$ and $\mathcal{C}_5$). Anti-Unitary Phase Symmetry: Real analysis verification of the trigonometric phase requirement $\Delta\phi = \pi$. Polyphase Perfect Reconstruction: Certified proof that parallel synthesis results in exact destructive interference of sterile subbands ($0, 2, 3, 4$), preventing information loss. 3. Applications in Number Theory & Parallel Computing (Sections 5 & 6) Modular Leibniz Representation: $\pi = 3 \sum_{k=0}^{\infty} (-1)^k \left( \frac{1}{6k+1} + \frac{1}{6k+5} \right)$ Modular Euler Product: $\pi = \sqrt{9 \cdot \prod_{p > 3, \, p \equiv \pm 1 \pmod 6} \frac{p^2}{p^2 - 1}}$ Complexity Reduction: Decimation by $m$ decouples calculations into independent threads with zero data dependencies, dropping the effective recursion tree depth by a factor of $\log_2 m$ (ideal for high-performance Shared-Nothing parallel computing architectures). Structural Unification Matrix The polyphase paradigm reformulates classical series by exposing hidden symmetries and revealing parallelization pathways: Mathematical Constant Classical Formulation Modular Polyphase Reformulation (m=6) Leibniz Constant ($\pi$) $\frac{\pi}{4} = \sum_{k=0}^{\infty} \frac{(-1)^k}{2k+1}$ $\pi = 3 \sum (-1)^k \left( \frac{1}{6k+1} + \frac{1}{6k+5} \right)$ Catalan Constant ($G$) $G = \sum_{k=0}^{\infty} \frac{(-1)^k}{(2k+1)^2}$ Orthogonal decomposition over active channels $\mathcal{C}_1 \oplus \mathcal{C}_5$ Apéry Constant ($\zeta(3)$) $\zeta(3) = \sum_{n=1}^{\infty} \frac{1}{n^3}$ Isolated parallel sums over resonant prime channels Hypergeometric Series $\sum \frac{(a)_n (b)_n}{(c)_n n!} z^n$ Discrete multirate polyphase decimation by factor $m$ Reproducibility & Environment Setup This repository is designed to be fully open, auditable, and reproducible. It contains two computational environments: 1. Formal Verification Environment (Lean 4) Path: /polyphase_isomorphism Uses elan as version manager and compiles against Mathlib (revision fabf563). Axiomatically checked via the pure decide tactic. 2. Numerical Validation Environment (Python) Replicates the perfect reconstruction validation, channel mapping, and Euler product convergence plots. Executable instantaneously on the cloud without local installations: Academic Citation If this theoretical framework or the accompanying Lean 4 proofs contribute to your research, please cite both companion works: Fragmento de código @article{peinador2026polyphase, title={Polyphase isomorphism between modular arithmetic and multirate digital signal processing: With formal verification in Lean 4 and computational validation}, author={Peinador Sala, Jos{\'e} Ignacio}, publisher={Zenodo}, year={2026}, doi={10.5281/zenodo.17680023}, url={https://github.com/NachoPeinador/Espectro-Modular-Pi} } @article{peinador2026modularDSP, title={Modular DSP Architecture for EPC of $\pi$]{A modular DSP architecture for extreme-precision computation of $\pi$: Theory, implementation, and the 100M barrier run}, author={Peinador Sala, Jos{\'e} Ignacio}, publisher={Zenodo}, year={2026}, doi={10.5281/zenodo.17768718} } Reference Implementation, Computational Validation, and Lean 4 Formal Verification Author: José Ignacio Peinador Sala Contact: joseignacio.peinador@gmail.com Repository & Source: GitHub Link Companion Practical Work: A Modular DSP Architecture for Extreme-Precision Computation of $\pi$: Theory, Implementation, and the 100M Barrier Run Licensing & Terms of Use Manuscrit Text & Notebooks: Distributed under the Creative Commons Attribution 4.0 International License (CC BY 4.0). Software Core Engine: Distributed under a dual license: the PolyForm Noncommercial License 1.0.0 for academic, peer-review, and non-commercial research; a separate commercial license is required for corporate setups or proprietary benchmarking architectures. 📝 Manuscript Status: This work has been submitted to SeMA Journal (Springer) for publication consideration.* Theoretical Foundation Paper ID: SEMJ-S-26-00195* Parallel Architecture Companion Paper ID: SEMJ-S-26-00196