regularTail
The regular tail definition isolates the genus-one Hadamard product over all zeros except one chosen index k, multiplied by the exponential prefactor from the identification data. Number theorists working on explicit formulas or local zero splittings for the completed xi function would cite this construction to separate a single elementary factor. The definition is assembled directly from the exponential term and an indicator-skipped infinite product to match the multipliable product API.
claimLet $H$ be the Hadamard identification with coefficients $A$, $B$ and zero sequence $ρ_n$. The regular tail at index $k ∈ ℕ$ and point $s ∈ ℂ$ is defined by $e^{A + B s} ∏_{n ≠ k} E_1(s / ρ_n)$, where $E_1$ is the genus-one elementary factor.
background
In the Recognition Science treatment the completed xi function ξ₀ admits a genus-one Hadamard product over its zeros. The module defines the regular tail as the product over all indices except k, times the exponential prefactor exp(A + B s), so that the full product factors as the local elementary factor E₁(s/ρ_k) times this tail. This relies on the shifted cost H(x) = J(x) + 1 = ½(x + x⁻¹) from CostAlgebra, whose functional equation is the d'Alembert form of the Recognition Composition Law, and on the isolation structure from SAT modules that guarantees unique solutions for the zero data.
proof idea
This is a direct definition that multiplies the exponential prefactor exp(H.A + H.B * s) by the infinite product over n, with the ite (n = k) 1 clause setting the k-term to unity so the local factor is excluded. The construction is written to line up exactly with Mathlib's Multipliable.tprod_eq_mul_tprod_ite' for the subsequent splitting step.
why it matters in Recognition Science
The definition supplies the skipped-product term required by the downstream theorem completedRiemannZeta0_local_split_regularTail, which rewrites ξ₀(s) as E₁(s/ρ_k) times the regular tail once the local splitting hypothesis holds. It populates the HadamardRegularTailStatus bundle that records the decomposition as theorem-grade under the hypothesis while flagging the remaining open tasks of unconditional multipliability on ℂ and global cost domination. The construction sits inside the Hadamard factorization program that parallels the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
scope and limits
- Does not prove multipliability of the product with the k-term removed.
- Does not establish holomorphy of the tail on compact subsets.
- Does not supply a global cost bound on the critical strip.
- Does not derive the explicit formula or connect to the phi-ladder.
Lean usage
theorem use_regular_tail (k : ℕ) (s : ℂ) (hsplit : LocalSplittingHypothesis H k s) : completedRiemannZeta₀ s = E1 (s / H.zeros k) * regularTail H k s := by rw [completedRiemannZeta0_local_split_regularTail H k s hsplit]formal statement (Lean)
58def regularTail (k : ℕ) (s : ℂ) : ℂ :=
proof body
Definition body.
59 Complex.exp (H.A + H.B * s) *
60 ∏' n, ite (n = k) 1 (E1 (s / H.zeros n))
61
62/-! ## 2. The local splitting hypothesis -/
63
64/-- Local splitting of the genus-one product at index `k` and point `s`.
65This isolates the single-factor extraction:
66`∏' n, E₁(s / zeros n) = E₁(s / zeros k) * ∏' n, ite (n = k) 1 (E₁ ⋯)`.
67On `ℂ`, this follows from Mathlib's `Multipliable.tprod_eq_mul_tprod_ite'`
68once a multipliability hypothesis for the skipped product is supplied. -/