What question did this study set out to answer?

To investigate prime density in permutation families defined by fixed digital roots across various numeral bases and verify the foundational theorems related to this study.

June 6, 2026Open Access

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

Key Points

To investigate prime density in permutation families defined by fixed digital roots across various numeral bases and verify the foundational theorems related to this study.
Employs a conditional Hardy–Littlewood framework for analysis.
Utilizes Lean 4 with Mathlib for machine verification of theorems.
Includes empirical data collection and verification using Python scripts.
The equidistribution theorem is verified without custom axioms or errors, maintaining three standard kernel axioms.
A significant lower bound for combinatorial cardinality is now proven, enhancing the existing framework.
Fourier analysis confirms the spectral gap properties crucial to the density proofs.

Abstract

**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ₖ (b) | ≥ c · φ (b) ᵏ` — the only residual axiom (`Aₖₗower`) in v1. x of this deposit — has been discharged as a proved theorem (`AₖLowerBound. Aₖₗowerₚroved`, file `Aₖₗowerₚroof. 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ᵥ13. 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 (`RIGOROUSSTRESST5₅. py`, `verifygammaₜable. 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).

Read Full Paperexternally

اسأل الذكاء الاصطناعي

Bookmark

View Full Paper