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

We study prime density within *permutation families* — sets of integers sharing the same digit multiset in a given base bb b — when all digits are coprime to bb b and the digital root is coprime to b−1b-1 b−1. For such admissible families, computational evidence across seven bases (b∈{7,8,9,10,12,14,16}b \in \{7,8,9,10,12,14,16\} b∈{7,8,9,10,12,14,16}) and digit counts k∈[5,30]k \in [5,30] k∈[5,30] shows that the aggregate density ratio clusters near the base-dependent value C(b)=(b/φ(b))⋅((b−1)/φ(b−1))C(b) = (b/\varphi(b)) \cdot ((b-1)/\varphi(b-1)) C(b)=(b/φ(b))⋅((b−1)/φ(b−1)). The paper has three contributions, deliberately separated by epistemic status: Machine-verified (unconditional): a local-factor lemma showing that C(b)C(b) C(b) arises exactly as a product of Hardy–Littlewood Euler factors at primes dividing b(b−1)b(b-1) b(b−1), in both cases p∣bp \mid b p∣b and p∣(b−1)p \mid (b-1) p∣(b−1). Together with the ring-homomorphism property of the digital-root map and the exclusion of safe primes with digital root 1 in base 10 (Proposition 6.1), these algebraic results are formally verified in Lean 4 with Mathlib. Empirical: aggregate ratios across seven bases up to k=30k=30 k=30 with bootstrap confidence intervals and Bonferroni adjustment. For base 10, a weighted regression on k∈{5,…,30}k \in \{5,\ldots,30\} k∈{5,…,30} gives C^=3.71\hat{C} = 3.71 C^=3.71 with 95% CI [3.62,3.80][3.62, 3.80] [3.62,3.80], containing C(10)=3.75C(10) = 3.75 C(10)=3.75 and excluding b/φ(b)=2.5b/\varphi(b) = 2.5 b/φ(b)=2.5. Conjectural: under an explicit Permutation Family Equidistribution Hypothesis (PFEH) and a Bombieri–Vinogradov-type level of distribution, the Hardy–Littlewood heuristic predicts πF(x)∼C(b) li(x)\pi_{\mathcal{F}}(x) \sim C(b) \,\mathrm{li}(x) πF(x)∼C(b)li(x). The technical obstructions to upgrading this to a theorem are discussed explicitly. This Zenodo deposit contains: main.pdf and paper/main.tex: the paper (13 pages, Version 8). formal/: complete Lean 4 / Mathlib formalisation of the unconditional results (PrimeDensity.lean and PrimeDensityExtended.lean), with lakefile.toml and lean-toolchain pinned for reproducibility. src/: Python pipeline for generating admissible families (generate_families_v2.py) and running the statistical analysis (advanced_analysis.py), plus four bash stage scripts and a run_all.sh driver. data/: nine Parquet datasets covering all seven bases and digit-count ranges referenced in the paper (~3.5 MB). results/: JSON analysis reports and PDF plots for base 10 (Table 1) and base 14 (Table 3). README.md, CITATION.cff, and data/SCHEMA.md: documentation and citation metadata. Full reproduction instructions are in README.md. The Python pipeline takes 30–90 minutes; the Lean verification takes approximately 20 minutes for the first build (Mathlib cache download) and is instantaneous thereafter.