Local limits along squares and prime values of digital functions

This record is the preprint of the paper "Local limits along squares and prime values of digital functions", together with a Lean 4 formalisation of part of it. Continuing "Prime values of digital functions along the primes" (doi:10.5281/zenodo.22093372), the paper proves a local limit theorem for a strongly b-additive function g along the squares — an asymptotic formula, uniform in k, for the number of n ≤ x with g(n²) = k, for arbitrary fixed digit weights in every base, including the previously missing binary case — and sieves the values: exponent of distribution 1/2 on the natural scale log x; at most three prime factors for ≫ x/log log x integers n ≤ x, and at most two when the lattice obstruction is trivial; an unconditional Mertens-type law for the n with g(n²) prime; and asymptotic independence of the Gaussian digit fluctuation and the Erdős–Kac fluctuation. The mechanism is isolated as a quantitative lattice local limit property, shared by the Martin–Mauduit–Rivat theorem on prime inputs; the parallel consequences along the primes include exact prime-value laws at zero digit mean, weights that see the length of the expansion, and the fact that every sufficiently large integer is the number of zero digits of a prime. An independent elementary construction from Sidon sets produces exp(c√q) squares, with root coprime to the base, whose digit sum is any prescribed large admissible q; the paper closes by quantifying, against a recent theorem of Drmota and Rivat, what is missing for the analogous theory along squares of primes. The Lean 4 project (Lean 4.33.0 with Mathlib, no sorry, no warnings) verifies: the entire prescribed-digit-sum half — Theorem 1.8 and every lemma feeding it, the theorem of Bose and Chowla included (proved rather than assumed) — with no axioms beyond Lean's built-in ones; the engine of the new local theorem, the two-digit spectral gap (Lemma 2.4), in full and in every base; the Fourier assembly of Theorem 1.1 as an implication whose two remaining analytic inputs are transcribed as definitions, never axioms; the output-distribution Theorem 1.2 (unweighted) as an axiom-free implication, with Poisson summation for the Gaussian proved from Mathlib's Jacobi theta transformation; the complete local-factor theory of Theorem 5.12; and the almost-prime theorems from at most two literature results each, declared as documented axioms (Martin–Mauduit–Rivat; Halberstam–Heath-Brown–Richert). An axiom audit lists the exact dependencies of all 107 verified statements — 102 depend on no axiom at all — and the discipline is enforced at build time. The verification report records the paper↔Lean correspondence, the deviations of the formal proofs from the paper's arguments, and an inventory of what is not machine-checked; the distributed scripts reproduce every numerical value quoted in the paper. Contents: paper_anonymous.pdf is the manuscript. The archive additionally contains its LaTeX source, the Lean project (31 modules, pinned toolchain and Mathlib), the axiom-audit driver with its expected output, the verification report and source audit, and the validation scripts with their committed output. Running "lake exe cache get && lake build" in the lean directory reproduces the check. Source repository: https://github.com/vibefrtz/vibemath (folder local-limits-along-squares, commit 94c6a33). The Lean sources are released under Apache-2.0; the manuscript is released under CC BY 4.0.