Trace — 2607.19337v1

DECLARATION — Central claim: if p_n is the n-th prime with p_1 = 2, then for every nonzero integer polynomial f there are infinitely many positive integers n for which p_n does not divide f(n); equivalently, the Champernowne-type finite-adelic element (n mod p_n) is A-transcendental in the paper's strong sense. Declared target: R3 (core). I expect to formalize the central theorem faithfully first (including one-based prime indexing), verify every explicit finite/decidable numerical claim, and formalize with no sorry the new algebraic cancellation and nonvanishing lemmas at the heart of the paper's proof. I do not expect R4 because the surrounding analytic input includes Maynard–Tao bounded prime gaps, which is not expected to be available in mathlib.

R1 first elaboration failed: Nat.nth is noncomputable, so paperPrime could not be compiled and native_decide could not prove its first two values. This ruled out direct executable use of mathlib's nth predicate enumerator.

R1 achieved: Repro.lean now gives an exact Prop-valued formalization of Theorem 1.1, with paperPrime n := Nat.nth Nat.Prime (n - 1), positivity of n, integer polynomial evaluation at n, integer divisibility, and Set.Infinite. The one-based indexing checks p_1=2 and p_2=3 elaborate. lake env lean Repro.lean succeeds.

R2 inspection found Nat.primeCounting is executable (Nat.count Prime), while paperPrime remains noncomputable. Mathlib supplies count_nth_succ_of_infinite, allowing a proof that π(p_n)=n for every positive one-based n.

The first 20-term π(p) check initially simplified to the concrete list map but simp did not normalize the whole list. Adding native_decide only after the general theorem-based simplification closed the finite residue.

R2 achieved for all finite/decidable/numerical assertions in the paper: proved π(p_n)=n generally; native_decide verified the exact 20 terms printed for π²(p) and π³(p); the printed π(p) list follows and its 20 terms were checked; and the equation-index set in (2.2) was proved to have d(d+1) elements. Repro.lean elaborates cleanly.

R3 approach: encode (2.2) as a d(d+1)-by-(d(d+1)+1) integer matrix. Instead of clearing denominators from a rational kernel vector, use mathlib's strong-rank-condition finrank theorem directly over ℤ to show the matrix linear map cannot be injective; subtract two equal-image vectors to obtain a nonzero integral kernel vector.

First integer-kernel elaboration failed in two useful ways: finrank simplification did not normalize the product-indexed codomain, and Function.not_injective_iff returns map equality before point inequality. Replacing finrank_fin_fun by finrank_pi plus cardinality lemmas, normalizing multiplication order, and swapping the extracted hypotheses fixed both.

Core milestone: exists_integer_cancellation now proves the exact nontrivial integer solution asserted for (2.2), for all d and all integer tuples h. Core.lean elaborates.

Initial polynomial definitions failed because nested Polynomial addition/product uses noncomputable classical instances; marking yFactor and rhoWithout noncomputable fixed the definition issue. The self-node evaluation also needed an explicit commutative normalization of -h_i+h_j to h_j-h_i.

Direct rewriting under evalRingHom did not match eval lemmas, and broad simp turned zero-product goals into irrelevant disjunctions. Changing the goals back to Polynomial.eval form and rewriting eval_mul/eval_C plus the node lemmas isolated the intended terms cleanly.

Core milestone: rho, rhoWithout, yFactor_mul_rhoWithout, shifted_polynomial_expansion, eval_Phi_at_node, and Phi_ne_zero formalize the interpolation/nonvanishing paragraph. Phi is the paper's bivariate polynomial (outer variable y), and evaluation at y=-h_i isolates c_i f(x+i) times the product of h_j-h_i.

The first induction for the finite geometric identity used congr at the wrong addition nesting, producing spurious obligations. Reassociating the new sum, cancelling the common prefix, then field_simp/ring proved the exact identity.

The first generic double-cancellation proof chose u,v summation order opposite to the order generated by mul_sum. Reordering the target to v then u, applying sum_comm twice, and proving each scalar rearrangement with ring closed the proof.

The first specialization to ℚ left the inner Fin d binder underconstrained and inference timed out at the generic theorem call. Explicit binder annotations and named type arguments eliminated the ambiguity; exact_mod_cast then transported every integer moment equation.

Declared R3 achieved: Core.lean proves the nonzero integer kernel vector, the exact rho/Phi construction and Phi nonvanishing, the b_u(n) shifted-polynomial expansion, the finite geometric-series identity, a general double moment cancellation theorem, and paper_cancellation_over_rationals matching the zero computation after (2.4). No sorry or user axioms occur.

R4 availability audit: repository search found neither Maynard–Tao bounded gaps nor a prime number theorem/nth-prime asymptotic in mathlib; only Chebyshev-type prime-counting bounds are present. Thus the two analytic inputs needed for (2.1) and (2.3) are not available to instantiate a full proof.

Packaging dead end: importing root-level Core from Repro failed because the mathlib lake library search path contains built .olean modules, not arbitrary root .lean files. Kept Repro.lean and Core.lean independently checkable with lake env lean, avoiding a hidden prebuild requirement.

R2 strengthened by executable counterexample search: verified the first 20 index/prime pairs and exhaustively checked all 625 nonzero coefficient vectors of degree at most 3 with coefficients in [-2,2]; each has a theorem witness among n=1,...,20. native_decide returns true.

Final verification succeeded: lake env lean Repro.lean and lake env lean Core.lean both elaborate; grep finds no sorry, axiom declaration, or unsafe declaration; every #print axioms result contains only mathlib's standard propext, Classical.choice, and Quot.sound; jq validates all trace.jsonl records.

VERDICT: reproduced at declared target R3. R1, R2, and the paper's new algebraic core are complete with checked Lean proofs. Further climb to R4 stops at genuinely absent/deep analytic prerequisites: Maynard–Tao bounded prime gaps and the prime-number-theorem asymptotic p_n ~ n log n; repository searches found no usable formalizations, and recreating either theorem is not a distinct tractable continuation of this run.