norm_eulerPrimeLogDerivTermComplex_le
plain-language theorem explainer
Norm bound controls the per-prime logarithmic derivative term in the Euler product for the zeta function under the Recognition Science carrier framework. Analysts deriving conditional Riemann hypothesis results via cost-covering axioms cite it to control sampled-circle perturbations. The tactic proof secures the denominator separation via the reverse triangle inequality, normalizes the real logarithm, and reduces the comparison to a real division inequality.
Claim. For complex $s$ with positive real part and prime $p$, let $z = p^{-s}$. Then the norm of the per-prime logarithmic derivative term satisfies $|| (log p) z^2 / (1 - z) || ≤ (log p) ||z||^2 / (1 - ||z||)$.
background
The EulerInstantiation module shows that the Euler product of ζ(s) realizes the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge. Core objects include the prime sum P(σ) = ∑_p p^{-σ}, the Hilbert-Schmidt norm squared ∑_p p^{-2σ}, and the carrier log series. Key results establish that the associated determinant C(s) is holomorphic and nonvanishing for Re(s) > 1/2 with bounded logarithmic derivative, allowing the cost-covering axiom to apply and produce a conditional Riemann hypothesis.
proof idea
The tactic proof first invokes norm_eulerPrimePowerComplex_lt_one to obtain ||z|| < 1. It records nonnegativity of log p from the fact that primes exceed 1, positivity of the denominator, and the reverse triangle inequality 1 - ||z|| ≤ ||1 - z||. After normalizing the norm of the real logarithm, it unfolds the definition of the log-derivative term and rewrites using norm_div, norm_mul, and norm_pow, then applies div_le_div_of_nonneg_left.
why it matters
This estimate is applied directly in norm_eulerPrimeLogDerivTermComplex_le_carrierDerivTerm to replace the complex norm by the real carrier derivative term. It advances the module's demonstration that C(s) satisfies the EulerCarrier interface, which permits the cost-covering axiom and yields the conditional Riemann hypothesis. Within the Recognition Science framework the step instantiates the number-theoretic layer that connects the Euler product to the forcing chain and the carrier/sensor axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.