Five from inverse pairs

For a prime p let S(p) = ∑ 1/√(a·ā) over a = 1, …, p−1, where ā is the inverse of a modulo p in 1, …, p−1. Nilotpal Kanti Sinha asked on Mathematics Stack Exchange (question 5146740) whether S(p) → 5, as computations suggested. This note proves S(p) = 5 + O(p^(−1/8+ε)) (Theorem 1).

The proof compares the inverse pairs (a, ā) with all pairs (a, b), scaled by 1/p. The all-pairs sum factors as C(p) = (∑ 1/√a)²/p, which tends to 4 by telescoping square roots (Lemma 2), and the term a = 1 gives the remaining 1. An exact layer-cake identity turns S(p) − 1 − C(p) into a weighted sum, over heights m, of the difference between the two counts under the hyperbola xy = m. For large m that difference is controlled by Weil’s bound for Kloosterman sums, counted in rectangles and stacked into staircases (Lemmas 3 and 4). For small m the divisor bound controls it (Lemma 5).

Preprint v1, 10 October 2026, not peer reviewed. Every step except Weil’s bound is formally verified in Lean 4 (lean/, standard axioms only). Weil’s bound (1948) is not in Mathlib; it enters the Lean theorems as an explicit hypothesis, never as an axiom. The author used AI tools (Claude, Anthropic) in this work, as described in the paper’s acknowledgement, and is responsible for its content.