Finite Ramanujan Divisor Identity
Abstract
The normalized sum of finite Ramanujan phases over the divisors of d is the indicator that d divides n.
Theorem 1.1 (The sum over all divisor moduli).
Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/FiniteRamanujanDivisorIdentity.sum_ramanujanSum_divisors (✓ std3). ∎
Source. Repository-derived.
Commentary.
For positive d and natural n, the sum of ramanujanSum q n over all divisors q of d is d when d divides n and zero otherwise.
Definition 1.2 (The finite Ramanujan phase sum).
Formalization. D5/S3/Analytic/Certified/FiniteRamanujanDivisorIdentity.ramanujanSum (✓ std3).
Source. Repository-derived.
Commentary.
For natural q and n, ramanujanSum q n is exactly the finite sum of exp(2 pi i a n / q) over natural residues a below q that are coprime to q. In particular, the phase carrier is not replaced by an arithmetically equivalent definition.
Theorem 1.3 (Normalized Ramanujan sums reconstruct the divisor indicator).
Proof. Machine-checked in Lean as D5/S3/Analytic/Certified/FiniteRamanujanDivisorIdentity.divisorIndicator_eq_normalized_sum_ramanujanSum (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every positive natural d and natural n, the indicator of d dividing n equals one over d times the sum of c_q(n) over all positive divisors q of d. This is formula (4) in the finite reconstruction argument.
The proof first constructs the coprime-index bijection from the source phases to primitive q-th roots. Primitive roots of all orders q dividing d partition the d-th roots of unity; the complete root sum is then d when d divides n and zero otherwise.
This module does not prove the von Mangoldt equality, the weighted finite phase expansion, or independence of that expansion from tau. Those remain separate obligations.