Code, data, and formal proofs accompanying the paper "Prime Density in Permutation Families with Fixed Digital Root Across Numeral Bases", Version 10. The repository contains: (i) the compiled paper (mainᵥ10. pdf) and its LaTeX source (mainᵥ10. tex) with figure; (ii) Lean 4 / Mathlib formal proofs of theunconditional results (local-factor lemma in both cases, digital-root homomorphism property, safe-prime exclusion) ; (iii) Python code for theempirical sampling and analysis; (iv) an exact verification script (verifyₚfehcounterexample. py) reproducing the new Section 6. 2 results. Version 10 adds Section 6. 2: an exact (non-sampled) counterexample showing that the pointwise Permutation Family Equidistribution Hypothesis fails when the basehas small multiplicative order modulo p and the digit multiset is poor in residues (closed-form bias, no decay in k), together with the exact result thatequidistribution is restored in aggregate over all admissible multisets. This explains the empirical convergence of the aggregate density ratio Rₐgg to C (b).
Giovanni Ferraiuolo (Fri,) studied this question.