Local limits along squares and prime values of digital functions

Call an integer admissible if it is congruent to a square modulo b−1 (for b = 2 the condition is vacuous). For every base b ≥ 2 there are constants c_b, C_b > 0 such that the following holds: if q is sufficiently large and admissible, then #{n ≥ 1 : (n,b) = 1, s_b(n²) = q, n² ≤ b^{C_b·q}} ≥ exp(c_b·√q). The Lean 4 formalisation proves the explicit form: at least 2^{√q/(36b)} representations of size n² ≤ b^{3q} once q ≥ 2304·b⁴.

New theorems, not a formalisation of known results. In base ten the bare existence of a square with any admissible digit sum was recorded in the recreational literature (Murthy–Ashbacher 2005); the theorem here is the quantitative all-base version — roots coprime to b (excluding their trailing-zero trick), exp(c_b√q) representations of controlled size — and that statement is what is machine-checked, with effective but non-optimal constants. The same paper proves a local limit theorem for g(n²) for arbitrary digit weights in every base including binary, and sieves the values: level of distribution 1/2, P₃ and P₂ values, an unconditional Mertens-type prime-value law, a joint Erdős–Kac theorem. Caveats: the two shrinking-frequency estimates behind the local theorem enter the Lean development only as transcribed definitions; the sieve and asymptotic results are unformalised; Corollary 1.9 is formalised in bases 2 and 3 only; the analogous theory along squares of primes remains open.