A Weight-5 Apéry-like Binomial Sum, its Calabi–Yau 4-fold Period, and Supercongruences

We study the binomial sum S(n) = Σ_{k=0}^{n} C(n,k)^4 · C(n+k,k), a weight-(4,1) Apéry-like sequence. We prove that S(n) arises as the main diagonal of an explicit rational function in five variables. Using a toric compactification argument (Batyrev 1994), we show the underlying variety is a smooth Calabi–Yau 4-fold. By two independent exact-arithmetic methods — a Q-nullspace solver and Zeilberger creative telescoping (WZ certificate) — we extract the minimal holonomic recurrence of order 5 and degree 9, with all 60 integer polynomial coefficients (up to 46 significant digits) stated explicitly. We verify Lian–Yau mirror-map integrality up to degree d=16. The sequence values, base-case recurrence identities, and a formal uniqueness theorem are certified by the Lean 4 kernel (sorry-free, axiom-free). We present computational evidence for three supercongruence families: a Lucas congruence S(mp+r) ≡ S(m)S(r) (mod p), an Apéry-style congruence S(p-1) ≡ 1 (mod p^3), and the striking cubic congruence S(p) ≡ 3 (mod p^3), verified for all primes p ≤ 29. All computational artifacts are publicly available at https://github.com/xaviercallens/Mirror-Map-Sieve (v1.0.0).