det2LogFactor
plain-language theorem explainer
The per-prime logarithmic factor supplies the term log(1 minus p to the minus sigma) plus p to the minus sigma that assembles the carrier logarithm from the Euler product in the recognition science cost framework. Analysts working on the conditional Riemann hypothesis via the cost-covering bridge cite this when constructing the holomorphic carrier C(s) as the product over primes. It is a direct definition that encodes the Taylor identity log(1 minus z) plus z equals minus the sum from m greater than or equal to 2 of z to the m over m for the z,
Claim. For a prime $p$ and real number $σ$, the per-prime logarithmic contribution to the regularized determinant is defined by $log(1 - p^{-σ}) + p^{-σ}$.
background
In the EulerInstantiation module the abstract carrier and sensor framework from AnnularCost and CostCoveringBridge receives a concrete realization through the Euler product of the zeta function. Core objects defined nearby include the prime sum equal to the sum over primes of p to the minus sigma and the Hilbert-Schmidt norm squared equal to the sum of p to the minus two sigma. The carrier logarithm is twice the sum over primes of the per-prime factor defined here, which expands via the series to minus twice the sum from m greater than or equal to two of the prime zeta function evaluated at m sigma.
proof idea
This is a direct definition with no lemmas or tactics applied. The expression is written verbatim as the real logarithm of one minus p to the minus sigma plus p to the minus sigma. The identity log(1 minus z) plus z equals minus the sum from m greater than or equal to two of z to the m over m for absolute value of z less than one is invoked only in the separate bound theorem that follows.
why it matters
This definition is the atomic term inside the carrierLog definition and thereby supports the convergence results carrier_log_convergent, det2_log_summable, and the EulerInstantiationCert. It completes the concrete Euler-product layer of the module's three-layer architecture, linking the abstract RS cost structure to the prime factors of the zeta function. Within the Recognition Science framework it advances the instantiation of the regular carrier needed for the cost-covering axiom, contributing to the conditional Riemann hypothesis. It leaves open the extension of the bounds into the critical strip.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.