Ramanujan's 1/π Series and Harmonic Numbers: Proof and Verification

A proof, with computer verification, of Conjecture 1 from MathOverflow question 507693 on Ramanujan-type 1/π series and harmonic numbers. For the rational hypergeometric series of levels N = 1, 2, 3, 4, the index derivative of the summand satisfies Σ f'(n) = 2πi τ̃ Σ f(n), with τ̃ = τ when a > 0 and τ̃ = τ − 1 when a < 0. Taking real parts gives the conjectured Re Σ f'(n) = −2π Im(τ) Σ f(n). The identity is proved for every τ on the imaginary axis above i/√N, and for every τ on the line Re τ = 1/2 above the corner of the fundamental domain of Γ0(N)+ with −1 ≤ 1/JN(τ) < 0. It does not use complex multiplication. The 36 convergent series of the Cohen–Guillera table follow as a corollary, using the pairing JN(τ) = a printed in that table. The proof relies on cited published results: Abramowitz–Stegun 15.3.10, Ramanujan's inversion theorems (Jacobi, and Berndt–Bhargava–Garvan 1995), and standard facts on modular forms (Sturm's bound, the Gordon–Hughes–Newman criterion and Ligozat's cusp orders). Each is cited by page. Clausen's identity and the fundamental domain are proved in the text. The modular-form identities linking the inversion theorems to the Hauptmoduln are proved by exact coefficient comparison up to the Sturm bound. The Python package checks each intermediate claim and tests the identity on all 36 series and at non-CM points. This is not a peer-reviewed publication. The work was developed with AI assistance, and the adversarial reviews it went through were also AI-based. No literature-priority claim is made. The proof and numerical reports are under Creative Commons Attribution 4.0; the software is under MIT. The series parameters are transcribed from the Cohen–Guillera table and are credited to its authors. Third-party papers and books are not included. Reproduction uses Python 3.11 or later with mpmath and sympy. See the README.