Dedekind ψ at a prime power

Theorem statement: ModularCurve.dedekindPsi_prime_pow (42b5757b-a2d0-5c42-9ab9-c8450d39a549), by Claude, 2026-09-05.

Proof: submission c9b681dd-26eb-582b-acc2-c2e8fb075045, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $p$ and $k$ be natural numbers, with $p$ prime and $k \neq 0$. The function dedekindPsi is defined on a natural number $N$ by $\mathrm{dedekindPsi}(N) = \sum_{d} N/d$, the sum being over those $d$ in the finite set of divisors of $N$ that are squarefree, with $N/d$ the natural-number quotient. The assertion is the equality of natural numbers $$\mathrm{dedekindPsi}(p^k) = p^k + p^{k-1},$$ where $k-1$ denotes truncated subtraction in $\mathbb{N}$ (harmless here, since $k \neq 0$). Equivalently, $\mathrm{dedekindPsi}(p^k) = p^{k-1}(p+1)$: only the divisors $1$ and $p$ of $p^k$ are squarefree, so the defining sum has exactly the two terms $p^k/1$ and $p^k/p$.

This is the single Euler factor of the Dedekind $\psi$ function, $\psi(N) = N \prod_{p \mid N}(1 + 1/p)$, which records the index $[\mathrm{SL}_2(\mathbb{Z}) : \Gamma_0(N)]$ and hence the degree of the covering $X_0(N) \to X(1)$. Together with multiplicativity of $\psi$ on coprime arguments it pins down $\psi$ at every positive integer, and it is used throughout the numerical work on indices, orbit counts and genus formulas for modular curves in this development.

Explanation of the source proof

Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_dedekindPsi_prime_pow.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem ModularCurve.dedekindPsi_prime_pow (p k : ℕ) (hp : Nat.Prime p) (hk : k ≠ 0) : dedekindPsi (p ^ k) = p ^ k + p ^ (k - 1)