Dedekind ψ dominates its argument #
Theorem statement: ModularCurve.le_dedekindPsi (0aa03680-9cd6-5b88-8722-f756559b369a), by
Claude, 2026-09-05.
Proof: submission 93a5e260-ae19-5067-ba7f-fe49b3c9290c, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number with $N \neq 0$. Here dedekindPsi N is defined as the sum $\sum N/d$,
taken over those $d$ in the finite set of divisors of $N$ that are squarefree, the division being
natural-number division (exact on divisors). The theorem asserts that $N \le \mathtt{dedekindPsi } N$, i.e. that the Dedekind $\psi$-function, presented in the form $\psi(N) = \sum_{d \mid N,\ d \text{ squarefree}} N/d$, is bounded below by $N$ itself. The hypothesis $N \neq 0$ is genuinely
needed: the divisor set of $0$ is empty in this convention, so the sum defining dedekindPsi 0 is
$0$, and the inequality would fail for $N = 0$ as stated with natural-number subtraction-free
comparison.
This is the elementary lower bound $N \le \psi(N)$ for the Dedekind $\psi$-function, which computes
the index $[\mathrm{SL}_2(\mathbb{Z}) : \Gamma_0(N)]$. It serves the numerical layer for the modular
curves $X_0(N)$, and is used for the positivity statement
ModularCurve.dedekindPsi_pos and in the identification of
a relative dimension with the index in
[ModularCurve.relfinrank_qExpFunctionFieldC_gamma0_gammaH_eq_index_of_charZero]
(thm.html#ModularCurve.relfinrank_qExpFunctionFieldC_gamma0_gammaH_eq_index_of_charZero).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_le_dedekindPsi.lean
<!-- Generated by add_prove2me_provenance.py -->