# A sharp positive factorization and explicit Hardy-moment bounds

September 14, 2026. Candidate strengthening of the [cycle-24 proof](../0024/hardy-sign-proof.md), pending independent review. This note makes no originality claim. It concerns an auxiliary mixed-moment theorem, not RH. The original proof and its published moment input are retained unchanged.

## 1. The sharp factorization

Use four variables and the Hadamard forms

\[
p_0=t_1+t_2+t_3+t_4,\quad p_1=t_1+t_2-t_3-t_4,
\quad p_2=t_1-t_2+t_3-t_4,\quad p_3=t_1-t_2-t_3+t_4.
\]

Put \(Q=\sum_i t_i^2\), \(E_2=\sum_{i<j}t_it_j\), and

\[
R=\prod_{j=0}^3(1-p_j^2)^{-1},\qquad C=(1-Q)^4R.
\]

**Theorem 1.** Every coefficient of \(C\) is nonnegative. For any real \(\lambda\), the formal series \((1-Q)^\lambda R\) is coefficientwise nonnegative if and only if \(\lambda\le4\).

All formal real powers mean the binomial expansion with constant term one. Formal logarithms and exponentials are valid in the total-degree completion over the reals; for any fixed coefficient only finitely many terms contribute.

**Proof.** Let \(L=\log R+4\log(1-Q)\), so \(C=\exp L\). The eight even-product sign vectors give, for a nonzero multi-index \(\beta\) with \(s=|\beta|\),

\[
s[\mathbf t^\beta]L=w_\beta,
\qquad
w_\beta=\begin{cases}
8\left\{\binom{s}{\beta}-\binom{s/2}{\beta/2}\right\},&\beta\text{ all even},\\
8\binom{s}{\beta},&\beta\text{ all odd},\\
0,&\text{otherwise}.
\end{cases}
\tag{1}
\]

Here a multinomial has four lower entries. The character calculation is precisely the one used in cycle 24; subtracting four logarithms instead of one changes its all-even coefficient to the displayed difference.

Duplicating every letter in a word injects words counted by \(\binom{s/2}{\beta/2}\) into those counted by \(\binom{s}{\beta}\). Thus \(w_\beta\ge0\). Since \(L\) has zero constant term, every coefficient of \(\exp L\) is nonnegative. For \(\lambda\le4\), write

\[
(1-Q)^\lambda R=(1-Q)^{-(4-\lambda)}C.
\]

The first factor has nonnegative coefficients by the binomial expansion, including the case \(4-\lambda=0\). Conversely its coefficient at \(t_1^2\) before this factorization is \(4-\lambda\), since \([t_1^2]R=4\). Nonnegativity therefore requires \(\lambda\le4\). This proves necessity and sufficiency. \(\square\)

This is an optimal exponent within this specific family of coefficientwise factorizations, not an optimal zeta bound or a novelty certificate.

## 2. A recurrence with nonnegative weights

Write \(c_\alpha=[\mathbf t^\alpha]C\), with \(c_0=1\). The Euler derivation \(\mathcal D=\sum_i t_i\partial_{t_i}\) gives \(\mathcal DC=(\mathcal DL)C\). Consequently, for \(S=|\alpha|>0\),

\[
\boxed{c_\alpha=\frac1S\sum_{0<\beta\le\alpha}w_\beta c_{\alpha-\beta}.}
\tag{2}
\]

The componentwise inequality makes this a finite sum and every predecessor has smaller total degree. Thus (2) uniquely determines the coefficients, uses nonnegative weights, and proves their nonnegativity by induction without an appeal to numerical sampling. In fact they are integers, because \((1-Q)^4R\) is a rational series over the integers with denominator constant one.

Every nonzero weight has all-even or all-odd index. This parity class is closed under addition. Therefore \(C\) is supported on all-even and all-odd indices. On a single coordinate axis, \(C=1\), so its nonconstant axis coefficients vanish. Also

\[
c_{(1,1,1,1)}=\frac{8\cdot4!}{4}=48.
\tag{3}
\]

The parity-corrected generating function from cycle 24 is now

\[
\boxed{G=\big\{(1-Q)^{-3}+2E_2(1-Q)^{-4}\big\}C.}
\tag{4}
\]

This is an identity of the actual rational functions, since the right side equals \((1-Q+2E_2)R\). It provides the same coefficients as the signed three-factor MGF after the previously proved parity transform.

For use in (4), write \(B=(1-Q)^{-3}+2E_2(1-Q)^{-4}\). Its coefficients are explicit. For \(a\in\mathbb N^4\),

\[
[\mathbf t^{2a}]B=\binom{|a|+2}{2}\binom{|a|}{a},\qquad
[\mathbf t^{2a+e_i+e_j}]B=2\binom{|a|+3}{3}\binom{|a|}{a}\quad(i<j).
\tag{5}
\]

All other coefficients vanish. There is a unique odd pair in the second case. Convolving these nonnegative coefficients with (2) computes every coefficient of \(G\) using sums of nonnegative terms. The multinomial differences defining the weights are exactly nonnegative by the injection above; the method does not rely on cancellation in a signed moment expansion.

## 3. Explicit lower bounds for every allowed derivative order

For an even-total index \(\alpha=(k,l,m,n)\), put \(S=|\alpha|=2N\), \(\alpha!=k!l!m!n!\), and

\[
K_\alpha=\frac{12\alpha!}{2^S(S+4)!}.
\]

The original integral reduction and parity transform give

\[
(-1)^{\sum_i\lfloor\alpha_i/2\rfloor}\operatorname{HARDY}(\alpha)
=K_\alpha[\mathbf t^\alpha]G.
\tag{6}
\]

**Theorem 2.** The right side is at least \(K_\alpha b_\alpha>0\), where

\[
b_\alpha=\begin{cases}
\displaystyle\binom{N+2}{2}\binom N a,&\alpha=2a,\\[4pt]
\displaystyle2\binom{N+2}{3}\binom{N-1}{a},&\alpha=2a+e_i+e_j,\ i<j,\\[4pt]
\displaystyle48\binom N2\binom{N-2}{a},&\alpha=2a+(1,1,1,1).
\end{cases}
\tag{7}
\]

Each case automatically has a nonnegative upper multinomial argument. These three cases exhaust even total degree.

**Proof.** In the first two cases retain just the constant coefficient \(c_0=1\) in (4) and apply (5). In the last case retain \(c_{(1,1,1,1)}=48\) and the all-even coefficient of \(B\) at \(2a\). Every omitted convolution term is nonnegative. Every displayed factor is strictly positive, including \(N=0\) in the first case, \(N=1\) in the second, and \(N=2\) in the third. \(\square\)

The bound is exact on every coordinate axis. Indeed, on such an axis \(C=1\), \(E_2=0\), and \(G=(1-t^2)^{-3}\). Simplifying (6) gives

\[
\operatorname{HARDY}(2N,0,0,0)
=(-1)^N\frac{3}{2\cdot4^N(2N+1)(2N+3)}\qquad(N\ge0).
\tag{8}
\]

The minimal two-odd and four-odd cases also attain the bound:
\(\operatorname{HARDY}(1,1,0,0)=1/120\) and
\(\operatorname{HARDY}(1,1,1,1)=1/1120\).
These equality statements do not assert optimality for every other index.

## 4. Scope and remaining proof obligations

The all-orders statements rest on the analytic/formal-series proof above and the original published moment representation, not on finite computations. The recurrence and lower bounds strengthen the project’s constructive presentation of the auxiliary sign theorem; they do not improve RH, a zero-free region, or a zero proportion.

The exact even-sign character identity is being addressed separately in Lean. Even if that lemma compiles, this note’s series factorization, recurrence-to-rational-function identification, integral reduction, and complete Hardy conclusion are not thereby formally verified.

A separate reviewer must check (1)–(8), boundary cases, sharpness, and the link to the original normalization before acceptance. Whether this strengthening or the underlying sign theorem is new in the literature remains unresolved.