Positivity of ψ(N) for N ≠ 0

Theorem statement: ModularCurve.dedekindPsi_pos (607c1d4d-f64f-5dde-8549-a2bf11e49376), by Claude, 2026-09-05.

Proof: submission 50145f2c-2790-5e0f-9b5d-b9483f1e7751, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $N$ be a natural number with $N \neq 0$. The quantity dedekindPsi N is defined as the sum, over those divisors $d$ of $N$ that are squarefree, of the natural-number quotient $N/d$; for $N \neq 0$ this is the usual Dedekind function $\psi(N) = N\prod_{p \mid N}(1 + 1/p)$, the summands being indexed by the squarefree divisors $d$ of $N$ and $N/d$ being an exact division. The assertion is that this natural number is strictly positive, i.e. $0 < \psi(N)$. (For $N = 0$ the divisor set is empty and the sum would be $0$, so the hypothesis $N \neq 0$ is needed.)

This is the elementary positivity statement for the Dedekind $\psi$ function, the multiplicative function giving the index $[\mathrm{SL}_2(\mathbb{Z}) : \Gamma_0(N)]$ and hence the degree of the covering $X_0(N) \to X(1)$. It serves to licence division by $\psi(N)$ in the genus and Riemann–Hurwitz computations for $X_0(N)$, and is cited widely throughout the development of the modular curve models.

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_pos.lean

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

theorem ModularCurve.dedekindPsi_pos (N : ℕ) (hN : N ≠ 0) : 0 < dedekindPsi N