eulerQuantitativeFactorization_logDerivBound
The equality asserts that the logarithmic derivative bound of the Euler quantitative factorization at a complex point ρ (ρ ≠ 1, Re(ρ) > 1/2) coincides with the carrier derivative bound evaluated at σ₀ = Re(ρ). Researchers verifying the RegularCarrier interface for the zeta function in the Recognition Science cost-covering chain would cite this result. The proof is a one-line simplification that unfolds the definition of the Euler quantitative factorization.
claimLet ρ ∈ ℂ with ρ ≠ 1 and let m ∈ ℤ be the meromorphic order of the reciprocal zeta function at ρ. Assume Re(ρ) > 1/2. Then the logarithmic derivative bound of the Euler quantitative factorization at ρ equals the carrier derivative bound at σ = Re(ρ).
background
The module instantiates the abstract RS carrier/sensor framework from AnnularCost and CostCoveringBridge using the Euler product of ζ(s). Core objects are the prime sum σ ↦ ∑_p p^{-σ}, the Hilbert-Schmidt norm squared ∑_p p^{-2σ}, the carrier log series ∑_p [2 log(1 - p^{-σ}) + 2 p^{-σ}], and the carrier derivative bound 2 ∑_p (log p) p^{-2σ} / (1 - p^{-σ}). The architecture proceeds from primes through A(s) Hilbert-Schmidt and det₂(I - A(s)) to C(s) holomorphic and nonvanishing on Re(s) > 1/2, after which the logarithmic derivative is bounded and the EulerCarrier interface holds. Upstream results supply the J-cost structure and ledger factorization that calibrate the cost-covering axioms once the bound is in place.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of the Euler quantitative factorization, directly equating its logDerivBound component to the carrier derivative bound at the real part.
why it matters in Recognition Science
This result verifies that the concrete Euler product satisfies the RegularCarrier interface needed for the cost-covering axiom to yield a conditional Riemann hypothesis. It supports the module's chain that produces euler_instantiation and euler_regular_carrier. In the Recognition Science framework it confirms alignment between the phi-ladder, eight-tick octave, and the analytic properties of ζ(s) on Re(s) > 1/2, consistent with the derivation of three spatial dimensions and the alpha band bounds.
scope and limits
- Does not establish the bound for Re(ρ) ≤ 1/2.
- Does not remove the hypothesis that the meromorphic order at ρ is an integer.
- Does not apply at ρ = 1.
- Does not prove unconditional convergence of the log derivative outside the stated half-plane.
formal statement (Lean)
658theorem eulerQuantitativeFactorization_logDerivBound (ρ : ℂ)
659 (hρ_ne : ρ ≠ 1) (m : ℤ)
660 (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
661 (hσ : 1/2 < ρ.re) :
662 (eulerQuantitativeFactorization ρ hρ_ne m hord hσ).logDerivBound =
663 carrierDerivBound ρ.re := by
proof body
Term-mode proof.
664 simp [eulerQuantitativeFactorization]
665
666/-- The center of the Euler quantitative factorization is the actual complex
667point `ρ`. -/