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 b — when all digits are coprime to b and the digital root is coprime to b−1. For such admissible families, computational evidence across seven bases (b ∈ {7, 8, 9, 10, 12, 14, 16}) and digit counts k ∈ {5, …, 30} shows that the aggregate density ratio clusters near the base-dependent value 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) arises exactly as a product of Hardy–Littlewood Euler factors at primes dividing b(b−1), in both cases p | b and 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 = 30 with bootstrap confidence intervals and Bonferroni adjustment. For base 10, a weighted regression on k ∈ {5, …, 30} gives Ĉ = 3.71 with 95% CI [3.62, 3.80], containing C(10) = 3.75 and excluding b/φ(b) = 2.50. 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). The technical obstructions to upgrading this to a theorem are discussed explicitly. This Zenodo deposit contains: main.pdf and paper/main.tex — the paper (14 pages, Version 9). 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. The PDF and LaTeX source of the paper (paper/main.pdf and paper/main.tex) are licensed under CC-BY-4.0. The Python and shell scripts in src/ are licensed under MIT (see LICENSE). The Lean formalisation in formal/ depends on Mathlib4 and inherits its Apache-2.0 license. The aggregate Zenodo deposit is published under CC-BY-4.0.