Four-point condition for tree distances: is there a detropicalization proof? 
Theorem 1. Let $G$ be a tree.
  Let $x$, $y$, $z$ and $w$ be four vertices of $G$.
  For any two vertices $s$ and $t$ of $G$, let $d \left(s, t\right)$ denote the minimum length of a path from $s$ to $t$.
Then, the two largest ones among the three numbers $d \left(x, y\right) + d \left(z, w\right)$, $d \left(x, z\right) + d \left(y, w\right)$ and $d \left(x, w\right) + d \left(y, z\right)$ are equal.

This is a known fact, sometimes called the "four-point condition" (or at least it is similar to the latter; IIRC the latter is about leaves in phylogenetic trees, where $d$ is no longer the minimum length of a path but the minimum cost in some metric, and I'm not fully sure if there are any clear-cut implications between these results).
I am wondering if there is a proof of Theorem 1 along the following lines:


*

*For any two vertices $s$ and $t$ of $G$, define some univariate polynomial $Q_{s, t} \in K\left[X\right]$ (for some field $K$, possibly $\mathbb{F}_2$) having the property that $Q_{s, t}$ is monic with leading term $X^{d\left(s, t\right)}$ (or $X^{d\left(s, t\right) + c}$ for some constant $c$).

*Prove the identity $Q_{x, y} Q_{z, w} \pm Q_{x, z} Q_{y, w} \pm Q_{x, w} Q_{y, z} = 0$ for some choice of $\pm$ signs.

*Conclude that the largest one among the three numbers $d \left(x, y\right) + d \left(z, w\right)$, $d \left(x, z\right) + d \left(y, w\right)$ and $d \left(x, w\right) + d \left(y, z\right)$ must be equal to another of these three numbers, since otherwise the leading term in the preceding identity could not cancel. Therefore, Theorem 1.
This kind of proof seems to be foreshadowed by the well-known tinfoil (not sure whether it has ever been made rigorous) that "the space of phyologenetic trees is the tropical Grassmannian" and, in particular, Theorem 1 is a sort of "tropical version" of the Ptolemy theorem $XY \cdot ZW \pm XZ \cdot YW \pm XW \cdot YZ = 0$ for four points $X, Y, Z, W$ lying on a circle (or line). Of course, the latter theorem itself is merely a shadow of more general results about Grassmannians (the Plücker relations for $\operatorname{Gr}\left(4,2\right)$).
I also have my personal interest in such a proof: I posed Theorem 1 on a graph theory midterm (specifically, exercise 6 on midterm #2 in Spring 2017 Math 5707 at the University of Minnesota; you can now find three different solutions on the course website), and discovered that the proofs I knew were less slick than I had hoped for...
 A: A proof literally following the strategy I suggested does not exist. In fact,
the following holds:

Proposition 2. Let $T$ be a tree with at least one edge. Let
  $c\in\mathbb{N}$. Let $K$ be a field. Let $Q_{s,t}\in K\left[  X\right]  $ be
  a nonzero polynomial for every pair of two vertices $s$ and $t$. Assume that
  \begin{equation}
\text{each polynomial }Q_{s,t}\text{ has degree }d\left(  s,t\right)
+c.
\tag{1}
\label{eq.prop.1.ass1}
\end{equation}
  Assume further that every four vertices $x,y,z,w$ of $T$ satisfy the equality
  \begin{equation}
Q_{x,y}Q_{z,w}\pm Q_{x,z}Q_{y,w}\pm Q_{x,w}Q_{y,z}=0
\tag{2}
\label{eq.prop.1.ass2}
\end{equation}
  for some choice of $\pm$ signs. Then, we have a contradiction.

Proof of Proposition 2. Consider any edge $xz$ of $T$. Thus, $d\left(
x,z\right)  =1$. Apply \eqref{eq.prop.1.ass2} to $y=x$ and $w=z$. This yields
\begin{equation}
Q_{x,x}Q_{z,z}\pm Q_{x,z}Q_{x,z}\pm Q_{x,z}Q_{x,z}=0.
\end{equation}
Hence, $Q_{x,x}Q_{z,z}=\pm Q_{x,z}Q_{x,z}\pm Q_{x,z}Q_{x,z}$ is a scalar
multiple of $Q_{x,z}Q_{x,z}$. Since the scalar is nonzero (because
$Q_{x,x}Q_{z,z}$ is nonzero (since $Q_{x,x}$ and $Q_{z,z}$ is nonzero), we
thus conclude that $\deg\left(  Q_{x,x}Q_{z,z}\right)  =\deg\left(
Q_{x,z}Q_{x,z}\right)  $. In other words, $\deg\left(  Q_{x,x}\right)
+\deg\left(  Q_{z,z}\right)  =\deg\left(  Q_{x,z}\right)  +\deg\left(
Q_{x,z}\right)  =2\deg\left(  Q_{x,z}\right)  $. Using \eqref{eq.prop.1.ass1},
we can rewrite this as $\left(  d\left(  x,x\right)  +c\right)  +\left(
d\left(  z,z\right)  +c\right)  =2\left(  d\left(  x,z\right)  +c\right)  $.
This simplifies to $d\left(  x,x\right)  +d\left(  z,z\right)  =2d\left(
x,z\right)  $. Hence, $2d\left(  x,z\right)  =\underbrace{d\left(  x,x\right)
}_{=0}+\underbrace{d\left(  z,z\right)  }_{=0}=0$, so that $d\left(
x,z\right)  =0$. This contradicts $d\left(  x,z\right)  =1$. This proves
Proposition 2.
I have not given up the concept that there might be an algebraic or geometric
proof of Theorem 1 using some Ptolemy-like condition; but the above makes it
clear that something subtler than polynomials would be needed here.
