2607.20408v1 / Repro/PaperErrors.lean

all files

import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.NumberTheory.LegendreSymbol.ZModChar

/-!
# Two literal errors in the paper under reproduction

These results are not used to manufacture the main theorem.  They record two
independently checkable defects found while auditing the proof.
-/

open scoped ArithmeticFunction.Moebius

namespace PaperErrors

/--
At `ε = 1/2`, the paper's definition of `g₂(n)` specializes to this divisor sum
(over `ℚ`, only to make the counterexample exact and computational).
-/
def g2AtHalf (n : ℕ) : ℚ :=
  ∑ q ∈ n.divisors, ((ArithmeticFunction.moebius q : ℤ) : ℚ) ^ 2 / q

/-- The Euler product printed in the paper, with a minus sign. -/
def printedProductAtHalf (n : ℕ) : ℚ :=
  ∏ p ∈ n.primeFactors, (1 - 1 / (p : ℚ))

/-- The divisor-sum definition gives `1 + 1/2 = 3/2` at `n = 2`. -/
example : g2AtHalf 2 = 3 / 2 := by
  have hdiv : (2 : ℕ).divisors = {1, 2} := by decide
  rw [g2AtHalf, hdiv]
  rw [Finset.sum_insert (by decide : 1 ∉ ({2} : Finset ℕ)), Finset.sum_singleton]
  rw [ArithmeticFunction.moebius_apply_prime Nat.prime_two]
  norm_num [ArithmeticFunction.moebius_apply_prime]

/-- The product printed after Lemma 2.2 gives `1 - 1/2 = 1/2` at `n = 2`. -/
example : printedProductAtHalf 2 = 1 / 2 := by
  norm_num [printedProductAtHalf, Nat.primeFactors]

/-- Thus the displayed Euler-product identity after Lemma 2.2 is false. -/
theorem g2_product_sign_counterexample :
    g2AtHalf 2 ≠ printedProductAtHalf 2 := by
  rw [show g2AtHalf 2 = 3 / 2 by
        have hdiv : (2 : ℕ).divisors = {1, 2} := by decide
        rw [g2AtHalf, hdiv]
        rw [Finset.sum_insert (by decide : 1 ∉ ({2} : Finset ℕ)), Finset.sum_singleton]
        rw [ArithmeticFunction.moebius_apply_prime Nat.prime_two]
        norm_num [ArithmeticFunction.moebius_apply_prime],
    show printedProductAtHalf 2 = 1 / 2 by
        norm_num [printedProductAtHalf, Nat.primeFactors]]
  norm_num

/-- The complex-valued character modulo `4` attached to the discriminant `-4`. -/
def chiNegFour : DirichletCharacter ℂ 4 :=
  ZMod.χ₄.ringHomComp (Int.castRingHom ℂ)

/-- `χ_{-4}` is odd. -/
theorem chiNegFour_odd : chiNegFour.Odd := by
  change ((ZMod.χ₄.ringHomComp (Int.castRingHom ℂ)) (-1)) = -1
  rw [show (-1 : ZMod 4) = 3 by decide]
  norm_num [ZMod.χ₄]

/--
Consequently mathlib's standard gamma factor for `χ_{-4}` is `Gammaℝ (s+1)`,
not the even-character factor `Gammaℝ s` used in Lemma 2.1 of the paper.
-/
theorem chiNegFour_gammaFactor (s : ℂ) :
    DirichletCharacter.gammaFactor chiNegFour s = Complex.Gammaℝ (s + 1) :=
  chiNegFour_odd.gammaFactor_def s

end PaperErrors