2607.19337v1 / README.md

all files

# Reproduction report: Seki's Champernowne-type theorem

Status: **reproduced**.

The formalization is in [`ChampernowneA.lean`](./ChampernowneA.lean).  It proves
the paper's central result:

```lean
theorem theorem_1_1 (hPNT : PrimeNumberTheorem)
    (hMT : MaynardTaoBoundedGaps) (f : ℤ[X]) (hf : f ≠ 0) :
    {n : ℕ | 0 < n ∧ ¬(paperPrime n : ℤ) ∣ f.eval (n : ℤ)}.Infinite
```

Here `paperPrime n := Nat.nth Nat.Prime (n - 1)`, so `paperPrime 1 = 2`.
Thus the indexing and the restriction to positive integers agree literally
with the paper.

## External hypotheses

Mathlib does not currently contain either of the two analytic-number-theory
inputs explicitly invoked by the paper.  They are isolated as named
hypotheses, with no other assumed propositions:

```lean
def PrimeNumberTheorem : Prop :=
  (fun n : ℕ ↦ (nthPrime n : ℝ)) ~[atTop]
    (fun n : ℕ ↦ (n : ℝ) * Real.log n)

def MaynardTaoBoundedGaps : Prop :=
  ∀ k : ℕ, ∃ B : ℕ,
    {n : ℕ | nthPrime (n + k) - nthPrime n ≤ B}.Infinite
```

The first is the standard nth-prime form of the prime number theorem.  The
second is precisely the bounded-cluster consequence of Maynard--Tao used in
the manuscript (`liminf (p_{n+k}-p_n) < ∞`).  The formal theorem has no
additional hypotheses.  In particular, the recurring exact gap pattern, all
linear algebra, and every asymptotic consequence used below are proved in the
file rather than assumed.

## What was built

The proof follows the manuscript's contradiction argument.

1. `fixed_prime_cluster` turns Maynard--Tao bounded diameter into a strictly
   increasing fixed offset tuple `0 = h₀ < ... < hₖ` occurring infinitely
   often.  The proof uses an infinite-fiber pigeonhole argument over the
   finite set of possible offset vectors.

2. `integer_cancellation_coefficients` constructs the nonzero integer vector
   `c`.  It forms a `d(d+1)` by `d(d+1)+1` matrix over `ℚ`, proves its kernel
   nontrivial by a finrank inequality, and clears every rational denominator
   in `clear_denominators`.

   The paper indexes the rows by the coefficients of `j^u h_j^v`.  The Lean
   file uses the equivalent rows given by the coefficients of
   `(-h_j)^v f(X+j)`.  Each shifted polynomial has degree at most `d`, so this
   is still exactly `d(d+1)` equations, and it directly yields

   ```text
   Σ_j c_j f(n+j) (-h_j)^v = 0,  0 ≤ v < d.
   ```

   This change is only a change of row basis/specialization in the same
   underdetermined homogeneous system; it does not strengthen a hypothesis or
   alter the auxiliary polynomial.

3. `auxiliaryPhi` is literally

   ```text
   Φ(x,y) = Σ_j c_j f(x+j) ∏_{i≠j} (y+h_i).
   ```

   `auxiliaryPhi_ne_zero` proves nonvanishing by specializing `y=-h_i`,
   exactly as in the paper.

4. The PNT part is developed rather than hidden behind a tailored hypothesis.
   `primeMonomial_isEquivalent` proves

   ```text
   n^i p_n^j ~ n^(i+j) (log n)^j.
   ```

   `finite_bivariate_sum_eventually_ne_zero` orders monomials first by total
   degree and then by the prime exponent, and proves the leading monomial
   dominates all others.  `bivariate_eventually_ne_zero` then establishes the
   formal counterpart of equation (2.3) for every nonzero bivariate
   polynomial.

5. `finite_geometric_reciprocal` proves the exact finite reciprocal expansion.
   `reciprocal_sum_eq_remainder` applies all cancellation equations, and
   `remainder_sum_tendsto_zero` proves the surviving remainder tends to zero.
   Divisibility on a recurring prime cluster makes the reciprocal sum an
   integer.  Its real norm is eventually less than one, so it is zero.

6. The resulting equality `Φ(n,p_n)=0` contradicts the PNT nonvanishing lemma.
   `infinitely_many_nthPrime_not_dvd` proves the zero-indexed form, and
   `theorem_1_1` shifts the polynomial by one to obtain the paper's exact
   one-indexed statement.

The degree-zero case is not split off: all definitions and estimates remain
valid for `d=0`, so the same proof covers nonzero constant polynomials.

## Verification

From this directory:

```bash
lake env lean ChampernowneA.lean
```

The command succeeds with Lean's exit code 0.  Integrity checks used for this
report:

```bash
rg -n '\bsorry\b|\badmit\b|^\s*axiom\b' ChampernowneA.lean
lake env lean ChampernowneA.lean
```

There are no `sorry`, `admit`, or locally declared axioms.  The only
unformalized mathematical inputs are the two explicit proposition parameters
`PrimeNumberTheorem` and `MaynardTaoBoundedGaps` above.