A base-r simplex that is not Ehrhart positive

For integers $r\ge2$ and $d\ge1$, Solus's base-$r$ $d$-simplex is the convex hull of the standard basis vectors of $\mathbb{R}^d$ and the point $-(r-1)(1,r,\dots,r^{d-1})$. Solus introduced these simplices through numeral systems, proved that their $h^*$-polynomials are real-rooted, and observed that computations suggest they are also Ehrhart positive. Fu Liu recorded this as Solus's conjecture that every base-$r$ $d$-simplex is Ehrhart positive, and Liu and Solus restated it for all $r\ge2$ and $d\ge1$. We show that the conjecture fails: the base-$14$ $5$-simplex has Ehrhart polynomial \[ 1-\tfrac{268}{15}t+\tfrac{3955}{12}t^2+\tfrac{5833}{2}t^3+\tfrac{10343}{12}t^4+\tfrac{67228}{15}t^5, \] whose linear coefficient is negative. The proof is an explicit bijection between the lattice points of each dilate and pairs consisting of a residue modulo $14^5$ and a vector of nonnegative integers, which reduces the count to the distribution of one integer-valued height function over the $537{,}824$ residues. Lean checks the whole statement from the definition of the convex hull, including the finite height distribution, by kernel evaluation. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.