Prime Observer Casimir Complete Monotonicity

Abstract

The split-prime zero-minus-first regulator mode is completely monotone.

Theorem 1.1 (Alternating derivatives of the split-prime observer Casimir).

$$\forall phase\in \mathrm{Nat}()\to \mathrm{Real}(),\left(\forall m\in \mathrm{Nat}(),sigma\in \mathrm{Real}(),1<sigma\Rightarrow \mathrm{pow}((-1),m)\times \mathrm{iteratedDeriv}(m,\mathrm{goldenObserverCasimir}(phase),sigma)=\sum _{p\in NatPrimes}\sum _{k\in \mathbb{N}}\{\begin{array}{ll}\frac{2\times (1-\cos ((k+1)\times phase\left(p\right)))}{(k+1)}\times ((k+1)\times \log (p){)}^m\times p^{-((k+1)\times sigma)},& \mathrm{mod}(p,5)=1\vee \mathrm{mod}(p,5)=4\\ 0,& \text{otherwise}\end{array}\right)\wedge \left(\left(\forall m\in \mathrm{Nat}(),sigma\in \mathrm{Real}(),p\in \mathrm{NatPrimes}(),k\in \mathrm{Nat}(),1<sigma\Rightarrow 0\le \{\begin{array}{ll}\frac{2\times (1-\cos ((k+1)\times phase\left(p\right)))}{(k+1)}\times ((k+1)\times \log (p){)}^m\times p^{-((k+1)\times sigma)},& \mathrm{mod}(p,5)=1\vee \mathrm{mod}(p,5)=4\\ 0,& \text{otherwise}\end{array}\right)\wedge \left(\forall m\in \mathrm{Nat}(),sigma\in \mathrm{Real}(),1<sigma\Rightarrow 0\le \mathrm{pow}((-1),m)\times \mathrm{iteratedDeriv}(m,\mathrm{goldenObserverCasimir}(phase),sigma)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/PrimeObserverCasimirCompleteMonotonicity.prime_observer_casimir_complete_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Golden split primes are the nonramified rational primes whose images are not prime in the golden integers. The phase function supplies their regulator angles.

Each Fourier mode is constructed as a prime-power Dirichlet coefficient. The Casimir is the logarithmic zero-mode reading minus the first-mode reading.

The prime-power coefficient is a nonnegative squared phase distance. Termwise logarithmic differentiation and prime-power support reindexing give the displayed signed double series throughout the half-plane sigma greater than one. The index k + 1 records the source’s positive prime-power exponent.

References

• Truth anchor: D5/S3/Analytic/Adelic/PrimeObserverCasimirCompleteMonotonicity.prime_observer_casimir_complete_monotonicity
• Dependency: D5/S3/PrimeForms/GoldenPrimeClassification