On the π-transcendence of a Champernowne-type constant
Let p_n denote the n-th prime. We prove that for every nonzero polynomial f(x)ββ€[x], there exist infinitely many positive integers n such that p_n\nmid f(n).
The paper proves that no nonzero integer polynomial can satisfy p_n \mid f(n) for all sufficiently large n, resolving the strong π-transcendence conjecture for the Champernowne-type element (n \bmod p_n)_{p_n}.
Reproduction
β* reproduced, conditional on declared hypotheses
Attempted: Assuming the prime number theorem in the form p_n βΌ n log n and the MaynardβTao bounded-gap statement (liminf over m of p_{m+k} β p_m finite for every k), every nonzero f β β€[x] has infinitely many positive integers n such that p_n β€ f(n), with p_1 = 2.
A zero-sorry Lean proof: all pigeonhole, linear-algebra, denominator-clearing, polynomial, asymptotic, and small-integer steps are proved from mathlib, with exactly the two disclosed deep hypotheses β both stated as explicit Prop-valued assumptions, not axioms, and both genuinely external research programs (neither is formalized anywhere). Independent re-verification: the file elaborates cleanly, kernel-checked; the hypothesis structure was audited directly. Details in the run's README.
trace (303 events) Β· code (2 files)