det2LogFactor
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,
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove summability of the sum over primes.
- Does not define the full carrier function C(s) or its exponential.
- Does not address complex values of sigma or analytic continuation.
- Does not reference the J-cost, forcing chain, or eight-tick octave.
Lean usage
noncomputable def carrierLog (σ : ℝ) : ℝ := 2 * ∑' (p : Nat.Primes), det2LogFactor p σformal statement (Lean)
101noncomputable def det2LogFactor (p : ℕ) (σ : ℝ) : ℝ :=
proof body
Definition body.
102 Real.log (1 - (p : ℝ) ^ (-σ)) + (p : ℝ) ^ (-σ)
103
104/-- The bound on each log-factor:
105 |log det₂_factor(p,σ)| ≤ p^{−2σ}/(1 − p^{−σ}).
106 This is summable over primes for σ > 1/2. -/