completedRiemannZeta0_local_split_regularTail
plain-language theorem explainer
The theorem gives the regular-tail form of the local decomposition for the completed Riemann zeta function at any chosen zero index k. Number theorists working on Hadamard factorizations within the Recognition Science analytic continuation would cite it to isolate the elementary factor E1(s/zeros k) from the remaining product. The proof is a one-line wrapper that rewrites via the base local-split identity and normalizes with ring.
Claim. Let $H$ be the shifted cost function. Assume the local splitting hypothesis at index $k$ and point $s$, which states that the genus-one product factors as $E_1(s/z_k)$ times the product over all other indices. Then the completed Riemann zeta function satisfies $completedRiemannZeta_0(s) = E_1(s/z_k) · regularTail(H,k,s)$, where regularTail is the genus-one product over indices ≠k multiplied by the exponential prefactor exp(A + B s).
background
The HadamardRegularTail module starts from a XiHadamardIdentification and seeks to split the completed zeta function ξ₀ at any zero index k. The regular tail is the genus-one product over indices ≠k times exp(A + B s). The LocalSplittingHypothesis isolates the single-factor extraction: the infinite product of E1(s/zeros n) equals E1(s/zeros k) times the skipped product, following from Mathlib's Multipliable.tprod_eq_mul_tprod_ite' once a multipliability hypothesis is supplied. This module imports HadamardGenusOne and packages the local-split identity as a named hypothesis for future analytic steps. Upstream results include the definition of H as J(x) + 1 from CostAlgebra, which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side using the completedRiemannZeta0_local_split theorem instantiated at the given hypothesis hsplit, substitutes the definition of regularTail, and applies the ring tactic to normalize the resulting algebraic expression.
why it matters
This supplies the regular-tail variant of the local split, which is directly assigned into the HadamardRegularTailStatus bundle. It completes the local-split identity step in the Hadamard factorization chain described in the module documentation. The result touches the open analytic questions of proving the splitting unconditionally on ℂ and establishing holomorphy of the regular tail via uniform-on-compact convergence. In the Recognition Science setting it supports the zero structure needed for cost domination arguments that link to the forcing chain and native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.