math.AG — Algebraic Geometry
Strict negativity and non-vanishing of Chen--Larson hypergeometric coefficients
Chen and Larson study tautological classes on the strata of holomorphic abelian differentials, where they predict a vanishing result. Using known tautological relations on the moduli space of curves, they reduce this prediction to the non-vanishing of certain coefficients of a quotient of hypergeometric generating series, treating the residue classes and through two separate series; they verify the non-vanishing by computer for small genus. We prove it in general: in both cases the relevant coefficient is non-vanishing for every genus and every stratum, and in the first case it has, more strongly, a uniform strict sign. Along the way we correct an error in the Chen--Larson derivation of the series, where a constant of the underlying relation of Ionel had inadvertently been changed. The paper falls into two parts. Part~I gives the mathematical proofs; Part~II documents the Lean~4 and Mathlib formalization --- whose only non-standard trust assumption is the compiler invoked by \code{native\_decide} for the large finite computations --- together with the long-horizon, multi-model generative-AI process that produced the proofs, exposed false intermediate routes, and uncovered the error in the printed Proposition~5.2 relation noted above.