hadamardRegularTailStatus
plain-language theorem explainer
Analysts working on Hadamard factorizations of the completed Riemann zeta function would cite this definition when isolating the contribution of one zero. It packages the local splitting identity, expressed through the regular tail product over the remaining zeros, as a reusable status record for the shifted cost H. The construction is a direct one-line instantiation of the status structure using the already-established regular-tail form of the splitting identity.
Claim. For the shifted cost function $H$, the regular-tail status asserts that for every natural number $k$ and complex $s$, if the local splitting hypothesis holds at $k$ and $s$, then the completed Riemann zeta function satisfies $completedRiemannZeta_0(s) = E_1(s / z_k) · regularTail(H, k, s)$, where $z_k$ denotes the $k$-th zero and regularTail is the genus-one product over all other zeros times the exponential prefactor.
background
The module operates in the setting of Hadamard products for the completed Riemann zeta function ξ₀. The shifted cost H is defined by H(x) = J(x) + 1 = ½(x + x⁻¹), which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The regular tail at index k consists of the infinite product over zeros other than the k-th, multiplied by exp(A + B s). The local splitting hypothesis states that ξ₀ factors as the elementary factor E₁(s / z_k) times this tail once the relevant multipliability conditions on the product are supplied.
proof idea
The definition is a one-line wrapper that supplies the theorem completedRiemannZeta0_local_split_regularTail H directly to the splitting field of the HadamardRegularTailStatus structure.
why it matters
This definition supplies the named interface for the local splitting step in the genus-one Hadamard product. It feeds the Track-D status bundle whose remaining open content, the unconditional proof of the splitting hypothesis on ℂ and the global cost domination on the strip, is documented as follow-on work. The construction prepares the ground for later analytic arguments that would connect the local factorization to the Recognition framework's treatment of the zeta function and the explicit formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.