Prime Density in Permutation Families with Fixed Digital Root Across Numeral Bases: An Empirical Study with a Conditional Hardy–Littlewood Framework and Machine-Verified Algebraic Results

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_v10.pdf) and its LaTeX source (main_v10.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_pfeh_counterexample.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_agg to C(b).