bibkey: apostol1976introduction authors: Tom M. Apostol year: 1976 title: Introduction to Analytic Number Theory doi: 10.1007/978-1-4757-5579-4 claim: The fundamental theorem of arithmetic and Euclid’s lemma, plus Euler products, von Mangoldt weights, and the logarithmic derivative of the zeta function. strata_touched:

• D5/S3/Arith/EuclidLemma
• D5/S3/Arith/PrimeFactorization
• D5/S3/Weil/EulerProduct
• D5/S3/Zeros/EulerWindows license: citation-only triage: anchor

Introduction to Analytic Number Theory

Tom M. Apostol develops finite and infinite Euler products, the von Mangoldt function, and the logarithmic derivative of the Riemann zeta function in the classical convergence half-plane. These results anchor the prime-power coefficient and logarithmic-derivative declarations in D5/S3/Weil/EulerProduct.

The same finite-product facts support D5/S3/Zeros/EulerWindows: when the real part is positive, none of a finite prime window’s local denominators can vanish, so the total finite product is nonzero. The stronger PZG claim about tail participation and continuation in the critical strip is not attributed to Apostol and remains outside that declaration.

Chapter 1 (The Fundamental Theorem of Arithmetic) states Euclid’s lemma as Theorem 1.5: if a prime p divides a product ab, then p divides a or p divides b. That classical statement anchors D5/S3/Arith/EuclidLemma, which formalizes PZG Lemma 9.1 over the natural numbers. Apostol proves the lemma from the fundamental theorem; the repository proof discharges the same statement through Mathlib’s Nat.Prime.dvd_mul, so only the statement, not the source’s v_p-additivity derivation, is attributed to Apostol.

The same chapter states the fundamental theorem of arithmetic as Theorem 1.10: every integer greater than one is a product of primes, uniquely up to order. Its existence half — every natural number greater than one is a product of finitely many primes — anchors D5/S3/Arith/PrimeFactorization. The repository proof exhibits Mathlib’s prime-factors list as the witnessing product, so only the existence statement, not the source’s minimal-counterexample argument or the uniqueness half, is attributed to Apostol.

The book does not state the repository declarations verbatim. In particular, Lean’s field inverse is a total function with 0^-1 = 0, so the formal finite Euler theorem separates nonvanishing on the regular locus from the exact denominator-zero lattice. That totalization qualification is repo-derived. The formal statement also omits the source volume’s empirical finite-window certificate and does not claim a meromorphic pole order.

Search log

• 2026-07-17: Queried NyxID/Tavily for "finite Euler product" zero-free poles Riemann zeta DOI. Results located standard Euler-product references and the Springer record for Apostol’s book.
• 2026-07-17: Queried "Introduction to Analytic Number Theory" Apostol DOI 10.1007. The publisher metadata verified the title and DOI 10.1007/978-1-4757-5579-4, and its contents identify the chapters on Dirichlet series, Euler products, zeta, and L-functions.
• 2026-07-17: Queried "von Mangoldt" "logarithmic derivative" Riemann zeta DOI. Results restated the classical prime-power definition and the identity -zeta'(s)/zeta(s) = sum Lambda(n)n^(-s) for real part greater than one.
• 2026-07-17: Queried "half-density" normalized Dirichlet series unitary critical line Riemann zeta DOI and then "scaling ledger" "half-density" zeta "unitary". No scholarly source matched the repository’s exact ledger formulation, so CriticalLine.unitarity_line_iff remains repo-derived.
• 2026-07-17: The first three proxy calls sent JSON with the wrong transport shape and received HTTP 422, repeating a failure already recorded by the preceding batch. Reissuing raw JSON on stdin with Content-Type: application/json succeeded; no bibliographic conclusion was drawn from the failed calls.
• 2026-07-29: Confirmed from the book’s Chapter 1 that the fundamental theorem of arithmetic is Theorem 1.10 (“every integer n > 1 is a product of primes, and the factorization is unique apart from order”). Its existence half anchors the new D5/S3/Arith/PrimeFactorization declaration. The DOI 10.1007/978-1-4757-5579-4 and title were already verified above; no new online lookup was required for this in-book locator.
• 2026-07-28: Confirmed from the book’s Chapter 1 that Euclid’s lemma is Theorem 1.5 (“if p is prime and p | ab, then p | a or p | b”), proved there from the fundamental theorem of arithmetic. This anchors the new D5/S3/Arith/EuclidLemma declaration (PZG Lemma 9.1). The DOI 10.1007/978-1-4757-5579-4 and title were already verified above; no new online lookup was required for this in-book locator.

Verified locator

• DOI: https://doi.org/10.1007/978-1-4757-5579-4