2607.19337v1 / Repro.lean

all files

import Mathlib.Data.Nat.Prime.Nth
import Mathlib.Data.PNat.Basic
import Mathlib.Data.Set.Card
import Mathlib.NumberTheory.PrimeCounting
import Mathlib.RingTheory.Polynomial.Basic

/-!
# Reproduction of Seki, “On the A-transcendence of a Champernowne-type constant”

The paper numbers primes starting at `p₁ = 2`, whereas `Nat.nth Nat.Prime` is
zero-based.  Keeping that shift explicit is essential: the polynomial is evaluated at the
paper's positive index `n`, not at the zero-based prime index.
-/

namespace ChampernowneA

/-- The paper's one-based `n`-th prime.  The value at zero is irrelevant to the theorem. -/
noncomputable def paperPrime (n : ℕ) : ℕ := Nat.nth Nat.Prime (n - 1)

@[simp] theorem paperPrime_one : paperPrime 1 = 2 := by simp [paperPrime]
@[simp] theorem paperPrime_two : paperPrime 2 = 3 := by simp [paperPrime]

/-- The exact assertion of Theorem 1.1 in the paper.

For every nonzero integer polynomial, the set of positive indices at which the one-based
`n`-th prime does not divide the value of the polynomial at `n` is infinite.
-/
def MainTheorem : Prop :=
  ∀ f : Polynomial ℤ, f ≠ 0 →
    Set.Infinite {n : ℕ | 0 < n ∧ ¬(paperPrime n : ℤ) ∣ f.eval (n : ℤ)}

/-! ## Finite and numerical checks -/

/-- At the paper's `n`-th prime, the prime-counting function is exactly `n`.
This proves the first displayed sequence `π(p) = (1,2,3,...)`, not merely its first 20 terms. -/
theorem primeCounting_paperPrime {n : ℕ} (hn : 0 < n) :
    Nat.primeCounting (paperPrime n) = n := by
  rw [paperPrime, Nat.primeCounting, Nat.primeCounting']
  rw [Nat.count_nth_succ_of_infinite Nat.infinite_setOfPred_prime]
  omega

example :
    (List.range 20).map (fun i ↦ Nat.primeCounting (paperPrime (i + 1))) =
      [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20] := by
  simp [primeCounting_paperPrime]
  native_decide

/-- The paper's displayed integer representatives for `π²(p)`, through the twentieth prime. -/
example :
    (List.range 20).map (fun i ↦ Nat.primeCounting (i + 1)) =
      [0, 1, 2, 2, 3, 3, 4, 4, 4, 4, 5, 5, 6, 6, 6, 6, 7, 7, 8, 8] := by
  native_decide

/-- The paper's displayed integer representatives for `π³(p)`, through the twentieth prime. -/
example :
    (List.range 20).map (fun i ↦ Nat.primeCounting (Nat.primeCounting (i + 1))) =
      [0, 0, 1, 1, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4, 4, 4] := by
  native_decide

/-- There are exactly `d(d+1)` cancellation equations indexed by
`0 ≤ u ≤ d` and `0 ≤ v ≤ d-1`, as asserted just before (2.2). -/
theorem cancellationEquation_count (d : ℕ) :
    ((Finset.range (d + 1)).product (Finset.range d)).card = d * (d + 1) := by
  simp [Nat.mul_comm]

/-- The first twenty one-based indices paired with their primes, for executable bounded search. -/
def firstTwentyIndexPrime : List (ℕ × ℕ) :=
  [(1, 2), (2, 3), (3, 5), (4, 7), (5, 11), (6, 13), (7, 17), (8, 19), (9, 23),
   (10, 29), (11, 31), (12, 37), (13, 41), (14, 43), (15, 47), (16, 53),
   (17, 59), (18, 61), (19, 67), (20, 71)]

example : firstTwentyIndexPrime.all (fun np ↦
    decide (np.2.Prime ∧ Nat.primeCounting np.2 = np.1)) = true := by
  native_decide

/-- Horner evaluation for a list of coefficients in ascending order. -/
def evalCoeffList : List ℤ → ℤ → ℤ
  | [], _ => 0
  | a :: as, n => a + n * evalCoeffList as n

/-- All 625 coefficient vectors of length four with coefficients in `[-2,2]`. -/
def smallCoefficientVectors : List (List ℤ) :=
  let s : List ℤ := [-2, -1, 0, 1, 2]
  s.flatMap fun a ↦ s.flatMap fun b ↦ s.flatMap fun c ↦ s.map fun d ↦ [a, b, c, d]

/-- Bounded counterexample search: every nonzero polynomial of degree at most three with all
coefficients in `[-2,2]` already has a witness to Theorem 1.1 among `1 ≤ n ≤ 20`. -/
def smallCounterexampleSearchPasses : Bool :=
  smallCoefficientVectors.all fun cs ↦
    cs == [0, 0, 0, 0] || firstTwentyIndexPrime.any fun np ↦
      decide (¬(np.2 : ℤ) ∣ evalCoeffList cs (np.1 : ℤ))

example : smallCounterexampleSearchPasses = true := by native_decide

end ChampernowneA

#print axioms ChampernowneA.primeCounting_paperPrime