We study the binomial sum S (n) = Σ₊=₀^n C (n, k) ⁴ · 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³), and the striking cubic congruence S (p) ≡ 3 (mod p³), verified for all primes p ≤ 29. All computational artifacts are publicly available at https: //github. com/xaviercallens/Mirror-Map-Sieve (v1. 0. 0).
Xavier Callens (Thu,) studied this question.