[proofplan]
Choose a full-rank matrix $A$ whose row span is $L$ and encode its maximal minors by their valuations. The ordinary Plucker relations among maximal minors tropicalize to the valuated Plucker relations, giving the valuated matroid. The same minors give explicit linear circuit relations among the columns of $A$; valuation vectors of points of $L$ must satisfy the corresponding tropical circuit equations. Conversely, if a vector satisfies all these tropical circuit equations, then the initial linear ideal has no monomial, so the fundamental theorem of tropical geometry for linear ideals gives a valued-field lift after passing to an extension; taking closure gives the stated equality.
[/proofplan]
[step:Show that the Plucker valuations satisfy the valuated Plucker relations]
Let $\nu:K\to \mathbb R\cup\{\infty\}$ denote the valuation on $K$, and let $[n] := \{1,\dots,n\}$. Choose an $r\times n$ matrix $A$ over $K$ whose row span is $L$. For an $r$-element subset $B \subset [n]$, write $A_B \in K^{r \times r}$ for the submatrix of $A$ with columns indexed by $B$, and write $\Delta_B(A) := \det A_B$. Since $A$ has rank $r$, at least one $\Delta_B(A)$ is nonzero, so $p$ is not identically $\infty$.
We verify the valuated Plucker relations. Let $S \subset [n]$ have cardinality $r-1$, and let $T \subset [n]$ have cardinality $r+1$. We use the Grassmann-Plucker determinant identity for maximal minors of a rank-$r$ matrix. Its hypotheses are satisfied because $A$ has rank $r$ and the displayed minors are the $r\times r$ maximal minors of $A$. We use the standard Grassmann-Plucker convention: if a displayed subset has repeated indices or does not have cardinality $r$, its minor is interpreted as $0$. With this convention, the relation says
\begin{align*}
\sum_{j \in T \setminus S} \epsilon_j \Delta_{S \cup \{j\}}(A)\Delta_{T \setminus \{j\}}(A) = 0,
\end{align*}
where each $\epsilon_j \in \{-1,1\}$ is the sign determined by placing the indices in increasing order before taking determinants. Terms with a zero minor have valuation $\infty$ by the definition of $p$. Applying the non-archimedean valuation inequality to the remaining nonzero finite sum, the minimum of the valuations of its nonzero summands must be attained at least twice. Hence the minimum
\begin{align*}
\min_{j \in T \setminus S}\bigl(p(S \cup \{j\}) + p(T \setminus \{j\})\bigr)
\end{align*}
is attained at least twice, with zero-minor terms ignored because their value is $\infty$. These are precisely the valuated Plucker relations, so $p$ is a valuated matroid.
If $A'$ is another rank-$r$ matrix with row span $L$, then $A' = GA$ for some $G \in GL_r(K)$. Therefore
\begin{align*}
\Delta_B(A') = \det(G)\Delta_B(A)
\end{align*}
for every $r$-element subset $B \subset [n]$. Thus $p$ changes by the common additive constant $\nu(\det G)$, which does not change the associated valuated matroid or its tropical linear space.
[/step]
[step:Identify the valuated circuits with the linear circuit equations of $L$]
For an $(r+1)$-element subset $S \subset [n]$, define coefficients $\lambda_{S,i} \in K$ for $i \in S$ by
\begin{align*}
\lambda_{S,i} := (-1)^{\operatorname{pos}_S(i)}\Delta_{S \setminus \{i\}}(A),
\end{align*}
where $\operatorname{pos}_S(i)$ is the position of $i$ in the increasing ordering of $S$. Let $a_i \in K^r$ denote the $i$th column of $A$. The alternating expansion of the determinant of the $r \times (r+1)$ matrix $A_S$ gives the column dependence
\begin{align*}
\sum_{i \in S}\lambda_{S,i} a_i = 0.
\end{align*}
Equivalently, define the linear form $\ell_S: K^n \to K$ by $\ell_S(x)=\sum_{i \in S}\lambda_{S,i}x_i$. For every row vector $x = (x_1,\dots,x_n) \in L$, the linear form $\ell_S$ vanishes on $L$.
The associated Plucker circuit vector is the function $c_S:[n]\to \mathbb R\cup\{\infty\}$ defined by
\begin{align*}
c_S(i) = p(S \setminus \{i\}) \quad \text{for } i \in S,
\end{align*}
and by $c_S(i)=\infty$ for $i\notin S$, with $c_S(i)=\infty$ also when the corresponding coefficient $\lambda_{S,i}$ vanishes. If the underlying ordinary matroid is not uniform, the finite support of $c_S$ need not be a minimal circuit. The actual ordinary circuits are the minimal nonempty finite supports arising from these Plucker circuit vectors, and the valuated circuits of $p$ are obtained by restricting the corresponding valuation data to those minimal supports. These are precisely the valuation data of the minimal linear circuit equations cutting out $L$ in the torus.
[/step]
[step:Show that every lifted point satisfies every tropical circuit equation]
Let $F/K$ be a valued-[field extension](/page/Field%20Extension) with valuation $\tilde{\nu}: F \to \mathbb{R}\cup\{\infty\}$ extending $\nu$, and let $x=(x_1,\dots,x_n) \in (L \otimes_K F)\cap(F^\times)^n$. Define
\begin{align*}
w := (\tilde{\nu}(x_1),\dots,\tilde{\nu}(x_n)) \in \mathbb{R}^n.
\end{align*}
For every circuit relation $\ell_S(x)=0$ as above, we have
\begin{align*}
\sum_{i \in S}\lambda_{S,i} x_i = 0.
\end{align*}
The valuation of the $i$th summand is
\begin{align*}
\tilde{\nu}(\lambda_{S,i} x_i) = \nu(\lambda_{S,i}) + \tilde{\nu}(x_i) = p(S \setminus \{i\}) + w_i.
\end{align*}
Since a finite sum in a valued field can vanish only if the minimum valuation among its nonzero summands is attained at least twice, the minimum
\begin{align*}
\min_{i \in S}\bigl(p(S \setminus \{i\}) + w_i\bigr)
\end{align*}
is attained at least twice. Therefore $w \in \mathcal{L}(p)$. Taking all valued-field extensions and then Euclidean closure gives
\begin{align*}
\operatorname{Trop}(L) \subseteq \mathcal{L}(p).
\end{align*}
[guided]
The point of this step is that an ordinary linear dependence becomes a tropical balancing condition after applying the valuation. Fix a valued-field extension $F/K$ and a point
\begin{align*}
x=(x_1,\dots,x_n) \in (L \otimes_K F)\cap(F^\times)^n.
\end{align*}
Because every coordinate of $x$ is nonzero, each number $w_i := \tilde{\nu}(x_i)$ is finite, and hence
\begin{align*}
w=(w_1,\dots,w_n) \in \mathbb{R}^n.
\end{align*}
Now take an $(r+1)$-element subset $S \subset [n]$. For each $i\in S$, the coefficient
\begin{align*}
\lambda_{S,i} := (-1)^{\operatorname{pos}_S(i)}\Delta_{S\setminus\{i\}}(A)
\end{align*}
was defined using the position $\operatorname{pos}_S(i)$ of $i$ in the increasing ordering of $S$. The alternating determinant expansion gives the column relation
\begin{align*}
\sum_{i\in S}\lambda_{S,i} a_i=0.
\end{align*}
Since every row vector $x\in L\otimes_K F$ is obtained from the row span of $A$ after extension of scalars, multiplying this column relation by the corresponding row coefficient vector gives
\begin{align*}
\sum_{i \in S}\lambda_{S,i} x_i = 0.
\end{align*}
Each coefficient $\lambda_{S,i}$ is a signed Plucker coordinate, so
\begin{align*}
\tilde{\nu}(\lambda_{S,i} x_i)=\nu(\lambda_{S,i})+\tilde{\nu}(x_i)=p(S\setminus\{i\})+w_i.
\end{align*}
If the minimum of these quantities were achieved at a unique index $i_0$, then the term $\lambda_{S,i_0} x_{i_0}$ would have strictly smaller valuation than every other term. The non-archimedean inequality would then force the whole sum to have that same smallest valuation, so the sum could not be zero. Since the sum is zero, the minimum must be attained at least twice:
\begin{align*}
\min_{i \in S}\bigl(p(S\setminus\{i\})+w_i\bigr) \text{ is attained at least twice.}
\end{align*}
This is exactly the tropical circuit equation defining membership in $\mathcal{L}(p)$. Since the argument applies to every circuit relation, every valuation vector of a lifted torus point of $L$ lies in $\mathcal{L}(p)$.
[/guided]
[/step]
[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*}
[guided]
The delicate point is not an individual linear relation; an arbitrary dependence among the columns of $A$ can involve coefficients outside a chosen circuit, so its coefficients cannot be restricted to a smaller circuit without changing the relation. Instead we use the initial matroid, which records all cancellations at the weight $w$ at once.
Define the initial matroid $M_w$ of $p$ to have as bases the $r$-subsets $B \subset [n]$ minimizing
\begin{align*}
p(B)+\sum_{i \in B}w_i.
\end{align*}
To see what this matroid represents, pass to a valued-field extension $E/K$ whose value group contains all coordinates $w_i$. Let $\nu_E:E\to\mathbb R\cup\{\infty\}$ be 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$, and let $D_w\in E^{n\times n}$ be the diagonal matrix with diagonal entries $t_1,\dots,t_n$. Scaling the $i$th coordinate by $t_i$ changes the valuation of the minor indexed by $B$ by exactly $\sum_{i\in B}w_i$. We use the following representation fact: after column scaling by elements with the prescribed valuations and row operations over the valuation ring, reduction modulo the maximal ideal represents the matroid whose bases are exactly the maximal minors of smallest valuation. The fact applies because $AD_w$ has rank $r$ and the required weights lie in the value group of $E$. Therefore the residue row space has nonzero maximal minors exactly for those $B$ minimizing
\begin{align*}
p(B)+\sum_{i\in B}w_i.
\end{align*}
Thus this residue-field initial degeneration represents $M_w$.
Now compare circuits. Let $\mathcal{C}(p)$ denote the set of valuated circuits of $p$, and 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*}
The circuit description of initial matroids says that the circuits of $M_w$ are the inclusion-minimal nonempty members of the family of sets $C_w(c)$ as $c$ ranges over all valuated circuits of $p$. They are not arbitrary nonempty subsets of the sets $C_w(c)$, and they need not be the whole sets $C_w(c)$ themselves. Because $w\in\mathcal L(p)$, every $C_w(c)$ has at least two elements. Therefore no inclusion-minimal nonempty member of this family can have one element, and so $M_w$ has no loop.
Now interpret this in terms of the Laurent initial ideal. The residue-field initial ideal $\operatorname{in}_w(I_L)\subset k_E[x_1^{\pm1},\dots,x_n^{\pm1}]$ is defined by taking each nonzero Laurent polynomial $f=\sum_u c_ux^u$ in $I_L\otimes_K E$, selecting the terms minimizing $\nu_E(c_u)+u\cdot w$, rescaling those minimal terms to valuation zero, and reducing their coefficients modulo $\mathfrak m_E$. For the linear generators coming from relations among the columns of $A$, this is the same linear ideal cut out by the row space obtained from $AD_w$ after valuation-ring row reduction and residue reduction. Thus $\operatorname{in}_w(I_L)$ cuts out the residue-field initial linear degeneration representing $M_w$.
Let $\overline{k_E}$ be an algebraic closure of $k_E$. After base change to $\overline{k_E}$, the initial degeneration is a linear subspace. A coordinate $x_i$ is identically zero on that linear subspace exactly when $i$ is a loop of the represented matroid. Since $M_w$ has no loop, each coordinate hyperplane intersects the base-changed initial linear space in a proper linear subspace. The field $\overline{k_E}$ is infinite, so finitely many proper linear subspaces cannot cover the whole initial linear space. Hence there is a point of the base-changed initial linear space with all coordinates nonzero, meaning that the base-changed initial degeneration has a point in the algebraic torus.
The Laurent Nullstellensatz criterion must be applied over an algebraically closed field. Over $\overline{k_E}$, it says that a Laurent ideal has empty torus zero set exactly when it contains the unit monomial $1$, equivalently a Laurent monomial. Since the base-changed torus zero set of $\operatorname{in}_w(I_L)$ is nonempty, its extension to $\overline{k_E}[x_1^{\pm1},\dots,x_n^{\pm1}]$ contains no Laurent monomial. Monomial containment descends under field extension, so the residue-field initial ideal $\operatorname{in}_w(I_L)$ contains no Laurent monomial.
We now apply the fundamental theorem of tropical geometry for linear ideals. Its hypotheses are the ones present here: $\nu:K\to\mathbb R\cup\{\infty\}$ is non-archimedean and real-valued, $I_L$ is a Laurent ideal so the ambient space is the torus, and the definition of $\operatorname{Trop}(L)$ allows valued-field extensions when the needed value group or residue field is not already available over $K$. Since $\operatorname{in}_w(I_L)$ contains no Laurent monomial, the theorem gives a valued-field extension $F/K$ and a point
\begin{align*}
x \in (L \otimes_K F)\cap(F^\times)^n
\end{align*}
with
\begin{align*}
(\tilde{\nu}(x_1),\dots,\tilde{\nu}(x_n))=w.
\end{align*}
Thus $w \in \operatorname{Trop}(L)$.
[/guided]
[/step]
[step:Combine the two inclusions]
The inclusion $\operatorname{Trop}(L)\subseteq \mathcal{L}(p)$ follows from applying the valuation inequality to every circuit equation of $L$. The reverse inclusion $\mathcal{L}(p)\subseteq \operatorname{Trop}(L)$ follows from the Laurent initial-ideal criterion and the fundamental theorem of tropical geometry for linear ideals, allowing valued-field extensions when a lift is required. Therefore
\begin{align*}
\operatorname{Trop}(L)=\mathcal{L}(p).
\end{align*}
Together with the valuated Plucker verification, this proves that every realizable tropical linear space is the tropical linear space of the valuated matroid given by the Plucker valuations of $L$.
[/step]