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

**Version 2.0.0 — Major release: zero-axiom formalisation complete.** This is the companion deposit to the paper "Prime Density in Permutation Families with Fixed Digital Root Across Numeral Bases: An Empirical Study with a Conditional Hardy–Littlewood Framework and a Fully Machine-Verified Aggregate Equidistribution Theorem" (Ferraiuolo, 2026, version 13). **Headline result.** The aggregate equidistribution theorem (Theorem 5.5 of the paper) is now machine-verified end-to-end in Lean 4 with Mathlib, with *no* `sorry` and *no* custom axioms. An `#print axioms` audit on every top-level theorem returns only the three standard Mathlib kernel axioms: `propext`, `Classical.choice`, `Quot.sound`. The combinatorial cardinality lower bound `|A_k(b)| ≥ c · φ(b)^k` — the only residual axiom (`A_k_lower`) in v1.x of this deposit — has been discharged as a proved theorem (`A_k_LowerBound.A_k_lower_proved`, file `A_k_lower_proof.lean`, 981 lines: 6 lemmas + main theorem), via Fourier inversion combined with the spectral gap `‖G(b,u)‖ < φ(b)` for `u ≠ 0`. **Contents:** - `paper/main_v13.pdf` — companion paper (24 pages)- `SpectralGapDensity/` — Lean 4 project: 6 files in `SpectralGapDensity/SpectralGapDensity/`, ~3500 lines, ~80 named theorems- `src/` — Python verification scripts, including two new independent verification tools (`RIGOROUS_STRESS_T5_5.py`, `verify_gamma_table.py`)- `data/`, `results/` — empirical data and aggregate ratio tables- `README.md`, `CHANGELOG.md`, `CITATION.cff` **License.** Code and Lean proofs: MIT. Paper and figures: CC-BY 4.0. Concept DOI (always resolves to the latest version): [10.5281/zenodo.20320999](https://doi.org/10.5281/zenodo.20320999).