primeLog
plain-language theorem explainer
primeLog records the natural logarithm of each prime p as a real number to ensure unambiguous terms in the complex Euler factor expressions. Analysts of the zeta function's Euler product within the Recognition Science carrier framework cite this definition when deriving logarithmic derivatives and norm bounds. It is implemented as a direct application of the real logarithm function to the prime cast to reals.
Claim. For a prime number $p$, define $L(p) :=$ natural logarithm of $p$ viewed as a real number.
background
The EulerInstantiation module shows how the Euler product of zeta(s) realizes the abstract RS carrier and sensor framework from AnnularCost and CostCoveringBridge. It proceeds from the prime sum and Hilbert-Schmidt norm squared through the carrier log series to holomorphic nonvanishing of the regularized determinant C(s) on Re(s) > 1/2, satisfying the EulerCarrier interface and enabling the cost-covering axiom for conditional RH.
proof idea
This is a one-line definition that casts the prime p to a real number and applies the real logarithm function.
why it matters
primeLog supports eulerPrimePowerComplex and eulerPrimeLogDerivTermComplex, which feed the norm bounds and carrier derivative terms used to verify the EulerCarrier and RegularCarrier properties. It supplies the unambiguous log p required for the logarithmic derivative in the prime zeta function and carrierLogSeries, advancing the module's instantiation chain from primes to convergent determinants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.