Prime values of digital functions along the primes

A mathematical manuscript together with a Lean 4 formalisation certifying part of its deductive content. The paper proves that an integer-valued strongly b-additive function g with gcd(g(1),…,g(b−1)) = 1 and nonnegative digit mean takes prime values at infinitely many primes p, with a Mertens-type formula when the mean is positive (sharpening theorems of Harman for the digit sum), counting bounds of order π(x)/log log x and normal order log₃ p for ω(g(p)); the proofs rest on the local limit theorem of Martin, Mauduit and Rivat. Running example: the primes whose sum of squared decimal digits is prime (OEIS A052034) are infinite. In the formalisation (Lean 4.33.0/Mathlib), that local limit theorem is the single axiom, transcribed from its source and audited clause by clause; the first two phases, including the infinitude of A052034, are machine-checked from it with no sorry, 32 of the 40 audited results are unconditional, and the axiom discipline is enforced at build time. Manuscript under CC BY 4.0; Lean sources and audits under Apache 2.0.