Golden Germ Third Normalized Factor Real Positivity

Abstract

The third normalized golden germ product is real and strictly positive at every real point above one over phi to the fifth.

Theorem 1.1 (The third normalized factor is positive on the full real ray).

$$\begin{array}{r}\forall s\in \mathbb{C},p\in \mathrm{Primes}(\mathbb{N}),\\ x(s,p):=p^{-s\times {\phi }^2},y(s,p):=p^{-s\times {\phi }^3},\mathrm{Kp}(s,p):=(1-y(s,p{)}^2{)}^{-1}\times (1-x(s,p{)}^2\times y(s,p))\times (1-y(s,p))\times (1+x(s,p){)}^{-1}\times \sum _{v\in \mathbb{N}}{p}^{-s\times o5Beta(v)},\\ \forall s\in \mathbb{C},G3(s):=\prod _{p\in \mathrm{Primes}(\mathbb{N})}\mathrm{Kp}(s,p),\\ \forall sigma\in \mathbb{R},\frac{1}{{\phi }^5}<sigma\Rightarrow \mathrm{Im}(G3(sigma))=0\wedge 0<\Re (G3(sigma)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Regularity/GoldenGermThirdNormalizedFactorRealPositivity.golden_germ_third_normalized_factor_real_axis_positivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

This theorem is the next real-axis sign step in the golden Euler germ extraction ladder of OACTC parts 580 and 581. It closes the remaining sign boundary for the third normalized factor by strengthening frozen real-point nonvanishing to strict positivity on the entire ray above one over phi to the fifth.

For a positive real sigma, each prime-local factor is represented over the reals. Both prime powers x and y lie strictly between zero and one. Consequently the inverse factor one minus y-squared, the mixed factor one minus x-squared times y, the factor one minus y, and the inverse factor one plus x are all strictly positive. The local germ series is also positive because it is a convergent sum of nonnegative terms whose vacuum term is one.

The frozen third-order factorization supplies summability of the local deviations from one. This yields a genuine real Multipliable family and nonnegativity of its product through finite positive subproducts. Frozen real-point nonvanishing from the regularity theorem rules out zero local factors, so the summable one-plus product theorem makes the infinite product nonzero and hence strictly positive.

Real powers and the real local series are transported to their complex counterparts before the real infinite product is mapped into the complex numbers. The resulting product therefore has imaginary part zero and strictly positive real part.

The conclusion concerns only positive real points above the displayed threshold and only the third normalized product. It does not assert O-5, RH, complex nonvanishing on the whole half-plane, boundary regularity, or any all-order extraction statement.

References

• Truth anchor: D5/S3/Analytic/Regularity/GoldenGermThirdNormalizedFactorRealPositivity.golden_germ_third_normalized_factor_real_axis_positivity
• Dependency: D5/S3/Analytic/EulerGerm/GoldenGermThirdOrderFactorization
• Dependency: D5/S3/Analytic/Regularity/GoldenGermThirdNormalizedFactorRegularity