PROVED (LEAN). The limit exists and satisfies $1.4457\le\alpha\le\frac{1+\sqrt5}2\approx1.618$ (the site's interval), so $\alpha<2$. Existence: Proposition 2 of Bradač's note (J. Graph Theory 108 (2025), no. 4, 817--818, published online 8 December 2024, refereed; cited from the arXiv v2), by Fekete's lemma for the marked-pair separator count $g(n)$, transferred to $c(n)$ by the paper's displayed sandwich $g(n-2)\le c(n)\le\binom n2g(n-2)$, whose right inequality is immediate and whose left inequality the paper asserts as "Clearly" without argument (recorded as a proof-coverage gap, not a dispute). The bound: every minimal cut is a minimal separator, so $c(n)\le\mathsf{sep}(n)$, and $\mathsf{sep}(n)=O(1.6181^n)$ by Fomin and Villanger's Theorem 1 (Combinatorica 2012, refereed; cited from the arXiv v2), whose proof's estimate has the golden ratio as its base (p. 7), reproved as $O(\rho^n\cdot n)$ by Gaspers and Mackenzie's Theorem 1 (J. Graph Theory 2018, refereed); Bradač's Theorem 1 gives $c(n)\le2^{(1+o(1))H(1/3)n}$, $\alpha\le2^{H(1/3)}<1.8899$, directly for minimal cuts; and the first proof of $\alpha<2$ is $\mathsf{sep}(n)=O(1.7087^n)$ of Fomin, Kratsch, Todinca and Villanger (SIAM J. Comput. 2008, refereed), as the journal's abstract states it and as Bradač's note and Gaspers and Mackenzie attest. These three separator bounds are accepted partial claims on the bound half of the question, recorded on the claim pages of Fomin, Kratsch, Todinca and Villanger, Fomin and Villanger and Gaspers and Mackenzie. The lower bound $3^{1/3}\approx1.4422$ is Seymour's construction in Erdős's paper, and $1.4457$ is the lower bound the site and Bradač attribute to Gaspers and Mackenzie's Theorem 2 for minimal separators, as the published J. Graph Theory version states it ($\omega(1.4457^n)$ in its abstract); that version is not held and its proof is unchecked, while the arXiv v2 prints $\omega(1.4521^n)$; the transfer to $\alpha$ is through the same sandwich. The site's curator accepted the resolution with the label PROVED (LEAN) on 31 March 2026, crediting Bradač's note; the external Lean file behind the label declares itself a formalization of Bradač's argument and works with the separator count, not the collection's minimal-cut count (Formalization). Bradač's note is the accepted full claim, recorded on its claim page (Bradač, 2024), which carries the Lean file as a formalization link, and the frontmatter standing is derived from it.