The 2n−1 arc minimum in Koljančić–Oblak, Problem 1.8 (p. 759)

Koljančić–Oblak's Problem 1.8, Electronic Journal of Linear Algebra 42 (2026), p. 759, has an affirmative answer: the minimum number of arcs in an n-vertex digraph requiring the nonsymmetric strong spectral property is 2n−1 for every n≥1. By their identification with Arav et al.'s Problem 6.2, this also gives the minimum 2n−1 of nonzero entries in a zero–nonzero pattern requiring the similarity-transversality property (STP). We give a self-contained exposition of the centralizer–incidence proof formalized in Lean. More generally, every real matrix with this property and with c weak support components has at least 2n−c nonzero entries. For connected supports, even allowing one such matrix forces 2n−1 arcs. Together with the endpoint-looped double path of Koljančić–Oblak, this also answers both questions in their Problem 2.9 (p. 764). The endpoint construction is prior work.