Golden Germ Zeta Simple Pole

Abstract

The golden germ zeta function has a genuine simple pole at one over phi squared.

Theorem 1.1 (The golden germ zeta function has a simple boundary pole).

$$\begin{array}{r}germZeta:\mathbb{C}\to \mathbb{C},\\ \forall s\in \mathbb{C},\mathrm{germZeta}(s):=\mathrm{riemannZeta}({\phi }^2\times s)\times \prod _{p\in \mathrm{Primes}(\mathbb{N})}(1-p^{-s\times {\phi }^2})\times \sum _{v\in \mathbb{N}}{p}^{-s\times o5Beta(v)},\\ \mathrm{MeromorphicAt}(germZeta,\frac{1}{{\phi }^2})\wedge \\ \mathrm{meromorphicOrderAt}(germZeta,\frac{1}{{\phi }^2})=-1\wedge \\ \mathrm{Tendsto}(germZeta,\mathrm{nhdsWithin}(\frac{1}{{\phi }^2},\mathbb{C}\setminus \{\frac{1}{{\phi }^2}\}),\mathrm{cobounded}(\mathbb{C})).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Isolation/GoldenGermZetaSimplePole.golden_germ_zeta_simple_pole (✓ std3). ∎

Source. Repository-derived.

Commentary.

Set a equal to one over phi squared and let G be the normalized prime product. The residue function is the analytic extension of (z-1) zeta(z), evaluated at phi squared times s, multiplied by G(s) over phi squared.

Pinned Mathlib supplies the zeta residue, the removable-singularity extension mechanism, the meromorphic local normal form, and the order criterion. GoldenGermNormalizedFactorRegularity makes G analytic at a, while GoldenGermZetaBoundary makes G(a) nonzero.

The residue function is therefore analytic and nonzero at a, with value G(a) over phi squared. On the punctured neighborhood, the germ equals (s-a)^(-1) times this residue function. Its meromorphic order is consequently minus one, and the negative order criterion gives convergence to the cobounded filter.

STOPPING JUSTIFICATION: this theorem closes the boundary singularity question left open by GoldenGermZetaBoundary, using the regularity input supplied by GoldenGermNormalizedFactorRegularity. It says nothing about other points, nothing about the zero set, and nothing about the germ away from the displayed punctured neighborhood.

References

• Truth anchor: D5/S3/Analytic/Isolation/GoldenGermZetaSimplePole.golden_germ_zeta_simple_pole
• Dependency: D5/S3/Analytic/EulerGerm/GoldenGermZetaBoundary
• Dependency: D5/S3/Analytic/Regularity/GoldenGermNormalizedFactorRegularity