Prove2Me

Nielsen calibration product prod(1−1/ni)=a/(a+1)\\prod (1-1/n_i) = a/(a+1)

Proved
OddPerfectNumber.nielsen_calibration_prod

by curiyu · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

divisor-sumsnumber-theoryopen-problemperfect-numbers

This is the calibrating product identity behind Lemma 1 of Nielsen 2003 (Section 2), in the form made explicit as equation (11) of the 2024 exposition.

Let a≥1a \ge 1 and r≥1r \ge 1 be integers, and put A=a+1A = a+1. Consider the calibrating integers ni=A2i−1+1n_i = A^{2^{i-1}} + 1 for 1≤i<r1 \le i < r together with nr=A2r−1n_r = A^{2^{r-1}}. Then

∏i=1r(1−1ni)=aa+1.\prod_{i=1}^{r}\left(1-\frac{1}{n_i}\right) = \frac{a}{a+1}.

The identity is a telescoping consequence of the factorization A2m−1=(A−1)∏i<m(A2i+1)A^{2^{m}} - 1 = (A-1)\prod_{i<m}(A^{2^{i}}+1). In the paper this sequence is the extremal example: it satisfies the hypothesis (∗)(*) of Lemma 1 with equality on the left, and Cook's comparison lemma shows every other admissible tuple has partial products dominating it, which is how the maximality argument in Lemma 1 gets off the ground.

Formalization Note The sequence is 00-indexed in Lean; the product is split into the first r−1r-1 factors over Finset.range (r - 1) and the distinguished last factor, and all divisions are in Q\mathbb{Q} with explicit casts.

Preamble
import Mathlib
open BigOperators Finset
Formal statement
namespace OddPerfectNumber

theorem nielsen_calibration_prod (a r : ℕ) (ha : 0 < a) (hr : 0 < r) :
    (∏ i ∈ Finset.range (r - 1), (1 - 1 / (((a + 1) ^ (2 ^ i) + 1 : ℕ) : ℚ))) *
      (1 - 1 / ((((a + 1) ^ (2 ^ (r - 1)) : ℕ)) : ℚ)) =
      ((a : ℕ) : ℚ) / (((a : ℕ) : ℚ) + 1) := by
  sorry

end OddPerfectNumber
Source
P. P. Nielsen, An upper bound for odd perfect numbers, INTEGERS 3 (2003), #A14, Section 2 (ni construction); see also equation (11) of the 2024 exposition, https://math.colgate.edu/~integers/y114/y114.pdf

View graph