Cover Image

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

Fuente: Zenodo
Saved in:
Bibliographic Details
Main Author: Ferraiuolo, Giovanni
Format: Recurso digital
Language:English
Published: Zenodo 2026
Subjects:
number theory
prime distribution
digital root
permutation families
Hardy-Littlewood conjecture
singular series
equidistribution
formal verification
Lean 4
Mathlib
reproducible research
computational number theory
Online Access:
Acceder al recurso
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866902082061074432
author Ferraiuolo, Giovanni
author_facet Ferraiuolo, Giovanni
contents <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">We study prime density within *permutation families* — sets of integers sharing the same digit multiset in a given base <span class="katex"><span class="katex-mathml">bb </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span></span></span></span> — when all digits are coprime to <span class="katex"><span class="katex-mathml">bb </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span></span></span></span> and the digital root is coprime to <span class="katex"><span class="katex-mathml">b−1b-1 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span></span></span></span>. For such admissible families, computational evidence across seven bases (<span class="katex"><span class="katex-mathml">b∈{7,8,9,10,12,14,16}b \in \{7,8,9,10,12,14,16\} </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">{</span><span class="mord">7</span><span class="mpunct">,</span><span class="mord">8</span><span class="mpunct">,</span><span class="mord">9</span><span class="mpunct">,</span><span class="mord">10</span><span class="mpunct">,</span><span class="mord">12</span><span class="mpunct">,</span><span class="mord">14</span><span class="mpunct">,</span><span class="mord">16</span><span class="mclose">}</span></span></span></span>) and digit counts <span class="katex"><span class="katex-mathml">k∈[5,30]k \in [5,30] </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">[</span><span class="mord">5</span><span class="mpunct">,</span><span class="mord">30</span><span class="mclose">]</span></span></span></span> shows that the aggregate density ratio clusters near the base-dependent value <span class="katex"><span class="katex-mathml">C(b)=(b/φ(b))⋅((b−1)/φ(b−1))C(b) = (b/\varphi(b)) \cdot ((b-1)/\varphi(b-1)) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">))</span><span class="mbin">⋅</span></span><span class="base"><span class="mopen">((</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">))</span></span></span></span>.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">The paper has three contributions, deliberately separated by epistemic status:</p> <ol class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-decimal flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Machine-verified (unconditional):</strong> a local-factor lemma showing that <span class="katex"><span class="katex-mathml">C(b)C(b) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span></span></span></span> arises exactly as a product of Hardy–Littlewood Euler factors at primes dividing <span class="katex"><span class="katex-mathml">b(b−1)b(b-1) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span></span></span></span>, in both cases <span class="katex"><span class="katex-mathml">p∣bp \mid b </span><span class="katex-html"><span class="base"><span class="mord mathnormal">p</span><span class="mrel">∣</span></span><span class="base"><span class="mord mathnormal">b</span></span></span></span> and <span class="katex"><span class="katex-mathml">p∣(b−1)p \mid (b-1) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">p</span><span class="mrel">∣</span></span><span class="base"><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span></span></span></span>. 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.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Empirical:</strong> aggregate ratios across seven bases up to <span class="katex"><span class="katex-mathml">k=30k=30 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">=</span></span><span class="base"><span class="mord">30</span></span></span></span> with bootstrap confidence intervals and Bonferroni adjustment. For base 10, a weighted regression on <span class="katex"><span class="katex-mathml">k∈{5,…,30}k \in \{5,\ldots,30\} </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">{</span><span class="mord">5</span><span class="mpunct">,</span><span class="minner">…</span><span class="mpunct">,</span><span class="mord">30</span><span class="mclose">}</span></span></span></span> gives <span class="katex"><span class="katex-mathml">C^=3.71\hat{C} = 3.71 </span><span class="katex-html"><span class="base"><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist"><span class="mord mathnormal">C</span><span class="accent-body"><span class="mord">^</span></span></span></span></span></span><span class="mrel">=</span></span><span class="base"><span class="mord">3.71</span></span></span></span> with 95% CI <span class="katex"><span class="katex-mathml">[3.62,3.80][3.62, 3.80] </span><span class="katex-html"><span class="base"><span class="mopen">[</span><span class="mord">3.62</span><span class="mpunct">,</span><span class="mord">3.80</span><span class="mclose">]</span></span></span></span>, containing <span class="katex"><span class="katex-mathml">C(10)=3.75C(10) = 3.75 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord">10</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mord">3.75</span></span></span></span> and excluding <span class="katex"><span class="katex-mathml">b/φ(b)=2.5b/\varphi(b) = 2.5 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mord">2.5</span></span></span></span>.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Conjectural:</strong> under an explicit Permutation Family Equidistribution Hypothesis (PFEH) and a Bombieri–Vinogradov-type level of distribution, the Hardy–Littlewood heuristic predicts <span class="katex"><span class="katex-mathml">πF(x)∼C(b) li(x)\pi_{\mathcal{F}}(x) \sim C(b) \,\mathrm{li}(x) </span><span class="katex-html"><span class="base"><span class="mord"><span class="mord mathnormal">π</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist"><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mord mathcal mtight">F</span></span></span></span><span class="vlist-s"></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mrel">∼</span></span><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mord"><span class="mord mathrm">li</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span>. The technical obstructions to upgrading this to a theorem are discussed explicitly.</li> </ol> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]"><strong>This Zenodo deposit contains:</strong></p> <ul class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-disc flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">main.pdf</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">paper/main.tex</code>: the paper (13 pages, Version 8).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">formal/</code>: complete Lean 4 / Mathlib formalisation of the unconditional results (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PrimeDensity.lean</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PrimeDensityExtended.lean</code>), with <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">lakefile.toml</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">lean-toolchain</code> pinned for reproducibility.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">src/</code>: Python pipeline for generating admissible families (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">generate_families_v2.py</code>) and running the statistical analysis (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">advanced_analysis.py</code>), plus four bash stage scripts and a <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">run_all.sh</code> driver.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">data/</code>: nine Parquet datasets covering all seven bases and digit-count ranges referenced in the paper (~3.5 MB).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">results/</code>: JSON analysis reports and PDF plots for base 10 (Table 1) and base 14 (Table 3).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">README.md</code>, <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">CITATION.cff</code>, and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">data/SCHEMA.md</code>: documentation and citation metadata.</li> </ul> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Full reproduction instructions are in <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">README.md</code>. 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.</p>
format Recurso digital
id zenodo_https___doi_org_10_5281_zenodo_20321000
institution Zenodo
language eng
publishDate 2026
publisher Zenodo
record_format zenodo
spellingShingle 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
Ferraiuolo, Giovanni
number theory
prime distribution
digital root
permutation families
Hardy-Littlewood conjecture
singular series
equidistribution
formal verification
Lean 4
Mathlib
reproducible research
computational number theory
<p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">We study prime density within *permutation families* — sets of integers sharing the same digit multiset in a given base <span class="katex"><span class="katex-mathml">bb </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span></span></span></span> — when all digits are coprime to <span class="katex"><span class="katex-mathml">bb </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span></span></span></span> and the digital root is coprime to <span class="katex"><span class="katex-mathml">b−1b-1 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span></span></span></span>. For such admissible families, computational evidence across seven bases (<span class="katex"><span class="katex-mathml">b∈{7,8,9,10,12,14,16}b \in \{7,8,9,10,12,14,16\} </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">{</span><span class="mord">7</span><span class="mpunct">,</span><span class="mord">8</span><span class="mpunct">,</span><span class="mord">9</span><span class="mpunct">,</span><span class="mord">10</span><span class="mpunct">,</span><span class="mord">12</span><span class="mpunct">,</span><span class="mord">14</span><span class="mpunct">,</span><span class="mord">16</span><span class="mclose">}</span></span></span></span>) and digit counts <span class="katex"><span class="katex-mathml">k∈[5,30]k \in [5,30] </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">[</span><span class="mord">5</span><span class="mpunct">,</span><span class="mord">30</span><span class="mclose">]</span></span></span></span> shows that the aggregate density ratio clusters near the base-dependent value <span class="katex"><span class="katex-mathml">C(b)=(b/φ(b))⋅((b−1)/φ(b−1))C(b) = (b/\varphi(b)) \cdot ((b-1)/\varphi(b-1)) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">))</span><span class="mbin">⋅</span></span><span class="base"><span class="mopen">((</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">))</span></span></span></span>.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">The paper has three contributions, deliberately separated by epistemic status:</p> <ol class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-decimal flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Machine-verified (unconditional):</strong> a local-factor lemma showing that <span class="katex"><span class="katex-mathml">C(b)C(b) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span></span></span></span> arises exactly as a product of Hardy–Littlewood Euler factors at primes dividing <span class="katex"><span class="katex-mathml">b(b−1)b(b-1) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span></span></span></span>, in both cases <span class="katex"><span class="katex-mathml">p∣bp \mid b </span><span class="katex-html"><span class="base"><span class="mord mathnormal">p</span><span class="mrel">∣</span></span><span class="base"><span class="mord mathnormal">b</span></span></span></span> and <span class="katex"><span class="katex-mathml">p∣(b−1)p \mid (b-1) </span><span class="katex-html"><span class="base"><span class="mord mathnormal">p</span><span class="mrel">∣</span></span><span class="base"><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mbin">−</span></span><span class="base"><span class="mord">1</span><span class="mclose">)</span></span></span></span>. 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.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Empirical:</strong> aggregate ratios across seven bases up to <span class="katex"><span class="katex-mathml">k=30k=30 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">=</span></span><span class="base"><span class="mord">30</span></span></span></span> with bootstrap confidence intervals and Bonferroni adjustment. For base 10, a weighted regression on <span class="katex"><span class="katex-mathml">k∈{5,…,30}k \in \{5,\ldots,30\} </span><span class="katex-html"><span class="base"><span class="mord mathnormal">k</span><span class="mrel">∈</span></span><span class="base"><span class="mopen">{</span><span class="mord">5</span><span class="mpunct">,</span><span class="minner">…</span><span class="mpunct">,</span><span class="mord">30</span><span class="mclose">}</span></span></span></span> gives <span class="katex"><span class="katex-mathml">C^=3.71\hat{C} = 3.71 </span><span class="katex-html"><span class="base"><span class="mord accent"><span class="vlist-t"><span class="vlist-r"><span class="vlist"><span class="mord mathnormal">C</span><span class="accent-body"><span class="mord">^</span></span></span></span></span></span><span class="mrel">=</span></span><span class="base"><span class="mord">3.71</span></span></span></span> with 95% CI <span class="katex"><span class="katex-mathml">[3.62,3.80][3.62, 3.80] </span><span class="katex-html"><span class="base"><span class="mopen">[</span><span class="mord">3.62</span><span class="mpunct">,</span><span class="mord">3.80</span><span class="mclose">]</span></span></span></span>, containing <span class="katex"><span class="katex-mathml">C(10)=3.75C(10) = 3.75 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord">10</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mord">3.75</span></span></span></span> and excluding <span class="katex"><span class="katex-mathml">b/φ(b)=2.5b/\varphi(b) = 2.5 </span><span class="katex-html"><span class="base"><span class="mord mathnormal">b</span><span class="mord">/</span><span class="mord mathnormal">φ</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mrel">=</span></span><span class="base"><span class="mord">2.5</span></span></span></span>.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><strong>Conjectural:</strong> under an explicit Permutation Family Equidistribution Hypothesis (PFEH) and a Bombieri–Vinogradov-type level of distribution, the Hardy–Littlewood heuristic predicts <span class="katex"><span class="katex-mathml">πF(x)∼C(b) li(x)\pi_{\mathcal{F}}(x) \sim C(b) \,\mathrm{li}(x) </span><span class="katex-html"><span class="base"><span class="mord"><span class="mord mathnormal">π</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist"><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mord mathcal mtight">F</span></span></span></span><span class="vlist-s"></span></span></span></span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span><span class="mrel">∼</span></span><span class="base"><span class="mord mathnormal">C</span><span class="mopen">(</span><span class="mord mathnormal">b</span><span class="mclose">)</span><span class="mord"><span class="mord mathrm">li</span></span><span class="mopen">(</span><span class="mord mathnormal">x</span><span class="mclose">)</span></span></span></span>. The technical obstructions to upgrading this to a theorem are discussed explicitly.</li> </ol> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]"><strong>This Zenodo deposit contains:</strong></p> <ul class="[li_&]:mb-0 [li_&]:mt-1 [li_&]:gap-1 [&:not(:last-child)_ul]:pb-1 [&:not(:last-child)_ol]:pb-1 list-disc flex flex-col gap-1 pl-8 mb-3"> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">main.pdf</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">paper/main.tex</code>: the paper (13 pages, Version 8).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">formal/</code>: complete Lean 4 / Mathlib formalisation of the unconditional results (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PrimeDensity.lean</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">PrimeDensityExtended.lean</code>), with <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">lakefile.toml</code> and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">lean-toolchain</code> pinned for reproducibility.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">src/</code>: Python pipeline for generating admissible families (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">generate_families_v2.py</code>) and running the statistical analysis (<code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">advanced_analysis.py</code>), plus four bash stage scripts and a <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">run_all.sh</code> driver.</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">data/</code>: nine Parquet datasets covering all seven bases and digit-count ranges referenced in the paper (~3.5 MB).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">results/</code>: JSON analysis reports and PDF plots for base 10 (Table 1) and base 14 (Table 3).</li> <li class="font-claude-response-body whitespace-normal break-words pl-2"><code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">README.md</code>, <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">CITATION.cff</code>, and <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">data/SCHEMA.md</code>: documentation and citation metadata.</li> </ul> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">Full reproduction instructions are in <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">README.md</code>. 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.</p>
title 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
topic number theory
prime distribution
digital root
permutation families
Hardy-Littlewood conjecture
singular series
equidistribution
formal verification
Lean 4
Mathlib
reproducible research
computational number theory
url https://doi.org/10.5281/zenodo.20321000

Similar Items