completedRiemannZeta0_local_split
plain-language theorem explainer
The local splitting identity isolates the k-th zero contribution inside the Hadamard factorization of the completed Riemann zeta function. Analysts constructing explicit formulas or zero-isolation arguments in the Recognition framework would cite this step when decomposing ξ₀ at an arbitrary point s. The proof is a direct rewrite that invokes the genus-one factorization theorem, substitutes the splitting hypothesis, and normalizes the resulting expression by ring.
Claim. Let H be an XiHadamardIdentification supplying coefficients A, B and the zero sequence {z_n}. For natural number k and complex s, assume the local splitting hypothesis at k and s, which asserts that the full genus-one product equals the isolated factor at k times the product with the k-th term replaced by 1. Then the completed Riemann zeta function satisfies ξ₀(s) = exp(A + B s) ⋅ E₁(s / z_k) ⋅ ∏_{n ≠ k} E₁(s / z_n).
background
The HadamardRegularTail module decomposes the completed Riemann zeta function ξ₀ from a supplied XiHadamardIdentification. The local splitting hypothesis is the equality (∏' n, E₁(s / H.zeros n)) = E₁(s / H.zeros k) ⋅ ∏' n, ite (n = k) 1 (E₁(s / H.zeros n)), which isolates one elementary factor under a multipliability assumption supplied by Mathlib. The module records that global cost domination on the strip and holomorphy of the regular tail are deliberately left open, as they require analytic content beyond the algebraic factorization.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side by the genus-one factorization theorem completedRiemannZeta0_genus_one_factorization, substitutes the local splitting hypothesis, and closes with the ring tactic.
why it matters
This result supplies the local-split form of the Hadamard product that is immediately consumed by the regular-tail variant completedRiemannZeta0_local_split_regularTail. It supplies the analytic bridge between the genus-one factorization and the cost-algebra objects H and J that appear throughout the Recognition forcing chain (T5 J-uniqueness). The module explicitly flags that uniform-on-compact convergence for the tail and global cost bounds remain open, requiring further multipliability or explicit-formula input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.