Reaction-minimal cusps in planar bimolecular mass-action networks: an exhaustive certified classification

A cusp of equilibria is the simplest generic mechanism by which a two-parameter family of vector fields passes between one and three nearby equilibria, and it organizes bistability in chemical reaction networks. We classify the two-species, five-reaction, rank-two bimolecular mass-action networks that admit a positive nondegenerate cusp transversely unfolded by two independent rate constants. Up to reaction permutation, positive rescaling of stoichiometric columns with reactants fixed, and exchange of the two species, there are exactly 52 such networks, and every one of them uses five distinct reactant complexes. Combined with the four-reaction exclusion of Banaji, Boros and Hofbauer, five reactions is the minimum reaction count for a rate-transverse cusp in planar bimolecular mass-action kinetics. The proof is exhaustive and certified. Necessary structural conditions reduce the $142{,}506$ literal five-reaction sets to $60{,}036$ eligible ones, and a reactant-labelled primitive-ray key collapses these to $9{,}999$ mechanism classes. Every class is decided by an exact rational certificate: $9{,}063$ determinant obstructions, $744$ quadratic-degeneracy obstructions, $140$ cubic-degeneracy obstructions and $52$ positive templates. The algebraic classification, including source-faithful coverage of every eligible literal network, is an unconditional theorem verified in Lean 4 against Mathlib. The passage to ordinary analytic cusps is a Lyapunov–Schmidt reduction of the planar vector field that makes explicit a correction to the parameter-unfolding derivative missing from the formal predicate; the corrected minors of all 52 templates are certified by exact rational-polynomial Bézout identities. Every one of the 52 classes organizes nearby positive stable–saddle–stable triples, and we exhibit a fully rational template whose equilibrium equation reduces exactly to $\mu+\nu z-z^{3}$. The paper separates the Lean-verified core from the conventional arguments and exact computer-algebra checks, records the native-evaluation trust boundary, and lists all 52 representatives.