[step:Use initial degenerations to lift every tropical circuit solution]Let $I_L \subset K[x_1^{\pm1},\dots,x_n^{\pm1}]$ be the Laurent ideal of functions vanishing on $L \cap (K^\times)^n$. It is generated by the linear forms coming from linear relations among the columns of $A$. Fix $w \in \mathbb{R}^n$. Choose a valued-field extension $E/K$ whose value group contains $w_1,\dots,w_n$, write $\nu_E:E\to\mathbb R\cup\{\infty\}$ for the extended valuation, let $\mathcal O_E$ be its valuation ring, let $\mathfrak m_E$ be its maximal ideal, and let $k_E:=\mathcal O_E/\mathfrak m_E$ be its residue field. Choose elements $t_i\in E^\times$ with $\nu_E(t_i)=w_i$.
For a Laurent polynomial $f=\sum_u c_u x^u\in E[x_1^{\pm1},\dots,x_n^{\pm1}]$, define
\begin{align*}
m_w(f):=\min_u(\nu_E(c_u)+u\cdot w).
\end{align*}
Choose $\alpha\in E^\times$ with $\nu_E(\alpha)=-m_w(f)$. The residue initial form $\operatorname{in}_w(f)\in k_E[x_1^{\pm1},\dots,x_n^{\pm1}]$, well-defined up to multiplication by a nonzero scalar in $k_E$, is the reduction modulo $\mathfrak m_E$ of the sum of the terms $\alpha c_u x^u$ for which $\nu_E(c_u)+u\cdot w=m_w(f)$. Define the residue-field Laurent initial ideal $\operatorname{in}_w(I_L)\subset k_E[x_1^{\pm1},\dots,x_n^{\pm1}]$ to be the ideal generated by the residue initial forms of all nonzero elements of $I_L\otimes_K E$. This is the initial ideal used below.
Assume $w \in \mathcal{L}(p)$. The initial matroid $M_w$ of the valuated matroid $p$ is the ordinary matroid on $[n]$ whose bases are the $r$-element subsets $B$ minimizing
\begin{align*}
p(B)+\sum_{i \in B} w_i.
\end{align*}
Let $D_w\in E^{n\times n}$ be the diagonal matrix with diagonal entries $t_1,\dots,t_n$. The row space $L_w\subset E^n$ of $AD_w$ is a linear subspace over $E$. We use the following initial-matroid representation fact: if a rank-$r$ matrix over a valued field has maximal-minor valuations $q(B)$ and the relevant weights lie in the value group, then after multiplying columns by elements of the prescribed valuations and applying row operations over the valuation ring, one obtains a full-rank row-equivalent matrix over the valuation ring whose reduction modulo the maximal ideal represents the ordinary matroid with bases exactly the $B$ minimizing $q(B)$. Its hypotheses are satisfied here because the value group of $E$ contains $w_1,\dots,w_n$, the matrix $AD_w$ has rank $r$, and row operations by invertible matrices preserve the represented row space. Applying the fact with
\begin{align*}
q(B)=p(B)+\sum_{i\in B}w_i
\end{align*}
shows that the residue-field initial degeneration represents $M_w$. More explicitly, the rows of the reduced matrix over $k_E$ cut out the same linear subspace of the residue torus as the residue initial ideal $\operatorname{in}_w(I_L)$: column scaling by $D_w$ accounts for the weights $w_i$, row operations over $\mathcal O_E$ do not change the generated linear ideal after reduction, and reducing the minimal-valuation terms of each linear relation is exactly the residue initial-form construction above.
Let $\mathcal{C}(p)$ denote the set of valuated circuits of $p$. Define the minimum-support map
\begin{align*}
C_w:\mathcal{C}(p) \to \mathcal{P}([n])
\end{align*}
by
\begin{align*}
C_w(c):=\{i\in[n]: c_i+w_i=\min_{j\in[n]}(c_j+w_j)\}.
\end{align*}
We use the circuit description of initial matroids: the circuits of $M_w$ are exactly the inclusion-minimal nonempty members of the family $\{C_w(c): c \in \mathcal{C}(p)\}$. This applies because $M_w$ is the initial matroid of the valuated matroid $p$ at the weight $w$. Since $w\in\mathcal L(p)$, every set $C_w(c)$ has cardinality at least two. Therefore no inclusion-minimal nonempty member of this family has cardinality one, so $M_w$ has no loop.
We now translate this loop-free condition into the Laurent initial ideal. Let $\overline{k_E}$ be an [algebraic closure](/page/Algebraic%20Closure) of $k_E$. A coordinate $x_i$ is forced to vanish on the residue-field initial linear space exactly when $i$ is a loop of the represented matroid, because $i$ is a loop precisely when every vector in the represented row space has $i$th coordinate equal to $0$. Since $M_w$ has no loop, each coordinate hyperplane cuts the initial linear space in a proper linear subspace after base change to $\overline{k_E}$. The field $\overline{k_E}$ is infinite, so a finite union of proper linear subspaces cannot equal the whole initial linear space. Therefore the base-changed initial linear space contains a point with all coordinates nonzero, and hence the zero set of the residue-field Laurent initial ideal $\operatorname{in}_w(I_L)$ in the algebraic torus over $\overline{k_E}$ is nonempty.
The Laurent Nullstellensatz criterion is applied over the algebraically closed field $\overline{k_E}$: a Laurent ideal has empty zero set in the algebraic torus over $\overline{k_E}$ exactly when its extension contains the unit monomial $1$, equivalently a Laurent monomial. Since the base-changed zero set is nonempty, the extension of $\operatorname{in}_w(I_L)$ to $\overline{k_E}[x_1^{\pm1},\dots,x_n^{\pm1}]$ contains no Laurent monomial. Laurent monomial containment descends along field extension, so the residue-field initial ideal $\operatorname{in}_w(I_L)$ itself contains no Laurent monomial. This proves the required initial-ideal criterion without reducing an arbitrary relation to a restriction of its coefficients on a circuit.
We apply the fundamental theorem of tropical geometry for linear ideals to the Laurent ideal $I_L\subset K[x_1^{\pm1},\dots,x_n^{\pm1}]$. Its hypotheses are satisfied: by the theorem statement, $\nu:K\to\mathbb R\cup\{\infty\}$ is a non-archimedean real-valued valuation; $I_L$ is a Laurent ideal, so its zero set is considered inside the algebraic torus; and the definition of $\operatorname{Trop}(L)$ permits passing to a valued-field extension when the required residue field or value group is not already present over $K$. The theorem says that a weight $w$ whose Laurent initial ideal contains no Laurent monomial is realized as the coordinatewise valuation of a torus point after such an extension. Hence there are a valued-field extension $F/K$ with extended valuation $\tilde\nu$ and a point
\begin{align*}
x \in (L \otimes_K F)\cap(F^\times)^n
\end{align*}
such that
\begin{align*}
(\tilde{\nu}(x_1),\dots,\tilde{\nu}(x_n))=w.
\end{align*}
Thus $w \in \operatorname{Trop}(L)$, and so
\begin{align*}
\mathcal{L}(p) \subseteq \operatorname{Trop}(L).
\end{align*}[/step]