Perfect powers in the OEIS sequence A113258

We study the factorial-power sum a(n) = sum_{i=1}^n (i!)^((n-i+1)!), recorded as OEIS A113258. Its fourth term is 125 = 5³. We prove that no term with n > 4 is a perfect power with base and exponent greater than one. The proof combines elementary congruences and power-gap estimates, a specialized interpolation-determinant proof of an explicit lower bound for a linear form in two logarithms, and finite arithmetic certificates. The result is formalized in Lean 4, including the correctness of the certificate checkers and coverage of the remaining candidates. The finite checks use native_decide and therefore additionally trust the Lean compiler and runtime. The manuscript documents these dependencies and provides reproduction instructions. The accompanying Lean source and certificates are archived as version 1.0.0 at https://doi.org/10.5281/zenodo.22812208.