IndisputableMonolith.NumberTheory.HadamardRegularTail
The HadamardRegularTail module supplies the definition of the regular tail in the genus-one Hadamard product, excluding the factor at a chosen zero index k while retaining the exponential prefactor. Analysts studying the completed Riemann zeta factorization or local splittings around individual zeros would cite this construction. The module consists of aligned definitions that interface directly with Mathlib's multipliable product lemmas via conditional terms.
claimThe regular tail at index $k$ and point $s$ is the genus-one product over all zeros except the one at index $k$, multiplied by the exponential prefactor: $E_1(s - z) = (1 - z) e^z$ with the product written via conditional selection to omit the $k$-th term.
background
This module sits inside the NumberTheory section of the Recognition Science codebase and imports the HadamardGenusOne substrate. That upstream module supplies the concrete Weierstrass factor $E_1(z) = (1 - z) e^z$ together with the elementary properties provable in Mathlib for entire functions of order at most one, since Mathlib currently lacks a packaged Hadamard theorem in this regime. The regular tail construction then excludes one zero to enable local analysis around individual roots of the completed zeta function.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the regular tail object that feeds the local splitting constructions for the completed Riemann zeta function, visible in sibling declarations such as completedRiemannZeta0_local_split_regularTail. It extends the genus-one factorization tools begun in HadamardGenusOne and thereby supports the analytic infrastructure required for the Recognition Science treatment of the functional equation and its zeros.
scope and limits
- Does not prove the full Hadamard factorization theorem.
- Does not treat zeros of multiplicity greater than one.
- Does not handle genus greater than one.
- Does not supply numerical evaluations of the tail.