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 the prime-indexed Champernowne-type element is strongly 𝒜-transcendental. Its algebraic proof mechanism is now machine-checked, isolating the remaining dependence on two deep analytic number-theory results.
Reproduction
✓ reproduced
Attempted: For every nonzero integer polynomial f, infinitely many positive n satisfy p_n ∤ f(n), where p_1 = 2; declared target: R3 core formalization.
R1–R3 achieved in Repro.lean and Core.lean: faithful statement, all displayed computations, an exhaustive 625-polynomial bounded search, and the integer-kernel, polynomial-nonvanishing, geometric-series, and cancellation lemmas. R4 requires unavailable formalizations of Maynard–Tao bounded prime gaps and p_n ~ n log n. Independent re-verification: both files elaborate cleanly; the core lemmas depend only on propext, Classical.choice, Quot.sound; the finite computational checks use native_decide, i.e. Lean's compiled-evaluation axiom.
trace (21 events) · code (2 files)