A sink equilibrium without local sources whose content is not an attractor

Biggar and Papadimitriou showed that a local source in a sink equilibrium prevents the content of the sink from being an attractor of the replicator dynamic and asked whether the converse holds: must every unstable sink equilibrium contain a local source? We answer this question in the negative. We give a two-player game with rational payoffs and five strategies per player in which the sink equilibrium consisting of all pure profiles but one has no local source in any subgame, while its content is not Lyapunov stable and hence not a uniform attractor. The local-source candidates are excluded by a sign certificate for the stationary profiles of a four-by-four block. The instability comes from an orbit on an invariant face that converges in backward time to a heteroclinic six-cycle inside the content. In logarithmic coordinates, the symmetry-reduced return map is, up to a uniformly bounded error, a linear map whose dominant eigenvalue is simple, exceeds one and has a positive eigenvector; an invariant cone then produces the orbit. The deposit includes the paper (PDF and LaTeX source) and a Lean 4 / Mathlib formalization. The formalization includes the orbit construction, the absence of local sources, failure of Lyapunov stability and uniform attraction, and convergence of every interior orbit to the content. The pointwise-attraction formulation in Section 1 of Biggar and Papadimitriou is not settled. See the package README for build instructions and the scope of the formalization. The Lean source package is licensed under Apache 2.0. Licenses: Proof.pdf and Proof.tex are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). The Lean source archive, sink-equilibrium-lean.zip, is licensed under Apache License 2.0.