Central-Factorial Parity Identities

Abstract

A universal half-shift factorization proves two central-factorial coefficient identities.

The two final statements match the conjectured formulas (4.27) and (4.41) in S. Yakubovich, On the generalized Dirichlet beta and Riemann zeta functions and Ramanujan-type formulae for beta and zeta values, arXiv:2405.03294, section 4. The proofs below are derived here from polynomial products and coefficient extraction. This citation identifies the questions being answered, not an external proof.

All polynomial equalities are in Q[X]. C denotes Polynomial.C, comp is polynomial composition, and coeff(P,K) is the coefficient of X^K. The notation t(N,K) denotes centralFactorial N K; A_n, C_n and F_n denote A n, Cpoly n and F n. The map rat is the natural-number cast into Q. The operator div is natural-number division, and mod is its remainder. Subtraction between natural-number indices is truncated at zero; subtraction involving rat is rational subtraction. Icc(a,b) is the inclusive natural interval, empty when b<a; range(a) is 0 through a-1. The operator choose is Nat.choose, with value zero when its lower index exceeds its upper index.

Definition 1.1 (Signed Rational Central-Factorial Coefficients).

$$\begin{array}{r}\forall N,K\in \mathbb{N},\\ t(N,K):\mathbb{Q},\\ (N\mathrm{mod}2=0)\Rightarrow t(N,K)=\mathrm{coeff}(\prod _{j\in \mathrm{range}(\mathrm{div}(N,2))}(X^2-C(\mathrm{rat}(j{)}^2)),K),\\ (N\mathrm{mod}2\ne 0)\Rightarrow t(N,K)=\mathrm{coeff}(X\cdot \prod _{j\in \mathrm{range}(\mathrm{div}(N,2))}(X^2-C((\mathrm{rat}(j)+\frac{1}{2}{)}^2)),K).\end{array}$$

Formalization. D5/S1/Recurrence/CentralFactorialParityIdentity.centralFactorial (✓ std3).

Source. Repository-derived.

Commentary.

These are the defining even and odd products, including all zero coefficients. The private squareProduct abbreviation has been expanded in this display. No absolute values or odd-row rescaling enter the definition. The paper’s first-kind even and odd product conventions are (1.22) and (1.24).

Definition 1.2 (Integer-Root Odd Polynomial).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ A_n=X\cdot \prod _{j\in \mathrm{Icc}(1,n-1)}(X^2-C(\mathrm{rat}(j{)}^2))\end{array}$$

Formalization. D5/S1/Recurrence/CentralFactorialParityIdentity.A (✓ std3).

Source. Repository-derived.

Commentary.

The leading X is outside the product, exactly as in the definition.

Definition 1.3 (Half-Integer-Root Even Polynomial).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ C_n=\prod _{j\in \mathrm{Icc}(1,n-1)}(X^2-C((\mathrm{rat}(j)-\frac{1}{2}{)}^2))\end{array}$$

Formalization. D5/S1/Recurrence/CentralFactorialParityIdentity.Cpoly (✓ std3).

Source. Repository-derived.

Commentary.

The factors use j minus one half, with j starting at one.

Theorem 1.4 (Evenness of the Half-Integer-Root Product).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ \mathrm{comp}(C_n,0-X)=C_n\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.Cpoly_even (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each quadratic factor is unchanged by substituting zero minus X.

Definition 1.5 (Scaled Shift Polynomial).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ F_n=C(\frac{1}{2})\cdot \mathrm{comp}(A_n,C(\frac{1}{2})\cdot (1+X))\end{array}$$

Formalization. D5/S1/Recurrence/CentralFactorialParityIdentity.F (✓ std3).

Source. Repository-derived.

Commentary.

Multiplication by C(1/2) scales the polynomial after composition.

Theorem 1.6 (Universal Half-Shift Factorization).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ (1\le n)\Rightarrow \\ \mathrm{comp}(A_n,X+C(\frac{1}{2}))=(X+C(\mathrm{rat}(n)-\frac{1}{2}))\cdot C_n\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.half_shift (✓ std3). ∎

Source. Repository-derived.

Commentary.

Induction pairs each new integer-root quadratic with the preceding linear factor. This produces the half-integer-root product uniformly in n.

Theorem 1.7 (Scaled Linear Times Even Factorization).

$$\begin{array}{r}\forall n\in \mathbb{N},\\ (1\le n)\Rightarrow \\ F_n=C(\frac{1}{4})\cdot (X+C(2\cdot \mathrm{rat}(n)-1))\cdot \mathrm{comp}(C_n,C(\frac{1}{2})\cdot X)\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.F_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Compose the half-shift identity with X/2 and multiply by one half. The resulting constant polynomial factor is C(1/4).

Theorem 1.8 (Adjacent Coefficient Relation).

$$\begin{array}{r}\forall n,r\in \mathbb{N},\\ (1\le n)\Rightarrow \\ \mathrm{coeff}(F_n,2\cdot r)=(2\cdot \mathrm{rat}(n)-1)\cdot \mathrm{coeff}(F_n,2\cdot r+1)\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.adjacent_coefficients (✓ std3). ∎

Source. Repository-derived.

Commentary.

The second factor is even, so each adjacent even and odd coefficient pair has the displayed ratio, including coefficients beyond the degree.

Theorem 1.9 (Parity Identity).

$$\begin{array}{r}\forall n,k\in \mathbb{N},\\ (1\le n)\Rightarrow \\ (1\le k)\Rightarrow \\ (\frac{1}{4}{)}^k\cdot t(2\cdot n-1,2\cdot k-1)=\sum _{q\in \mathrm{Icc}(k,n)}((\frac{1}{4}{)}^q\cdot \mathrm{rat}(\mathrm{choose}(2\cdot q-1,2\cdot k-1))\cdot t(2\cdot n,2\cdot q))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.identity_427 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Compare the odd coefficients of F in its defining expansion and its factorization. The statement covers all positive n and k, without a k<=n hypothesis. The notation (1/4)^k equals 4 raised to the integer exponent -k.

Theorem 1.10 (Adjacent Binomial Relation).

$$\begin{array}{r}\forall p,d\in \mathbb{N},\\ \mathrm{rat}(p+1)\cdot \mathrm{rat}(\mathrm{choose}(p,d))=(\mathrm{rat}(\mathrm{choose}(p,d))+\mathrm{rat}(\mathrm{choose}(p,d+1)))\cdot \mathrm{rat}(d+1)\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.choose_adjacent (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive j and l, specialize p=2j-1 and d=l-1 to obtain the named 2j and l relation. The proof applies Mathlib’s Nat.add_one_mul_choose_eq, rewrites with Nat.choose_succ_succ’, and casts the equality into Q.

Theorem 1.11 (Weighted Sum Reduction).

$$\begin{array}{r}\forall n,m\in \mathbb{N},\\ (1\le n)\Rightarrow \\ (m\le n-1)\Rightarrow \\ \sum _{k\in \mathrm{range}(m+1)}(4^k\cdot t(2\cdot n,2\cdot (n-k))\cdot \mathrm{rat}(\mathrm{choose}(2\cdot (n-k)-1,2\cdot (n-m-1)))\cdot \mathrm{rat}(2\cdot n\cdot (m-k)+k))=\frac{4^n\cdot \mathrm{rat}(2\cdot (n-m-1)+1)}{2}\cdot ((2\cdot \mathrm{rat}(n)-1)\cdot \mathrm{coeff}(F_n,2\cdot (n-m-1)+1)-\mathrm{coeff}(F_n,2\cdot (n-m-1)))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.weighted_sum_reduction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The upper coefficient index is l=2(n-m-1)+1. The reflected coefficient expansion and adjacent-binomial relation give the displayed scalar multiple.

Theorem 1.12 (Weighted Vanishing Sum).

$$\begin{array}{r}\forall n,m\in \mathbb{N},\\ (1\le n)\Rightarrow \\ (m\le n-1)\Rightarrow \\ \sum _{k\in \mathrm{range}(m+1)}(4^k\cdot t(2\cdot n,2\cdot (n-k))\cdot \mathrm{rat}(\mathrm{choose}(2\cdot (n-k)-1,2\cdot (n-m-1)))\cdot \mathrm{rat}(2\cdot n\cdot (m-k)+k))=0\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CentralFactorialParityIdentity.identity_441 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reflect the coefficient expansion, use the parity identity for its odd part, and apply the adjacent-binomial relation. The weighted sum is a scalar multiple of the vanishing adjacent-coefficient difference. The parity identity is a prerequisite on the live proof path, in consumer-to-prerequisite direction.

References

• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.A
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.Cpoly
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.Cpoly_even
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.F
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.F_factorization
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.adjacent_coefficients
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.centralFactorial
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.choose_adjacent
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.half_shift
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.identity_427
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.identity_441
• Truth anchor: D5/S1/Recurrence/CentralFactorialParityIdentity.weighted_sum_reduction