\section{Proof of the polytope criterion}\label{sec:conclusion}
\begin{proof}[Proof of Theorem~\ref{thm:main}]
Full Fock--Goncharov implies Laurent finiteness of all theta functions. Proposition~\ref{prop:rational} then constructs a rational positive polytope with the required interior property.

Conversely, a polytope as in condition (2) gives Laurent finiteness by Proposition~\ref{prop:finite}. Replace it by the rational polytope of Proposition~\ref{prop:rational}. Lemmas~\ref{lem:compactification} and \ref{lem:poisson} give a finitely generated normal theta algebra $C$ and its regular symplectic form. If a prime divisor were omitted by the initial and adjacent seed tori, Lemma~\ref{lem:valuation} would classify its valuation. Section~\ref{sec:star} would then give a proper theta series in the cylindrical diagram $\D_b$, with no correction parallel to $b$, whose specialization at $H=c$ vanishes. Proposition~\ref{prop:proper} contradicts this. Thus these seed tori cover every codimension-one point of $\Spec C$.

Every upper-cluster function is regular on these tori and therefore belongs to every height-one local ring of $C$. A normal Noetherian domain is the intersection of these local rings inside its fraction field, so $\Up(\Aprin)\subseteq C$. The reverse inclusion follows from universal Laurent finiteness. Principal theta independence gives the required injectivity, and all labels occur, proving full Fock--Goncharov over an algebraically closed field.

For a general field $\kk$ of characteristic zero, extend scalars to an algebraic closure. Any given $f\in\Up_\kk$ remains regular on every seed torus and hence has a finite expression $f=\sum_{i=1}^s c_i\tht_{m_i}$ there. Comparison of initial Laurent coefficients gives a linear system over $\kk$. Independence of the theta functions gives an invertible $s\times s$ coefficient minor, forcing all $c_i\in\kk$. This descends the spanning assertion element by element.

If there are no mutable indices, all functions are characters and an ordinary box proves the statement. When principal coefficients are attached only to mutable indices, the extra coefficient variables in the complete convention are independent Laurent units. All seed tori and theta functions split by that torus factor. Finite Laurent expansion in these extra variables identifies the upper algebras coefficientwise. Positive polytopes transfer by product with a box and by the zero-coordinate section in the reverse direction. Thus the two principal coefficient conventions give the same criterion.
\end{proof}

\begin{thebibliography}{99}
\bibitem{FZ}
S. Fomin and A. Zelevinsky,
\emph{Cluster algebras I: Foundations},
Journal of the American Mathematical Society \textbf{15} (2002), 497--529.
\href{https://arxiv.org/abs/math/0104151}{arXiv:math/0104151}.

\bibitem{FG06}
V. Fock and A. Goncharov,
\emph{Moduli spaces of local systems and higher Teichm\"uller theory},
Publications Math\'ematiques de l'IH\'ES \textbf{103} (2006), 1--211.
\href{https://arxiv.org/abs/math/0311149v4}{arXiv:math/0311149v4}.

\bibitem{BCMN}
L. Bossinger, M.-W. Cheung, T. Magee, and A. N\'ajera Ch\'avez,
\emph{Newton--Okounkov bodies and minimal models for cluster varieties},
Advances in Mathematics \textbf{447} (2024), 109680.
\href{https://arxiv.org/abs/2305.04903v2}{arXiv:2305.04903v2}.

\bibitem{CMN}
M.-W. Cheung, T. Magee, and A. N\'ajera Ch\'avez,
\emph{Compactifications of cluster varieties and convexity},
International Mathematics Research Notices \textbf{2022} (2022), no.~14, 10858--10911.
\href{https://arxiv.org/abs/1912.13052v2}{arXiv:1912.13052v2}.

\bibitem{CMMM}
M.-W. Cheung, T. Magee, T. Mandel, and G. Muller,
\emph{Valuative independence and cluster theta reciprocity},
\href{https://arxiv.org/abs/2505.09585v2}{arXiv:2505.09585v2} (2026).

\bibitem{FG}
V. V. Fock and A. B. Goncharov,
\emph{Cluster ensembles, quantization and the dilogarithm},
Annales Scientifiques de l'\'Ecole Normale Sup\'erieure (4) \textbf{42} (2009), 865--930.
\href{https://arxiv.org/abs/math/0311245v7}{arXiv:math/0311245v7}.

\bibitem{GHK}
M. Gross, P. Hacking, and S. Keel,
\emph{Birational geometry of cluster algebras},
Algebraic Geometry \textbf{2} (2015), 137--175.
\href{https://doi.org/10.14231/AG-2015-007}{doi:10.14231/AG-2015-007}.

\bibitem{GHKK}
M. Gross, P. Hacking, S. Keel, and M. Kontsevich,
\emph{Canonical bases for cluster algebras},
Journal of the American Mathematical Society \textbf{31} (2018), 497--608.
\href{https://arxiv.org/abs/1411.1394v2}{arXiv:1411.1394v2}.
Theorem and proposition numbers in the text refer to this arXiv version unless the published numbering is specified.
\bibitem{RethlasOSV}
OSVerify contributors,
\emph{Rethlas-OSV}, software repository (2026).
\url{https://github.com/OSVerify/Rethlas-OSV}.

\bibitem{NieEtAl}
F. Nie, H. Ye, S. Liu, Z. Wang, S. Ermon, and J. Zou,
\emph{One-Sided Verification Under Limited Expert Review},
\href{https://arxiv.org/abs/2610.18089v2}{arXiv:2610.18089v2} (2026).
\end{thebibliography}

\bigskip
\begingroup\small
\noindent\textsc{Zhili College, Tsinghua University, Beijing 100084, China}\par
\noindent\textit{Email address:}\enspace
\mbox{\href{mailto:tangqy24@mails.tsinghua.edu.cn}{\texttt{tangqy24@mails.tsinghua.edu.cn}}}\par
\endgroup