HadamardRegularTailStatus
plain-language theorem explainer
HadamardRegularTailStatus packages the conditional local-split decomposition of the completed Riemann zeta function into an elementary Weierstrass factor at a chosen zero and the remaining regular tail. Number theorists working on Hadamard products for zeta would cite the structure to isolate the splitting step under an explicit hypothesis. The declaration is a pure structure definition that records the implication without supplying a proof of the hypothesis itself.
Claim. Let $H$ be the shifted cost function. For every natural number $k$ and complex number $s$, if the local splitting hypothesis holds at $(k,s)$, then the completed Riemann zeta function satisfies $$completedRiemannZeta_0(s) = E_1(s/H.zeros(k)) · regularTail(H,k,s),$$ where $E_1(z)=(1-z)exp(z)$ and $regularTail$ is the genus-one product over all indices except $k$ multiplied by the exponential prefactor.
background
The module HadamardRegularTail works from a XiHadamardIdentification and splits the completed zeta function ξ₀ at any chosen zero index k. The genus-one elementary factor is defined by E₁(z) = (1-z)·exp(z). The regular tail at (k,s) is exp(A + B s) times the product over n≠k of E₁(s/zeros n), written with ite to match Mathlib's multipliability API. The local splitting hypothesis states that the full infinite product ∏' E₁(s/zeros n) equals E₁(s/zeros k) times the skipped product; this follows from Multipliable.tprod_eq_mul_tprod_ite' once a multipliability hypothesis for the skipped product is supplied. Upstream, H is the shifted cost H(x) = J(x) + 1 = ½(x + x⁻¹) from CostAlgebra, which reparametrizes the Recognition Composition Law into d'Alembert form.
proof idea
The declaration is a structure definition with an empty proof body. It directly encodes the single field splitting as the implication from LocalSplittingHypothesis to the product identity completedRiemannZeta0_local_split_regularTail, serving as a named bundle with no computational content or tactic steps.
why it matters
The structure tracks the status of the regular-tail decomposition for the Hadamard factorization of the completed zeta function and is instantiated by the downstream definition hadamardRegularTailStatus. It records the local-split identity as theorem-grade once the hypothesis is assumed while explicitly documenting the remaining open tasks (unconditional local splitting on ℂ and global cost domination) as named follow-on work. In the Recognition framework this supports the analytic steps required for the explicit formula and the energy-budget decompositions that link to the HonestPhaseCostBridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.