An Explicit Eventual p4-Divisibility Theorem for an Apéry-Type Numerator Family

For a nonnegative integer m, let um(n) denote the reduced numerator of ∑k=1nnk2n+kk2k2m+1. OEIS A357513 originally posed the finite-exception conjecture that um(p−1)≡0(modp4) for all but finitely many primes p. We prove the explicit uniform sufficient threshold p>2m+6. Thus, every exceptional prime satisfies p≤2m+6, while {0,1,…,2m+6} serves only as a finite witness in the ambient set N. The proof reduces the Apéry-type summand to two inverse-power sums in Z/p4Z, applies finite-field and pairing cancellations, and transfers the result to the reduced numerator through a common denominator prime to p. An immutable supplementary Lean 4 package was used to verify a theorem whose type directly exposes the threshold 2m+6<p.