# (In)dependence of the Axioms of $\Lambda$-trees

Raphael Appenzeller  Department of Mathematics, ETH Zurich, Switzerland
<EMAIL_ADDRESS>
###### Abstract.

A $\Lambda$-tree is a $\Lambda$-metric space satisfying three axioms (1), (2)
and (3). We give a characterization of those ordered abelian groups $\Lambda$
for which axioms (1) and (2) imply axiom (3). As a special case, it follows
that for the important class of ordered abelian groups $\Lambda$ that satisfy
$\Lambda=2\Lambda$, (3) follows from (1) and (2). For some ordered abelian
groups $\Lambda$, we show that axiom (2) is independent of the axioms (1) and
(3) and ask whether this holds for all ordered abelian groups. Part of this
work has been formalized in the proof assistant
$\operatorname{\mathsf{Lean}}$.

###### Key words and phrases:

$\Lambda$-trees, ordered abelian groups, Euclidean fields,
$\Lambda$-buildings.

###### 1991 Mathematics Subject Classification:

51M30, 06F20, 05C05.

##  1\. Introduction

Let $(\Lambda,+)$ be an ordered abelian group. A set $X$ together with a
$\Lambda$-valued function $d\colon X\times X\to\Lambda$ that is positive
definite, symmetric and satisfies the triangle inequality is called a
_$\Lambda$ -metric space_. A $\Lambda$-metric space $(X,d)$ is a _$\Lambda$
-tree_ if it satisfies the following three axioms (definitions in Section 2):

  * (1)

$(X,d)$ is geodesic: any two points can be joined by a segment.

  * (2)

If two segments $s,s^{\prime}\subseteq X$ intersect in a single point $s\cap
s^{\prime}=\\{p\\}$, which is an endpoint of $s$ and $s^{\prime}$, then their
union $s\cup s^{\prime}$ is a segment.

  * (3)

If two segments $s,s^{\prime}\subseteq X$ have an endpoint in common, then
their intersection $s\cap s^{\prime}$ is a segment.

It is known that for $\Lambda=\mathbb{Z}$ and $\Lambda=\mathbb{R}$, axiom (3)
follows from (1) and (2), see [MS84, Lemma I.1.1] or [Chi01, Lemma I.2.3]. As
$\Lambda$-trees generalize trees from graph theory ($\Lambda=\mathbb{Z}$) and
real trees ($\Lambda=\mathbb{R}$) the following question arises. For which
ordered abelian groups $\Lambda$ is the addition of axiom (3) necessary? In
Theorem 1, we give a complete characterization of the groups $\Lambda$, for
which axiom (3) follows from (1) and (2), answering the question.

######  Theorem 1.

Let $\Lambda$ be an ordered abelian group. The following are equivalent:

  * (a)

For every positive $\lambda_{0}\in\Lambda$, the set $\\{t\in\Lambda\colon
0\leq 2t\leq\lambda_{0}\\}$ has a maximum.

  * (b)

Every $\Lambda$-metric space that satisfies axioms (1) and (2) also satisfies
(3).

For $\Lambda=\mathbb{Z}$ and $\Lambda=\mathbb{R}$, we recover the statement of
[MS84, Lemma I.1.1], as every bounded subset of $\mathbb{Z}$ and $\mathbb{R}$
has a supremum. Condition (a) can also be satisfied if every element in
$\Lambda$ is divisible by $2$, showing that axiom (3) follows from (1) and (2)
for groups like $\mathbb{Q},\,\mathbb{Z}[\frac{1}{2}]$ or
$\mathbb{R}\times\mathbb{R}$ with the lexicographical ordering. On the other
hand, Theorem 1 also shows that in general, (for example for
$\Lambda=\mathbb{Z}[\frac{1}{3}]$ or $\Lambda=\mathbb{Z}[\sqrt{2}]$), axiom
(3) is independent of (1) and (2).

When $\Lambda$-trees were introduced in [MS84], $X$ was required to be
uniquely geodesic as part of the definition of $\Lambda$-trees. The uniqueness
however already follows from the conditions (1) and (2), see [Chi01, Lemma
I.3.6]. We show in Proposition 1 that uniqueness also follows from the
conditions (1) and (3).

######  Proposition 1.

Let $(X,d)$ be a geodesic $\Lambda$-metric space. If $(X,d)$ satisfies axiom
(3), then $(X,d)$ is uniquely geodesic.

We show further that for many ordered abelian groups $\Lambda$, axiom (2) does
not follow from axioms (1) and (3).

######  Theorem 2.

Let $\Lambda\neq 2\Lambda$ or let $\Lambda$ be the additive group of an
ordered field. Then axiom (2) is independent of the axioms (1) and (3).

Theorem 2, does not cover all the cases: the group
$\Lambda_{2}:=\mathbb{Z}[\frac{1}{2}]$ for instance does not satisfy the
conditions of Theorem 2. It is not even clear whether every uniquely geodesic
$\Lambda_{2}$-metric space is a $\Lambda_{2}$-tree. We would therefore like to
propose the following two questions. In view of Proposition 1, a positive
answer to the first question would imply a positive answer to the second.

######  Question 1.

Let $\Lambda$ be a non-trivial ordered abelian group. Is axiom (2) independent
of the axioms (1) and (3)?

######  Question 2.

Let $\Lambda$ be a non-trivial ordered abelian group. Is there a uniquely
geodesic $\Lambda$-metric space that does not satisfy axiom (2)?

In applications, the algebraic condition $\Lambda=2\Lambda$ is often
satisfied. An important source of ordered abelian groups is as the image of a
valuation $v\colon\mathbb{F}_{>0}\to\Lambda$ of an ordered field $\mathbb{F}$.
If $\mathbb{F}$ is _Euclidean_ , meaning that all positive elements have
square roots in the field, then $\Lambda=2\Lambda$, because $v$ turns
multiplication into addition. In particular, all real closed fields are
Euclidean. For example, Brumfiel [BR88] starts with a non-Archimedean
Euclidean field $\mathbb{F}$ with a valuation
$v\colon\mathbb{F}_{>0}\to{\Lambda\subseteq\mathbb{R}}$ and obtains a
$\Lambda$-metric space $X$ as a quotient of a non-standard hyperbolic plane
over $\mathbb{F}$. By Theorem 1, it suffices to check axioms (1) and (2) when
proving that the obtained $\Lambda$-metric space is a $\Lambda$-tree.

Formaliziation in the proof assistant $\operatorname{\mathsf{Lean}}$. The
$\operatorname{\mathsf{Lean}}$ theorem prover is a proof assistant developped
mainly by Leonardo de Moura at Microsoft Research [dM+15]. There is an
extensive community-built mathematical library mathlib [mC19], which by now
contains a large part of undergraduate mathematics and also some more advanced
projects such as a formalization of perfectoid spaces [BCM10]. We build on the
definition of ordered abelian groups already present in mathlib to formalize
parts of this paper. We first formalize the notions of $\Lambda$-metric spaces
and $\Lambda$-trees. We show some basic properties such as reparametrizations
of segment maps. We give complete formal proofs for Lemma 1, Lemma 2 and the
direction (a) implies (b) of Theorem 1. The
$\operatorname{\mathsf{Lean}}$-files can be found [App23]. We believe that the
formalization of proofs can considerably improve the reliability of new
mathematical results.

Relation to $\Lambda$-buildings. The notion of a $\Lambda$-tree was introduced
in [MS84] to generalize the notion of $\mathbb{R}$-trees which itself is a
generalization of trees (or $\mathbb{Z}$-trees) from graph theory. Analogously
Bennett [Ben90] gave a system of axioms (A1) - (A6) for affine
$\Lambda$-buildings, which generalize affine $\mathbb{R}$-buildings which
themselves generalize the classical affine buildings (or
$\mathbb{Z}$-buildings). Indeed, the rank $1$ affine $\Lambda$-buildings are
exactly the $\Lambda$-trees without leaves. While axiom (3) ensures that the
tree-segments intersect where they should, axiom (A6) has a similar role in
the theory of affine $\Lambda$-buildings. Just like (3) follows from (1) and
(2) in the case $\Lambda=\mathbb{R}$, (A6) follows from the other axioms for
affine $\mathbb{R}$-buildings, see [Par00]. To show that (A6) is independent
of (A1) - (A5), Bennett ([Ben94], Remark 3.3) claims to give an example of a
$\mathbb{Q}$-metric space that satisfies all axioms of a rank $1$ affine
$\mathbb{Q}$-building except for (A6). However, there is a mistake in the
example: not all distances are $\mathbb{Q}$-valued. Indeed, Theorem 1 implies,
that no rank $1$ counterexample for $\Lambda=\mathbb{Q}$ can exist. However,
the example in [Ben94] can be modified by taking
$\Lambda=\mathbb{Z}[\frac{1}{3}]$ instead of $\mathbb{Q}$ to show that axiom
(A6) is independent of the other axioms. The axioms of affine
$\Lambda$-buildings have been studied and simplified in [BSS14], and it would
be interesting to know under which assumptions on $\Lambda$ (A6) follows from
the other axioms, thus simplifying the axioms further and possibly
generalizing Theorem 1.

Structure of the paper. In Section 2 we state the definitions and some
elementary results in the theory of $\Lambda$-trees, such as Proposition 1. In
Section 3 we prove the implication (a) $\implies$ (b) of Theorem 1. In Section
4 we construct counterexamples to show the implication $\neg$(a) $\implies$
$\neg$(b) of Theorem 1 and to show Theorem 2.

The author would like to thank L. De Rosa and X. Flamm for insightful
discussions.

##  2\. Definitions and elementary results

We define the notion of a $\Lambda$-tree following Chiswell’s book [Chi01],
where more details can be found. Let $(\Lambda,+)$ be an ordered abelian
group. A set $X$ together with a $\Lambda$-valued function

$d\colon X\times X\to\Lambda$

that is positive definite, symmetric and satisfies the triangle inequality is
called a _$\Lambda$ -metric space_. A _closed $\Lambda$-interval_ is a set of
the form

$[a,b]:=\\{\lambda\in\Lambda\colon a\leq\lambda\leq b\\}$

for $a\leq b\in\Lambda$. Closed $\Lambda$-intervals with
$d_{\Lambda}(t,t^{\prime})=|t^{\prime}-t|$ for $t,t^{\prime}\in[a,b]$ are
$\Lambda$-metric spaces. Let $X$ be any $\Lambda$-metric space. An isometric
embedding $\varphi\colon[a,b]\to X$ is called a _parametrization_ of its image
$s=\varphi([a,b])\subseteq X$, which is called a _segment_. Note that the set
of _endpoints_ $\\{\varphi(a),\varphi(b)\\}\subseteq X$ is independent of the
parametrization $\varphi$ of the segment $s$. A $\Lambda$-metric space is
_geodesic_ if for any two points $p,q\in X$ there exists a segment that has
$p$ and $q$ as endpoints. If there is only one such segment, then $X$ is
called _uniquely geodesic_ (or _geodesically linear_ in [Chi01]). In a
uniquely geodesic $\Lambda$-metric space, we denote a segment $s$ with
endpoints $x,y\in X$ by $s=[x,y]$.

A $\Lambda$-metric space $(X,d)$ is a _$\Lambda$ -tree_ if it satisfies the
following three axioms, two of which are illustrated in Figure 1.

  * (1)

$(X,d)$ is geodesic.

  * (2)

If two segments $s,s^{\prime}\subseteq X$ intersect in a single point $s\cap
s^{\prime}=\\{p\\}$, which is an endpoint of $s$ and $s^{\prime}$, then their
union $s\cup s^{\prime}$ is a segment.

  * (3)

If two segments $s,s^{\prime}\subseteq X$ have an endpoint in common, then
their intersection $s\cap s^{\prime}$ is a segment.

Figure 1. Illustration of axiom (2) (left) and axiom (3) (right) of
$\Lambda$-trees. In axiom (2) the segments $s,s^{\prime}$ are only allowed to
intersect in one point.

In the presence of either axiom (2) or axiom (3), geodesic $\Lambda$-metric
spaces are uniquely geodesic. For axiom (2), this is Lemma 1 and was shown in
[Chi01, Lemma I.3.6]. For axiom (3), this is Proposition 1 and we give a proof
here.

######  Lemma 1 (Lemma I.3.6 in [Chi01]).

Let $(X,d)$ be a geodesic $\Lambda$-metric space. If $(X,d)$ satisfies axiom
(2), then $(X,d)$ is uniquely geodesic.

######  Proposition 1.

Let $(X,d)$ be a geodesic $\Lambda$-metric space. If $(X,d)$ satisfies axiom
(3), then $(X,d)$ is uniquely geodesic.

###### Proof.

Let us assume that axiom (3) is satisfied and let $s,s^{\prime}$ be two
segments with common endpoints $p$ and $q$. By axiom (3), their intersection
$s\cap s^{\prime}$ is a segment. We note that $p,q\in s\cap s^{\prime}$. Let
$\varphi\colon[0,d(p,q)]\to X$ be a parametriztion of (potentially a
subsegment of) $s\cap s^{\prime}$ with $\varphi(0)=p$ and $\varphi(d(p,q))=q$.
For $r\in s$, we have $d(p,r)\leq d(p,q)$ and hence $\varphi(d(p,r))\in s\cap
s^{\prime}\subseteq s$. Since $r$ is the unique point on $s$ with distance
$d(p,r)$ from $p$, we have $\varphi(d(p,r))=r$ showing $s\subseteq s\cap
s^{\prime}$. Similarly $s^{\prime}\subseteq s\cap s^{\prime}$ and hence
$s=s\cap s^{\prime}=s^{\prime}$. ∎

The idea for the following lemma appears also in Chiswell’s proof of Lemma 1.
We will use this lemma in the proof of Theorem 1.

######  Lemma 2.

Let $(X,d)$ be a uniquely geodesic $\Lambda$-metric space. Let $s=[x,y]$ be a
segment, $z\in s$ and $p\in X$. Then

$[x,z]\cap[z,p]=\\{z\\}\quad\text{ or }\quad[y,z]\cap[z,p]=\\{z\\}.$

Figure 2. The lemma states that the segment $[z,p]$ cannot intersect both
$[x,z]$ and $[y,z]$ outside of $\\{z\\}$. It is also possible that $[z,p]$
intersects $[x,y]$ in only one point $z$, in which case both possibilities in
the lemma are correct.

###### Proof.

For $a:={d(z,p)\in\Lambda}$, let $\varphi\colon[0,a]\to X$ be a
parametrization of $[z,p]$ with $\varphi(0)=z$ and $\varphi(a)=p$. Note that
$z$ is an endpoint of $[z,p]$. Let $x^{\prime}\in[x,z]\cap[z,p]$ and
$y^{\prime}\in[y,z]\cap[z,p]$. We would like to show that $x^{\prime}=z$ or
$y^{\prime}=z$.

There are $t_{x},t_{y}\in[0,a]$, such that $\varphi(t_{x})=x^{\prime}$ and
$\varphi(t_{y})=y^{\prime}$, and thus
$d(x^{\prime},y^{\prime})=|t_{y}-t_{x}|$. Looking at the segment $[x,y]$, we
also know that $z\in[x^{\prime},y^{\prime}]\subseteq s$, since
$[x^{\prime},y^{\prime}]\subseteq[x,y]=[x,z]\cup[z,y]$ is unique. So
$d(x^{\prime},y^{\prime})=d(x^{\prime},z)+d(z,y^{\prime})=t_{x}+t_{y}$. The
equation $|t_{y}-t_{x}|=t_{y}+t_{x}$ can only be resolved if $t_{x}=0$ or
$t_{y}=0$, so $x^{\prime}=z$ or $y^{\prime}=z$. This concludes the proof of
the lemma. ∎

##  3\. Dependence results

Recall that $r\in\Lambda$ is called the _maximum of a subset
$S\subseteq\Lambda$_ if $r\in S$ and for all $s\in S$, $s\leq r$. We now state
the main theorem and prove (a) $\implies$ (b). This proof of this direction is
formalized in $\operatorname{\mathsf{Lean}}$ in [App23]. The converse
direction is proved in Section 4.

######  Theorem 1.

Let $\Lambda$ be an ordered abelian group. The following are equivalent:

  * (a)

For every positive $\lambda_{0}\in\Lambda$, the set $\\{t\in\Lambda\colon
0\leq 2t\leq\lambda_{0}\\}$ has a maximum.

  * (b)

Every $\Lambda$-metric space that satisfies axioms (1) and (2) also satisfies
(3).

###### Proof.

We will show (a) implies (b). So let $\Lambda$ be an ordered abelian group
such that for every positive $\lambda_{0}\in\Lambda$ the set
$[0,\lambda_{0}/2]:=\\{\lambda\in\Lambda\colon 0\leq
2\lambda\leq\lambda_{0}\\}$ has a maximum and let $(X,d)$ be a
$\Lambda$-metric space which is (1) geodesic and (2) whenever two segments
intersect in a single common endpoint, then their union is a segment. Let
$s,s^{\prime}$ be two segments with a common endpoint $x\in X$. We want to
prove that (3) the intersection $s\cap s^{\prime}$ is a segment.

By Lemma 1, $X$ is uniquely geodesic. Let $y$ be the other endpoint of $s$ and
let $z$ be the other endpoint of $s^{\prime}$, i.e. $s=[x,y]$ and
$s^{\prime}=[x,z]$. For $a:=d(x,y)$ and $b:=d(x,z)$, we have parametrizations

$\displaystyle\varphi\colon[0,a]$ $\displaystyle\to
X,\quad\quad\varphi(0)=x,\quad\varphi(a)=y$ $\displaystyle\psi\colon[0,b]$
$\displaystyle\to X,\quad\quad\psi(0)=x,\quad\psi(b)=z$

of the segments $s$ and $s^{\prime}$. Without loss of generality, let $a\leq
b$. We consider $\tilde{z}=\psi(a)\in[x,z]$. By (1) there is a segment
$[y,\tilde{z}]$ with parametrization

$\displaystyle\sigma\colon[0,d(y,\tilde{z})]$ $\displaystyle\to
X,\quad\quad\sigma(0)=y,\quad\sigma(d(y,\tilde{z}))=\tilde{z}.$

We consider the subset $S=\\{\lambda\in\Lambda\colon 0\leq 2\lambda\leq
d(y,\tilde{z})\\}$ which by assumption (a) has a maximum $r\in\Lambda$. We
define $\ell=d(y,\tilde{z})-r$ and note that $\ell\geq r$, since $2r\leq
d(y,\tilde{z})$. Next, we show that $\ell\leq a$ : if $d(y,\tilde{z})\leq a$,
then $\ell\leq d(y,\tilde{z})\leq a$ is clear, otherwise we have
$d(y,\tilde{z})-a\geq 0$, and by the triangle inequality

$2(d(y,\tilde{z})-a)=d(y,\tilde{z})+d(y,\tilde{z})-2a\leq
2a+d(y,\tilde{z})-2a=d(y,\tilde{z})$

and hence $d(y,\tilde{z})-a\in S$, which implies $d(y,\tilde{z})-a\leq r$,
i.e. $\ell\leq a$.

We can now define four points
$p:=\sigma(r),q:=\sigma(\ell),y^{\prime}:=\varphi(a-\ell)$ and
$z^{\prime}:=\psi(a-\ell)$, such that
$d(y,y^{\prime})=d(y,q)=\ell=d(\tilde{z},p)=d(\tilde{z},z^{\prime})$. The
situation is illustrated in Figure 3.

Figure 3. Given the segments $s=[x,y],s^{\prime}=[x,z]\subseteq X$, we can
construct points $\tilde{z},p,q,y^{\prime}$ and $z^{\prime}$ with
$d(y,y^{\prime})=d(y,q)=d(\tilde{z},z^{\prime})=d(\tilde{z},p)=\ell$. The idea
of the proof is to show that $p=y^{\prime}=z^{\prime}$, and $s\cap
s^{\prime}=[x,p]$ and thus a segment.

Our goal is to show that $y^{\prime}=z^{\prime}$ and to then conclude that
$s\cap s^{\prime}=[x,y^{\prime}]$ is a segment. We apply Lemma 2 to the
segments $s=[x,y]$ (and $\tilde{s}^{\prime}=[x,\tilde{z}]$), $y^{\prime}\in s$
(and $z^{\prime}\in\tilde{s}^{\prime}$) and $p$ to create the following case
distinction, illustrated in Figure 4. In all cases we prove that
$y^{\prime}=z^{\prime}$.

Figure 4. We apply Lemma 2 to two segments. The two possibilities in the lemma
lead to four cases we have to consider.

Case 1a): $[x,y^{\prime}]\cap[y^{\prime},p]=\\{y^{\prime}\\}$ and
$[x,z^{\prime}]\cap[z^{\prime},p]=\\{z^{\prime}\\}$.

In this case we have by axiom (2) that $[x,y^{\prime}]\cup[y^{\prime},p]$ and
$[x,z^{\prime}]\cup[z^{\prime},p]$ are segments from $x$ to $p$. Since the
segment $[x,p]$ is unique, and $d(x,y^{\prime})=a-\ell=d(x,z^{\prime})$, it
follows that $y^{\prime}=z^{\prime}$.

Case 1b): $[y,y^{\prime}]\cap[y^{\prime},p]=\\{y^{\prime}\\}$ and
$[x,z^{\prime}]\cap[z^{\prime},p]=\\{z^{\prime}\\}$.

In this case, we have by axiom (2) that
$[y,y^{\prime}]\cup[y^{\prime},p]=[y,p]$ is a segment. Since
$r\leq\ell=d(y,y^{\prime})\leq d(y,y^{\prime})+d(y^{\prime},p)=d(y,p)=r$, we
have in this case $\ell=r$ and $d(y^{\prime},p)=0$, hence $y^{\prime}=p$. Now
we apply (2) again to see that
$[x,z^{\prime}]\cup[z^{\prime},p]=[x,p]=[x,y^{\prime}]$ is a segment. By
uniqueness it is a subsegment of $s=[x,y]$, and since
$d(x,z^{\prime})=a-\ell=d(x,y^{\prime})$ we have that
$z^{\prime}=y^{\prime}=p$.

Case 2a): $[x,y^{\prime}]\cap[y^{\prime},p]=\\{y^{\prime}\\}$ and
$[\tilde{z},z^{\prime}]\cap[z^{\prime},p]=\\{z^{\prime}\\}$.

This case is similar to 1b). We have by axiom (2) that
$[\tilde{z},z^{\prime}]\cup[z^{\prime},p]=[\tilde{z},p]$ is a segment. Since
$d(\tilde{z},z^{\prime})\leq
d(\tilde{z},z^{\prime})+d(z^{\prime},p)=d(\tilde{z},p)=\ell=d(\tilde{z},z^{\prime})$,
we have $d(z^{\prime},p)=0$ and hence $z^{\prime}=p$. Now we apply (2) again
to see that $[x,y^{\prime}]\cup[y^{\prime},p]=[x,p]=[x,z^{\prime}]$ is a
segment. By uniqueness it is a subsegment of $s=[x,\tilde{z}]$, and since
$d(x,y^{\prime})=a-\ell=d(x,z^{\prime})$ we have that
$y^{\prime}=z^{\prime}=p$.

Case 2b): $[y,y^{\prime}]\cap[y^{\prime},p]=\\{y^{\prime}\\}$ and
$[\tilde{z},z^{\prime}]\cap[z^{\prime},p]=\\{z^{\prime}\\}$.

In this case $y^{\prime}=p$ follows as in the first part of Case 1b) and
$z^{\prime}=p$ follows as in the first part of Case 2a).

In all cases we have established that $y^{\prime}=z^{\prime}$. By uniqueness,
we see that $[x,y^{\prime}]=[x,z^{\prime}]\subseteq s\cap s^{\prime}$. It
remains to show that $s\cap s^{\prime}\subseteq[x,y^{\prime}]=[x,z^{\prime}]$.
Let $t,t^{\prime}\in\Lambda$ such that $\varphi(t)=\psi(t^{\prime})\in s\cap
s^{\prime}$. By uniqueness of $[x,\varphi(t)]=[x,\psi(t^{\prime})]$,
$t=t^{\prime}$ has to hold. We use the triangle inequality to get
$d(y,\tilde{z})\leq d(y,\varphi(t))+d(\psi(t),\tilde{z})=2(a-t)$, hence

$2(d(y,\tilde{z})-(a-t))\leq 2(a-t)+d(y,\tilde{z})-2(a-t)=d(y,\tilde{z})$

from which we conclude that $d(y,\tilde{z})-(a-t)\in
S=\\{\lambda\in\Lambda\colon 0\leq 2\lambda\leq d(y,\tilde{z})\\}$ (or is
smaller than $0$), hence $d(y,\tilde{z})-(a-t)\leq r$, so
$\ell=d(y,\tilde{z})-r\leq a-t$ and $t\leq
a-\ell=d(y,y^{\prime})=d(\tilde{z},z^{\prime})$. Thus
$\varphi(t)\in[x,y^{\prime}]=[x,z^{\prime}]$ and $s\cap
s^{\prime}=[x,y^{\prime}]$, proving axiom (3). ∎

##  4\. Independence results

In this section we construct three counterexamples $X_{1},X_{2},X_{3}$. Their
properties are summarized in the following proposition.

######  Proposition 2.

.

  * (i)

When condition (a) of Theorem 1 does not hold, there is a $\Lambda$-metric
space $X_{1}$ satisfying axioms (1) and (2), but not axiom (3).

  * (ii)

When $\Lambda$ is the additive group of an ordered field, there is a
$\Lambda$-metric space $X_{2}$ satisfying axioms (1) and (3), but not axiom
(2).

  * (iii)

When $\Lambda\neq 2\Lambda$, there is a $\Lambda$-metric space $X_{3}$
satisfying axioms (1) and (3), but not axiom (2).

The existence of $X_{1}$ proves that $\neg$(a) implies $\neg$(b) in Theorem 1.
Together with the results of Section 3 this concludes the proof of Theorem 1.
The existence of $X_{2}$ and $X_{3}$ together imply Theorem 2.

###  4.1. Construction of $X_{1}$

We will construct a $\Lambda$-metric space $X_{1}$ that satisfies axioms (1)
and (2), but not (3), whenever the condition

  * (a)

For every positive $\lambda_{0}\in\Lambda$, the set $\\{t\in\Lambda\colon
0\leq 2t\leq\lambda_{0}\\}$ has a maximum.

is not satisfied. So let $\lambda_{0}\in\Lambda$ be an element such that the
set

$I=\\{t\in\Lambda\colon 0\leq 2t\leq\lambda_{0}\\}$

has no maximum and is not empty. Intuitively, $I$ is an interval which has a
minimum $0$, but no maximum. In particular, $\lambda_{0}$ is not divisible by
$2$. We construct a $\Lambda$-metric space $X_{1}$ as illustrated in Figure 5.
We will sometimes use the fact that $\Lambda$ and $[0,\lambda_{0}]$ are
$\Lambda$-trees without proof.

Figure 5. When $\Lambda$ does not satisfy condition (a), we can construct the
$\Lambda$-metric space $X_{1}$ which satisfies (1) and (2), but not (3). The
idea is that the branch-point is missing.

######  Lemma 3.

The set

$X_{1}=\bigcup_{i=1}^{3}I\times\\{i\\}$

with the distance function

$\displaystyle d\colon X_{1}\times X_{1}$ $\displaystyle\to\Lambda$
$\displaystyle((x,i),(y,j))$
$\displaystyle\mapsto\left\\{\begin{array}[]{ll}|x-y|&\text{if }i=j\\\
\lambda_{0}-x-y&\text{else}\\\ \end{array}\right.$

is a $\Lambda$-metric space.

###### Proof.

Positive definiteness and symmetry follow directly, the triangle inequality
requires a case distinction: If all three points are in $I\times\\{i\\}$, then
the triangle inequality follows from the one on $\Lambda$. For
$(x,i),(y,i),(z,j)\in X_{1}$ with $i\neq j$, where without loss of generality
$x\leq y$, an explicit calculation shows

$d((x,i),(y,i))+d((y,i),(z,j))=d((x,i),(z,j)).$

For $(x,i),(y,j),(z,k)\in X_{1}$ with distinct $i,j,k$ a calculation shows
that the strong triangle inequality

$d((x,i),(z,k))<d((x,i),(y,j))+d((y,j),(z,k))$

holds. ∎

######  Lemma 4.

Let $(x,i),(y,j)\in X_{1}$ and $x\leq y$ or $i\neq j$. The image of the map

$\displaystyle\varphi\colon[0,D]$ $\displaystyle\to X_{1}$ $\displaystyle t$
$\displaystyle\mapsto\left\\{\begin{array}[]{ll}(x+t,i)&\text{if}\quad
2(x+t)<\lambda_{0}\\\ (\lambda_{0}-x-t,j)&\text{if}\quad
2(x+t)>\lambda_{0},\\\ \end{array}\right.$

where $D=d((x,i),(y,j))$, is a segment from $(x,i)$ to $(y,j)$. The
$\Lambda$-metric space $(X_{1},d)$ is geodesic.

###### Proof.

If $i=j$ and $x\leq y$, $D=y-x$ and $2(x+t)<\lambda_{0}$ is satisfied for all
$t\in[0,D]$. It is then clear that the map $\varphi$ is an isometry with
$\varphi(0)=(x,i)$ and $\varphi(D)=(y,j)$. The corresponding segment is given
by $[x,y]\times\\{i\\}$.

For $i\neq j$, we have $D=\lambda_{0}-x-y$. The map $\varphi$ is well defined
since if $2(x+t)>\lambda_{0}$, then
$2(\lambda_{0}-x-t)=2\lambda_{0}-2(x+t)<2\lambda_{0}-\lambda_{0}=\lambda_{0}$.
The endpoints behave correctly, $\varphi(0)=(x,i)$ and $\varphi(D)=(y,j)$
since $2(x+D)=2(x+\lambda_{0}-x-y)=\lambda_{0}+(\lambda_{0}-2y)>\lambda_{0}$
and hence $\varphi(D)=(\lambda_{0}-x-D,j)=(y,j)$. It remains to show that
$\varphi$ is an isometry. Let $t,t^{\prime}\in[0,D]$ with $t<t^{\prime}$. If
$2(x+t)$ and $2(x+t^{\prime})$ are both either larger or smaller than
$\lambda_{0}$, then $\varphi(t)$ and $\varphi(t^{\prime})$ are contained in
the same copy of $I$ and the isometries follow from calculations in $\Lambda$.
If $2(x+t)<\lambda_{0}$ and $2(x+t^{\prime})>\lambda_{0}$, then

$d(\varphi(t),\varphi(t^{\prime}))=\lambda_{0}-(x+t)-(\lambda_{0}-x-t^{\prime})=t^{\prime}-t.$

Given any two points $(x,i)$ and $(y,j)$ in $X$ we may assume without loss of
generality $x\leq y$. The image of the map $\varphi$ thus gives us the
segment. ∎

From Lemma 4 we can conclude that $[0,\lambda_{0}]$ is isometric to
$I\times\\{i\\}\cup I\times\\{j\\}$ whenever $i\neq j$, (choose $x=y=0$). The
segments described in Lemma 4 can therefore be viewed as subsets of
$[0,\lambda_{0}]$. The next lemma states that the segments in Lemma 4 are the
only ones.

######  Lemma 5.

The $\Lambda$-metric space $(X_{1},d)$ is uniquely geodesic.

###### Proof.

Every segment from $(x,i)$ to $(y,j)$ admits a parametrization of the form
$\psi\colon[0,D]\to X_{1}$, where $\psi(0)=(x,i)$ and $\psi(D)=(y,j)$. We
first claim that for every $t\in[0,D]$, $\psi(t)\in I\times\\{i\\}\cup
I\times\\{j\\}$. If this were not the case, then we would have

$\displaystyle d((x,i),\psi(t))$ $\displaystyle=\lambda_{0}-x-r$
$\displaystyle d((y,j),\psi(t))$ $\displaystyle=\lambda_{0}-y-r$

for some $r\in I$ with $(r,k)=\psi(t)$. We would then have

$D=d((x,i),(y,j))=d((x,i),\psi(t))+d((y,j),\psi(t))=2\lambda_{0}-x-y-2r$

since $\psi$ is an isometry. If $i=j$ and without loss of generality $x<y$
then

$y-x=2\lambda_{0}-x-y-2r$

which contradicts $\lambda_{0}>2r$ and $\lambda_{0}>2y$. If $i\neq j$, then

$D=\lambda_{0}-x-y=2\lambda_{0}-x-y-2r$

which contradicts $\lambda_{0}>2r$.

Let $k\neq i$ and $k=j$ if $j\neq i$. We can use Lemma 4 with $(0,i)$ and
$(0,k)$ to get an isometry $f\colon[0,\lambda_{0}]\to I\times\\{i\\}\cup
I\times\\{k\\}$. Since segments in $[0,\lambda_{0}]$ are unique, also segments
in $f([0,\lambda_{0}])=I\times\\{i\\}\cup I\times\\{k\\}$, such as
$\psi([0,D])$ are unique, concluding the proof. ∎

######  Lemma 6.

The $\Lambda$-metric space $(X_{1},d)$ satisfies axiom (2).

###### Proof.

Let $s,s^{\prime}$ be two segments that intersect exactly in one common
endpoint $(x,i)\in X_{1}$. We will show that there is a $j\neq i$ such that
both $s$ and $s^{\prime}$ are contained in $I\times\\{i\\}\cup
I\times\\{j\\}$. If the other endpoint of $s$ is in $I\times\\{j\\}$ and the
other endpoint of $s^{\prime}$ is in $I\times\\{k\\}$ for distinct $i,j,k$,
then $s\subset I\times\\{i\\}\cup I\times\\{j\\}$ and $s^{\prime}\subset
I\times\\{i\\}\cup I\times\\{k\\}$ and we know how the segments look like by
the description of segments in Lemmas 4 and 5. Let $y\in I$ with $x<y$, which
exists because $x$ is not a maximum of $I$, (we are assuming $I$ does not have
a maximum). But then $(y,i)\in s\cap s^{\prime}$ by the description of the
segments in Lemma 4, which contradicts the assumption $s\cap
s^{\prime}=\\{(x,i)\\}$.

We conclude that there is a $j\neq i$ such that both $s$ and $s^{\prime}$ are
contained in $I\times\\{i\\}\cup I\times\\{j\\}$, which is isometric to
$[0,\lambda_{0}]$. Since axiom (2) holds in $[0,\lambda_{0}]$ also $s\cup
s^{\prime}$ is a segment. ∎

######  Lemma 7.

The $\Lambda$-metric space $(X_{1},d)$ does not satisfy axiom (3).

###### Proof.

Let $s$ be the unique segment from $(0,1)$ to $(0,2)$ and let $s^{\prime}$ be
the unique segment from $(0,1)$ to $(0,3)$. The point $(0,1)$ is a common
endpoint of $s$ and $s^{\prime}$. Since $s\cap s^{\prime}=I\times\\{1\\}$, and
$I$ does not have a maximum, $s\cap s^{\prime}$ is not isometric to a closed
$\Lambda$-interval and hence is not a segment. ∎

We have constructed a $\Lambda$-metric space $(X_{1},d)$ which satisfies
axioms (1) and (2) but not (3). This shows $\neg$(a) $\implies\neg$(b) in
Theorem 1 and thus completes its proof.

This example shows that axiom (3) forces the branchpoints to be part of the
$\Lambda$-tree. For groups such as $\Lambda=\mathbb{Q}$ (or
$\mathbb{Z}[\frac{1}{2}]$), one might be tempted to construct $\Lambda$-metric
spaces with branchpoints at an irrational distance (or at $\frac{1}{3}$).
However, that construction fails, since the resulting metric does not take
values in $\Lambda$. The number $\frac{1}{2}$ plays a special role, as
reflected in condition (a) of Theorem 1.

###  4.2. Construction of $X_{2}$

It was noted in [AB87], that for $\Lambda=\mathbb{R}$, axiom (2) is
independent from the axioms (1) and (3), consider for instance
$\mathbb{R}^{2}$ with the Euclidean distance. In view of Proposition 1, any
such example has to be geodesically unique. The idea of this section is thus
to build a uniquely geodesic $\Lambda$-metric space $X_{2}$ which is
$2$-dimensional in some sense.

Let $\Lambda$ be the additive group of a ordered field. The idea is to create
a version of the $\ell_{1}$-distance (also called the Manhattan-distance) but
using polar coordinates instead of the usual Cartesian coordinates. The
distance can be thought as the length of the shortest path consisting only of
radial and circumferential movements. To be uniquely geodesic, we restrict
ourselves to a subset. The situation is illustrated in Figure 6. We consider
the set

$X_{2}=(0,2]\times[0,1]=\\{(t,\varphi)\in\Lambda^{2}\colon 0<t\leq 2,\
0\leq\varphi\leq 1\\}$

and endow it with the function $d\colon X_{2}\times X_{2}\to\Lambda$ given by

$\displaystyle
d((t_{1},\varphi_{1}),(t_{2},\varphi_{2}))=|t_{2}-t_{1}|+\min\\{t_{1},t_{2}\\}\cdot|\varphi_{2}-\varphi_{1}|.$

Figure 6. In the $\Lambda$-metric space $X_{2}$ segments consist of a radial
part and the shorter of two circumferential parts. Unlike in the Manhattan-
distance, segments are unique.

######  Lemma 8.

The pair $(X_{2},d)$ is a $\Lambda$-metric space.

###### Proof.

Symmetry is clear from the definition and positive definiteness follows from
the fact that $\Lambda$ is a field. We prove the triangle inequality. Let
$p_{i}=(t_{i},\varphi_{i})\in X_{2}$ for $i\in\\{1,2,3\\}$ be three points. To
prove $d(p_{1},p_{2})\leq d(p_{1},p_{3})+d(p_{3},p_{2})$, we may assume
without loss of generality that $t_{1}\leq t_{2}$. We first show the triangle
inequality for the case $t_{3}\leq t_{1}$,

$\displaystyle d(p_{1},p_{2})$
$\displaystyle=t_{2}-t_{1}+t_{1}|\varphi_{2}-\varphi_{1}|$
$\displaystyle=t_{2}-t_{1}+(t_{1}-t_{3})|\varphi_{2}-\varphi_{1}|+t_{3}|\varphi_{2}-\varphi_{1}|$
$\displaystyle<t_{2}-t_{1}+2(t_{1}-t_{3})+t_{3}|\varphi_{2}-\varphi_{1}|$
$\displaystyle\leq
t_{2}-t_{3}+t_{1}-t_{3}+t_{3}|\varphi_{3}-\varphi_{1}|+t_{3}|\varphi_{2}-\varphi_{3}|$
$\displaystyle=d(p_{1},p_{3})+d(p_{3},p_{2})$

and then in the case $t_{1}\leq t_{3}$

$\displaystyle d(p_{1},p_{2})$
$\displaystyle=t_{2}-t_{1}+t_{1}|\varphi_{2}-\varphi_{1}|$ $\displaystyle\leq
t_{2}-t_{3}+t_{3}-t_{1}+t_{1}|\varphi_{3}-\varphi_{1}|+t_{1}|\varphi_{2}-\varphi_{3}|$
$\displaystyle\leq|t_{3}-t_{2}|+|t_{3}-t_{1}|+t_{1}|\varphi_{3}-\varphi_{1}|+t_{1}|\varphi_{2}-\varphi_{3}|$
$\displaystyle=d(p_{1},p_{2})+d(p_{2},p_{3}).$

∎

######  Remark 3.

We note that we could also define this metric on some other subsets of
$\Lambda\times\Lambda$. For some examples like $(0,1]\times[0,2]$ and
$\Lambda_{\geq 0}\times[0,2]$ we also get a $\Lambda$-metric space, but the
triangle inequality would not hold on $(0,1]\times[0,3]$. We could also add
one more point $(0,0)$ to $X_{2}$ and get a metric space that includes the
”centerpoint”.

######  Lemma 9.

The $\Lambda$-metric space $(X_{2},d)$ is uniquely geodesic.

###### Proof.

For the points $p_{i}=(t_{i},\varphi_{i})$ with $i\in\\{1,2\\}$ we may assume
without loss of generality that $t_{1}\leq t_{2}$. We write
$\varphi_{0}:=t_{1}\cdot|\varphi_{2}-\varphi_{1}|$, so that
$d(p_{1},p_{2})=\varphi_{0}+(t_{2}-t_{1})$. One can check that

$\displaystyle f\colon[0,d(p_{1},p_{2})]$ $\displaystyle\to X_{2}$
$\displaystyle t$
$\displaystyle\mapsto\left\\{\begin{array}[]{ll}\left(t_{1},\frac{1}{\varphi_{0}}\left(t\cdot\varphi_{2}+(\varphi_{0}-t)\cdot\varphi_{1}\right)\right)&\text{if}\quad
t<\varphi_{0}\\\ (t-\varphi_{0}+t_{1},\varphi_{2})&\text{if}\quad
t\geq\varphi_{0}\end{array}\right.$

defines a segment-map whose image $s$ is a segment with $p_{1}$ and $p_{2}$ as
endpoints. Let $p=(t,\varphi)\in X\setminus s$. We claim that then
$d(p_{1},p_{2})<d(p_{1},p)+d(p,p_{2})$. If $t<t_{1}\leq t_{2}$, then

$\displaystyle d(p_{1},p_{2})$
$\displaystyle=t_{2}-t_{1}+t_{1}|\varphi_{2}-\varphi_{1}|$
$\displaystyle=t_{2}-t_{1}+(t_{1}-t)|\varphi_{2}-\varphi_{1}|+t|\varphi_{2}-\varphi_{1}|$
$\displaystyle<t_{2}-t_{1}+2(t_{1}-t)+t|\varphi_{2}-\varphi_{1}|$
$\displaystyle\leq
t_{2}-t+t_{1}-t+t|\varphi_{3}-\varphi_{1}|+t|\varphi_{2}-\varphi_{3}|$
$\displaystyle=d(p_{1},p)+d(p,p_{2}).$

If $t_{1}\leq t_{2}<t$, then $t_{2}-t<t-t_{2}=|t-t_{2}|$ and

$\displaystyle d(p_{1},p_{2})$
$\displaystyle=t_{2}-t+t-t_{1}+t_{1}|\varphi_{2}-\varphi_{1}|$
$\displaystyle<|t_{2}-t|+|t_{1}-t|+t_{1}|\varphi_{2}-\varphi|+t_{1}|\varphi-\varphi_{1}|$
$\displaystyle\leq|t_{2}-t|+t_{2}|\varphi_{2}-\varphi|+|t_{1}-t|+t_{1}|\varphi-\varphi_{1}|$
$\displaystyle=d(p_{1},p)+d(p,p_{2}).$

If $t\in[t_{1},t_{2}]$, we have

$\displaystyle d(p_{1},p_{2})$
$\displaystyle=|t_{2}-t_{1}|+t_{1}|\varphi_{2}-\varphi_{1}|$
$\displaystyle\leq|t_{2}-t|+|t-t_{1}|+t_{1}(|\varphi_{2}-\varphi|+|\varphi-\varphi_{1}|)$
$\displaystyle=|t-t_{1}|+t_{1}|\varphi-\varphi_{1}|+|t_{2}-t|+t_{1}|\varphi_{2}-\varphi|$
$\displaystyle\leq|t-t_{1}|+t_{1}|\varphi-\varphi_{1}|+|t_{2}-t|+t|\varphi_{2}-\varphi|$
$\displaystyle=d(p_{1},p)+d(p,p_{2})$

and we see that in the last inequality, equality can only hold when
$t_{1}|\varphi_{2}-\varphi|=t|\varphi_{2}-\varphi|$, i.e. when $t_{1}=t$ or
$\varphi_{2}=\varphi$, which is exactly when $p\in s$. This shows the claim
and we can conclude that $s$ is the unique segment from $p_{1}$ to $p_{2}$. ∎

######  Remark 4.

We note that the $\Lambda$-metric space $X_{2}$ could also be defined more
generally for $\Lambda$ the additive group of an ordered integral domain, but
the segment-parametrization in Lemma 9 requires division.

######  Lemma 10.

The $\Lambda$-metric space $(X_{2},d)$ satisfies axiom (3).

###### Proof.

We know from Lemma 9 how segments look like. Let $s_{1},s_{2}$ be two segments
with a common endpoint $p$. Let $p_{1}=(t_{1},\varphi_{1})$ be the other
endpoint of $s_{1}$ and $p_{2}=(t_{2},\varphi_{2})$ be the other endpoint of
$s_{2}$. If $\varphi_{1}\neq\varphi_{2}$, then the intersection $s_{1}\cap
s_{2}$ is contained in $\\{t\\}\times[0,1]$ and we know that $s_{1}\cap s_{2}$
is a segment, since $\\{t\\}\times[0,1]$ is a $\Lambda$-tree and satisfies
axiom (3). If $\varphi_{1}=\varphi_{2}$ then we know that $s_{1}\cap
s_{2}\cap(0,1]\times\\{\varphi_{1}\\}$ is a segment of the $\Lambda$-tree
$(0,1]\times\\{\varphi_{1}\\}$. By the description of the segments in Lemma 9
$s_{1}\cap s_{2}$ is a segment. ∎

######  Lemma 11.

The $\Lambda$-metric space $(X_{2},d)$ does not satisfy axiom (2).

###### Proof.

We consider the segments $s_{1}=[(1,0),(2,0)]$ and $s_{2}=[(1,0),(2,1)]$. The
two segments intersect exactly in one point $(1,0)$, but the union $s_{1}\cup
s_{2}$ is not a segment by the description of segments in Lemma 9. ∎

###  4.3. Construction of $X_{3}$

We now give an example for the case $\Lambda\neq 2\Lambda$. Let $a\in\Lambda$
not divisible by $2$. Consider the space $X_{3}=[0,3a]/\\!\\!\sim$, where we
identify $0\sim 3a$. The $\Lambda$-metric is given by

$d(p,q)=\min\left\\{\left|q-p+k\cdot 3a\right|\colon
k\in\mathbb{Z}\right\\},\quad\quad\text{for }p,q\in X_{3}.$

Intuitively we have turned the interval $[0,3a]$ into a circle with the
shortest path metric. From the definition it follows that $(X_{3},d)$ is a
$\Lambda$-metric space and that it satisfies (1) and (3). Axiom (2) is however
not satisfied, because the union $[0,a]\cup[a,2a]$ of two segments is not
again a segment, since $d(0,2a)=a\neq 2a$. The actual segment connecting $0$
to $2a$ is $[2a,3a]$.

## References

  * [AB87] R. Alperin, H. Bass, _Length functions of group actions on $\Lambda$-trees._ Combinatorial group theory and topology, (Ed. S. M. Gersten and J. R. Stallings), Annals of Math. Studies 111, 265–378. Princeton University Press, 1987.
  * [App23] R. Appenzeller _$\Lambda$ -metric-space - Lean project_, https://github.com/Strichcoder/lambda-metric-space, 2023.
  * [Ben90] C. Bennett, _Affine $\Lambda$-buildings_, Ph.D.-thesis. University of Chicago, 1990.
  * [Ben94] C. Bennett, _Affine $\Lambda$-buildings I._, Proc. London Math. Soc. (3), 68(3):541-576, 1994.
  * [BCM10] K. Buzzard, J. Commelin and P. Massot, _Formalising perfectiod spaces_ , Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
  * [BSS14] C. Bennett, P. Schwer, K. Struyve, _On axiomatic definitions of non-discrete affine buildings_ , Adv. Geom., 14(3):381-412, 2014.
  * [BR88] G. W. Brumfiel, _The tree of a non-Archimedean hyperbolic plane_ , Contemporary Mathematics, 74, 1988.
  * [Chi01] I. M. Chiswell, _Introduction to $\Lambda$-trees_, River Edge, NJ: World Scientific Publishing Co. Inc., ISBN 981-02-4386-3, 2001.
  * [dM+15] L. M. de Moura, S. Kong, J. Avigad, F. van Doorn and J. von Raumer, _The Lean Theorem Prover (System Description)_ Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 378-388, 2015.
  * [mC19] The mathlib Community. _The Lean mathematical library_ , 2019. arXiv:1910.09336.
  * [MS84] J. W. Morgan and P. B. Shalen. _Valuations, trees, and degenerations of hyperbolic structures. I._ Ann. of Math. (2), 120(3):401–476, 1984.
  * [Par00] A. Parreau, _Immeubles affines: construction par les normes._ Crystallographic Groups and Their Generalizations: Workshop, Katholicke Universiteit Leuven Campus Kortrijk, Belgium, May 26-28, 1999, 262, page 263. American Mathematical Soc., 2000.


11institutetext: Instituto de Astrofísica de Canarias, Vía Láctea S/N, La
Laguna 38205, Tenerife, Spain
11email<EMAIL_ADDRESS>22institutetext: Departamento de Astrofísica,
Universidad de La Laguna, 38205, Tenerife, Spain

# How likely is the interstellar origin of CNEOS14?

On the reliability of the CNEOS database

H. Socas-Navarro 1122

This paper investigates the likelihood that the CNEOS 2014-01-08 superbolide
(CNEOS14) was caused by an interstellar object. This issue has remained
controversial due to lack of information on the capabilities of the classified
satellite sensors that recorded the fireball. We critically evaluate previous
studies, specifically addressing the reliability of the CNEOS database and the
associated measurement uncertainties. With proper statistical analysis of
existing data and the addition of a relevant new event (the 2024 Iberian
superbolide), we disprove some claims in previous work, such as: a) the
existence of a purported correlation between CNEOS velocity errors and bolide
speed; b) the presence of large velocity errors of 10-15 km/s in the CNEOS
database; and c) the assertion that CNEOS14 is most likely a solar system
object with a hyperbolic trajectory due to measurement errors. We present a
quantitative estimate of the probability that CNEOS14 is interstellar. If its
measurement errors are drawn from the same underlying distribution as the 18
calibrated events, then the probability that CNEOS14 is interstellar is 94.1%.
This probability is lower than the 99.7% confidence (3-$\sigma$) generally
required to claim a scientific discovery. However, it is sufficiently high to
be considered significant and, by far, the most likely explanation for the
currently available empirical evidence.

###### Key Words.:

Meteorites, meteors, meteoroids – Astronomical data bases – methods:
statistical

##  1 Introduction

The possibility that some meteors might be of interstellar origin has
motivated extensive investigation and searches for such events since at least
the 1950s (Fisher 1928; Opik 1950; Almond et al. 1950; Peña-Asensio et al.
2022 and references therein). However, the unambiguous identification of
interstellar impactors on our planet has proven to be a formidable challenge
(Hajdukova et al. 2020).

Empirical evidence exists for interstellar objects passing through our solar
system. Two sub-kilometer bodies have been observed in unbound trajectories,
1I/’Oumuamua and 2I/Borisov. On the smaller end of the size spectrum, in situ
measurements of dust by the spacecraft Ulysses and Galileo have resulted in
the unequivocal detection of particles coming from beyond the boundaries of
our solar system. Using these two extremes of the size distribution as
constraints, one can estimate that the distribution of flux versus particle
size may be approximated with a $r^{-3}$ power law (Jewitt & Seligman 2023),
where $r$ is the radius of the object. There should be an abundance of
interstellar meteoroids of all sizes, even asteroids, routinely impacting our
planet. However, except for one notable exception, observational uncertainties
have prevented a sufficiently confident separation of hyperbolic and
elliptical orbits, thus precluding the identification of interstellar meteors
or bolides.

Siraj & Loeb (2022) identified a peculiar event in the CNEOS fireball database
maintained by NASA’s Jet Propulsion
Laboratory111https://cneos.jpl.nasa.gov/fireballs/. The bolide was recorded
with a geocentric speed of 44 km s-1, implying that the meteoroid had a very
hyperbolic heliocentric speed of 60 km s-1 (the Sun’s escape velocity at 1 AU
is 42 km s-1). Although the authors referred to it as IM1 (interstellar meteor
1), we shall adopt here the more neutral nomenclature CNEOS14 to remain
agnostic about its possible interstellar origin. By that name we shall
designate both the fireball and the meteoroid, as the context will make it
clear which one we are alluding to.

CNEOS14 exhibits some peculiarities; most notably, it has a low inclination
with respect to the plane of the ecliptic (7o) and a high velocity with
respect to the local standard of rest if we assume that it has not interacted
with any other object on its way before reaching our planet. Socas-Navarro
(2023) pointed out that these anomalies would be resolved if the meteoroid had
experienced a gravitational encounter with the putative Planet Nine, a
scenario that is further supported by the coincidence of its trajectory with
the highest probability region of finding Planet Nine (Brown & Batygin 2021).

Following the claim of an interstellar bolide discovery, the authors organized
an expedition to search for a meteorite on the ocean floor near the impact
site. The use of infrasound and seismic stations to obtain a precise location
(Siraj & Loeb 2023), the recovery of spherules, allegedly from CNEOS14, and
their analysis (Loeb et al. 2024a, b) were subjects of intense controversy in
the scientific literature (Fernando et al. 2024; Gallardo 2023, 2024; Desch
2024), but also in mainstream media, sparked in great measure by the
suggestion of an artificial extraterrestrial origin (Loeb et al. 2024a). This
controversy extends to a wider context of high-profile claims by these authors
on key areas of solar system research, including a cometary origin for the
Chicxulub impactor (Siraj & Loeb 2021), or the extraterrestrial technological
origin of 1I/’Oumuamua (Bialy & Loeb 2018; Sheerin & Loeb 2021; Loeb 2022).
Other authors deem all these extraordinary claims as unfounded, exaggerated or
not backed by empirical data (Desch et al. 2022; Bannister et al. 2019).

A recent paper by Brown & Borovička (2023) (hereafter BB23) raises doubts on
the interstellar origin of CNEOS14, stating instead that it was most likely a
solar system object. Its apparent interstellar origin, according to these
authors, would be the result of a combination of large measurement errors. The
CNEOS database is populated with events provided to NASA by the U.S. Space
Force which, unfortunately, are obtained by satellite sensors whose
characteristics have not been disclosed (Tagliaferri et al. 1994). In
particular, the measurement uncertainties are not published. Given the
scientific relevance of this particular event, some further information has
been disclosed by the U.S. Department of Defense, including the light
curve222https://cneos.jpl.nasa.gov/fireballs/lc/bolide.2014.008.170534.pdf and
a statement confirming (using additional data available to them) that the data
in the CNEOS database is sufficiently accurate to indicate the meteoroid’s
interstellar trajectory333https://lweb.cfa.harvard.edu/ loeb/DoD.pdf.
Fortunately, some information about the reliability of the measurements may be
inferred from a set of CNEOS fireballs that were also measured by independent
scientific observatories (see section 2 below).

We quantified the likelihood that, based on the available evidence, CNEOS14
was a solar system object and tested some relevant claims of BB23 that were
made without a quantitative justification. Specifically, we find the following
claims to be inconsistent with the available evidence: a)there is a
correlation between the measured velocity and the velocity error; b)CNEOS14’s
velocity has an error of 10-15 km s-1; c)the simplest explanation is that
CNEOS14 is a solar system object whose trajectory appears hyperbolic due to
measurement errors.

Due to their relatively unsurprising nature, these claims are already
propagating in the literature as other authors take them as established truth
without further scrutiny (Fernando et al. 2024; Desch & Jackson 2023). We thus
felt compelled to write this paper with the goal of clarifying what can and
cannot be inferred from the data in order to prevent further confusion. Debate
and even controversy are inherent aspects of the scientific process. However,
it is important to maintain it rigorous and dispassionate, and not respond to
exaggerated or unfounded claims with others of similar nature.

##  2 Velocity errors

The key factor to assess a possible extrasolar origin of CNEOS14 is its
velocity vector. With its measured radiant, the velocity error would need to
be greater than 20 km s-1 to make its orbit bound to the Sun (there is, of
course, the possibility that a smaller velocity error could be combined with
radiant errors; we shall address this in the next section). Even though there
is no public information on the CNEOS database uncertainties, it is possible
to obtain some upper bounds by comparing data for events that have been
simultaneously observed with scientific ground-based facilities. Such
comparisons have been performed by Devillepoix et al. (2019), Peña-Asensio et
al. (2022), BB23, Peña-Asensio et al. (2024b). Similarly to these authors, we
shall here adopt the interpretation that the discrepancies with the ground-
based measurements are ascribed entirely to errors in the CNEOS entries.

###  2.1 Using 2023 data

BB23 argued that faster bolides should yield larger measurement errors, which
would be true if the measurements were limited by cadence. To test this
hypothesis, they plotted the velocity error $dv$ (discrepancy between the
CNEOS and ground-based measurements) versus the fireball velocity $v$ for the
17 available events (their Figure 2, recreated here in Figure 1, left panel).
The result is a rather scattered cloud of points with one outlier (the point
marked as a blue dot in Figure 1) that has high velocity and high error
($v$=35.7 km s-1, $dv$=7.9 km s-1). The outlier might give the reader a visual
impression that there is a correlation between $v$ and $dv$.

In order to avoid subjectivity and confirmation bias, one needs to quantify
the correlation coefficient to determine if a correlation really exists.
Unfortunately, BB23 did not make this straightforward calculation and simply
relied on the subjective appearance of the plot to make a very strong claim,
namely that there is a correlation between the error $dv$ and the velocity
$v$. Here we have calculated the relevant numbers to test this assertion. The
Spearman’s rank correlation coefficient (Spearman 1904) for this particular
set of points is a modest $\rho$=0.42 (the presence of a strong outlier makes
the Spearman’s coefficient a better suited statistical test than the Pearson’s
coefficient, as it is less sensitive to outliers), with an associated
$p$-value of 0.095. In the context of hypothesis contrast, a correlation is
considered statistically significant when its associated $p$-value is lower
than 0.05. Values greater than 0.10 are generally considered as ”no evidence”.
Therefore, even with the methodology and data employed by BB23, we can
conclude that the claim of a correlation between $dv$ and $v$, which they base
solely on subjective perception, is not supported by objective evidence.

Figure 1: Left panel: Velocity error vs velocity for the 17 events analyzed in
BB23. Right panel: Same as the left panel but considering the absolute value
of the errors. In both panels, the high-velocity, high-error outlier is marked
as a blue point.

We observed another problem with the BB23 methodology. In their figure they
plotted the velocity errors with sign, thus increasing the influence of the
(positive-sign) outlier. In order to rigorously test their hypothesis (that
the limited cadence results in larger errors for faster meteors), they should
have considered the absolute values of the errors $|dv|$. We show this plot in
Figure 1 (right panel). As expected, taking the absolute value of the errors
results in a lower weight of the outlier and even weaker correlation
coefficients. The Spearman’s coefficient is now 0.14 and its $p$-value is
0.60. In conclusion, there is absolutely no correlation between $|dv|$ and
$v$.

###  2.2 The 2024 Iberian superbolide

As we have seen, the visual appearance of correlation in the BB23 scatter plot
is based entirely on one single outlier point on the far right side of the
figure. During the writing of this paper, a very bright fireball occurred that
provided very relevant new data. Here we discuss the implications of this
fortuitous event. An extremely bright bolide was seen over Spain and Portugal
the night of May 18th 2024, which was recorded both by the USG satellite
sensors and by scientific observatories (Peña-Asensio et al. 2024a). The
superbolide was nearly as fast as CNEOS14, measured at 40.1 km s-1 by ground-
based stations. When it is added to the dataset, we obtain the plots shown in
Figure 2 (the new event is represented by the red dot). As before, the left
panel shows the data using the same methodology as BB23, whereas the right
panel shows the absolute value of the error, which we believe would be the
correct approach. Notice how the addition of this second point on the right-
hand side of the figure completely eliminates any possible subjective
perception of a correlation between $dv$ and $v$.

Figure 2: Same as Fig 1 but including the recent event (2024 Iberian
superbolide), shown here as a red point.

For completeness, Figure 3 shows the radiant errors. The plot in the upper-
left panel is similar to Figure 3 in BB23 but updated to include the 2024
Iberian superbolide. The other panels plot the R.A. and declination errors
separately.

Figure 3: Scatter plots of velocity and radiant errors. The radiant errors are
shown combined (upper left panel) or separated into R.A. ($d\alpha$) and dec
($d\delta$). The blue and red points mark the same events as in Figs 1 and 2.

###  2.3 Extrapolation

There is a second strong claim in BB23 that is not well justified. They state
that the comparison of CNEOS data to ground-based observations shows that the
former has large uncertainties of 10-15 km s-1 at high-speed events. This is
as much as twice the largest value of $dv$ observed in the database. To obtain
this 10-15 km s-1 range, they fit a straight line to the points in Figure 1
and extrapolate it to the CNEOS14 observed speed (44.8 km s-1). However, as we
have shown above, there is no significant correlation between $dv$ and $v$ and
therefore this fit is meaningless. In fact, if it is done considering the 2024
Iberian superbolide, then the extrapolation yields a completely different
(much lower) value.

Figure 4: Various fits to various measurement errors as a function of bolide
speed and the extrapolation to the error expected for CNEOS14. Top panel:
Velocity error for the 17 events analyzed in BB23. Middle panel: Same as the
upper panel but including the 2024 Iberian superbolide (red point). Bottom
panel: Radiant error. All panels: The blue line is a simple straight line fit,
as in BB23. The other lines are three different statistically robust fits,
less sensitive to outliers (see text for details and references). The crosses
mark the extrapolation of each fit to CNEOS14’s speed (numerical values are
given in the legend).

Figure 4 (top panel, blue line) shows the results of fitting the cloud of 17
points to a straight line, as done in BB23 (but with unsigned errors).
Clearly, the fit is dominated by a strong outlier (marked by the blue point in
the figure), resulting in an extrapolated error $dv$ for CNEOS14 of 9.6 km
s-1. We compared this result to what is obtained using three different robust
fitting methods: RANSAC (Derpanis 2010), Theil-Sen (Akritas et al. 1995), and
Siegel (Siegel 1982). With the robust fits, the extrapolated errors for the
CNEOS14 velocity are: -0.7, 1.1 and 0.4 km s-1, respectively.

If we now add the 2024 Iberian superbolide to the plot (middle panel of Figure
4), we have a second data point (marked in red) in the fast event region of
the plot. Even the simple straight line fit now yields a lower extrapolated
error of 4.5 km s-1. The robust extrapolations now yield 1.9, 0.6 and 0.4 km
s-1, respectively. For completeness, the bottom panel of the figure shows a
similar plot for the radiant error.

We conclude that the data of CNEOS errors does not exhibit any correlations
that would support the notion of anomalously large errors for CNEOS14,
compared to the rest of the dataset. For the 18 events considered here (the 17
in BB23 plus the 2024 Iberian superbolide), the standard deviation of the
velocity error is $\sigma$(dv)=3.2 km s-1, the standard deviation of the
absolute value of the velocity error is $\sigma$(—dv—)=2.5 km s-1, and the
maximum error in the sample is 7.9 km s-1. Figure 2 seems to hint at a
possible bimodal distribution of errors, with 72% of events having errors
smaller than 2 km s-1 and 28% between 4 and 8 km s-1, but they are not
correlated with speed.

###  2.4 Combining velocity and radiant errors

BB23 argue that, even if the velocity errors are lower than the 20 km s-1
needed to make CNEOS14’s orbit unbound, there exist combinations of velocity
and radiant errors that would do so. This argument is then used to claim that
CNEOS14 is most likely a solar system object. The relevant question in this
situation is how likely are such combinations of errors. Evidence for
scientific discoveries is generally reported within some confidence intervals
(typically 3-$\sigma$ or 99.7% confidence, but in some scenarios the
requirements are even more strict). In order to make the case for dismissing
the empirical evidence of CNEOS14’s hyperbolic orbit, one would need to show
that the probability of the required measurement error is significant.
Unfortunately, BB23 did not present any attempts to quantify this probability
and relied solely on a qualitative discussion involving a large extrapolated
error for CNEOS14 combined with a large radiant error. Figure 4 indicates that
such scenario might be rather unlikely. In this section we take a quantitative
look at the problem.

We have estimated the probability that CNEOS14 is hyperbolic by using the
available information on the CNEOS events that have been simultaneously
measured by scientific observatories. To that aim, we constructed a matrix
with all the measured errors in velocity $dv$ and radiant ($d\alpha$,
$d\delta$), where $\alpha$ and $\delta$ represent the R.A. and declination,
respectively. Each value of $dv$ and ($d\alpha$, $d\delta$) is included with
both positive and negative sign. In total, we have
2$\times$18$\times$2$\times$18 (i.e., 1296) combinations of errors. We then
looped through all of these and added them as a perturbation to the nominal
speed and radiant of CNEOS14. Each one of these perturbed velocities was then
transformed to the solar system barycentric reference frame and we counted how
many had a barycentric velocity in excess of the Sun’s escape velocity at 1
AU, 42 km s-1.

We obtained that CNEOS14 is still hyperbolic in 94.3% of the 1296 cases
analyzed. The percentage does not depend significantly on the inclusion of the
2024 Iberian superbolide (93.9% if we neglect it). This probability is below
the 99.7% that is typically required to claim a firm scientific discovery but
it seems sufficient to assert that, based on the best available empirical
evidence, CNEOS14 was most likely on a hyperbolic trajectory (assuming that
its uncertainties are represented by the same underlying distribution as the
18 calibrated events).

##  3 Conclusions

We have concentrated here on analyzing the velocity vector because, as BB23
noted, it is the crux of the problem. They discussed other arguments, such as
the fact that other apparently hyperbolic bolides in the database have orbits
that are very close to elliptical, within reasonably small observational
errors. This is actually expected behavior (where some highly eccentric orbits
may be converted into hyperbolic with small velocity errors) that does not say
anything about the probability that CNEOS14 is hyperbolic. In other words, the
existence of a population of hyperbolic impostors does not undermine the
reality of legitimate hyperbolics. Additionally, arguments concerning the
challenges of fitting certain aspects of CNEOS14 to current models are not
very persuasive, either. It is plausible that models derived from the fitting
of solar system meteors might not apply equally well to a potentially
different class of objects with extrasolar origin. Therefore, the real issue
is to understand as best as we can the empirical data and the associated
uncertainties. In lieu of a disclosure of more detector information, future
progress might come from the accumulation of more calibration data in the form
of new fireballs simultaneously observed by scientific observatories and the
CNEOS sensors.

In the meantime, the best we can do is to analyze the existing events with
adequate statistical methodologies. We have found that, contrarily to
assertions made in previous work:

  * •

There is no correlation between the CNEOS velocity error and the bolide speed.

  * •

There is no reason to claim that the fast CNEOS events have uncertainties of
10-15 km s-1. The maximum error observed in the database is an event with $dv$
= 7.9 km s-1. The standard deviation of the error (in absolute value) is 2.5
km s-1.

  * •

Current empirical evidence indicates that, if the errors of the calibrated set
are representative, there is a 94.3% probability that CNEOS14 is of extrasolar
origin.

The conclusions of our analysis, initially drawn from previously existing
data, are strongly reinforced by the recent 2024 Iberian superbolide. This new
event allows us to add a second data point to the fast limit of the calibrated
CNEOS population, thus providing a more robust picture of the statistical
sample.

###### Acknowledgements.

The author acknowledges support from the Agencia Estatal de Investigación del
Ministerio de Ciencia e Innovación (AEI-MCINN) under grant ”Hydrated Minerals
and Organic Compounds in Primitive Asteroids” with reference
PID2020-120464GB-100. This research has made use of NASA’s Astrophysics Data
System Bibliographic Services and the NASA JPL CNEOS fireball database. The
Python Matplotlib (Hunter, 2007), Numpy (Van Der Walt et al., 2011), Scipy
(Virtanen et al., 2020) and IPython (Pérez & Granger, 2007) modules have been
employed to generate the figures and calculations in this paper.

## References

  * Akritas et al. (1995) Akritas, M. G., Murphy, S. A., & Lavalley, M. P. 1995, Journal of the American Statistical Association, 90, 170
  * Almond et al. (1950) Almond, M., Davies, J., & Lovell, A. 1950, The Observatory, Vol. 70, p. 112-113 (1950), 70, 112
  * Bannister et al. (2019) Bannister, M. T., Bhandare, A., Dybczyński, P. A., et al. 2019, Nature astronomy, 3, 594
  * Bialy & Loeb (2018) Bialy, S. & Loeb, A. 2018, The Astrophysical Journal Letters, 868, L1
  * Brown & Batygin (2021) Brown, M. E. & Batygin, K. 2021, The Astronomical Journal, 162, 219
  * Brown & Borovička (2023) Brown, P. G. & Borovička, J. 2023, The Astrophysical Journal, 953, 167
  * Derpanis (2010) Derpanis, K. G. 2010, Image Rochester NY, 4, 2
  * Desch (2024) Desch, S. 2024, arXiv preprint arXiv:2403.05161
  * Desch & Jackson (2023) Desch, S. & Jackson, A. 2023, arXiv e-prints, arXiv:2311.07699
  * Desch et al. (2022) Desch, S. J., Jackson, A. P., Noviello, J. L., & Anbar, A. D. 2022, Scientific reports, 12, 10415
  * Devillepoix et al. (2019) Devillepoix, H. A., Bland, P. A., Sansom, E. K., et al. 2019, Monthly Notices of the Royal Astronomical Society, 483, 5166
  * Fernando et al. (2024) Fernando, B., Charalambous, C., Desch, S., et al. 2024, LPI Contributions, 3040, 2595
  * Fernando et al. (2024) Fernando, B., Mialle, P., Ekström, G., et al. 2024, arXiv e-prints, arXiv:2403.03966
  * Fisher (1928) Fisher, W. J. 1928, Harvard College Observatory Circular, 331, 1
  * Gallardo (2023) Gallardo, P. A. 2023, Research Notes of the AAS, 7, 220
  * Gallardo (2024) Gallardo, P. A. 2024, Research Notes of the AAS, 8, 88
  * Hajdukova et al. (2020) Hajdukova, M., Sterken, V., Wiegert, P., & Kornoš, L. 2020, Planetary and Space Science, 192, 105060
  * Hunter (2007) Hunter, J. D. 2007, Computing In Science & Engineering, 9, 90
  * Jewitt & Seligman (2023) Jewitt, D. & Seligman, D. Z. 2023, Annual Review of Astronomy and Astrophysics, 61, 197
  * Loeb (2022) Loeb, A. 2022, Astrobiology, 22, 1392
  * Loeb et al. (2024a) Loeb, A., Adamson, T., Bergstrom, S., et al. 2024a, arXiv preprint arXiv:2401.09882
  * Loeb et al. (2024b) Loeb, A., Adamson, T., Bergstrom, S., et al. 2024b, Research Notes of the AAS, 8, 39
  * Opik (1950) Opik, E. 1950, Irish Astronomical Journal, vol. 1 (3), p. 80, 1, 80
  * Peña-Asensio et al. (2024a) Peña-Asensio, E., P. Grèbol-Tomàs, P., Trigo-Rodríguez, J. M., Ramírez-Moreta, P., & Kresken, R. 2024a, submitted [arXiv:astro-ph/2405.15024]
  * Peña-Asensio et al. (2022) Peña-Asensio, E., Trigo-Rodríguez, J. M., & Rimola, A. 2022, The Astronomical Journal, 164, 76
  * Peña-Asensio et al. (2024b) Peña-Asensio, E., Visuri, J., Trigo-Rodríguez, J. M., et al. 2024b, Icarus, 408, 115844
  * Pérez & Granger (2007) Pérez, F. & Granger, B. E. 2007, Computing in Science and Engineering, 9, 21
  * Sheerin & Loeb (2021) Sheerin, T. F. & Loeb, A. 2021, Journal of the British Interplanetary Society, 74, 427
  * Siegel (1982) Siegel, A. F. 1982, Biometrika, 69, 242
  * Siraj & Loeb (2021) Siraj, A. & Loeb, A. 2021, Scientific Reports, 11, 3803
  * Siraj & Loeb (2022) Siraj, A. & Loeb, A. 2022, The Astrophysical Journal, 939, 53
  * Siraj & Loeb (2023) Siraj, A. & Loeb, A. 2023, Signals, 4, 644
  * Socas-Navarro (2023) Socas-Navarro, H. 2023, The Astrophysical Journal, 945, 22
  * Spearman (1904) Spearman, C. 1904, The American Journal of Psychology, 15, 72
  * Tagliaferri et al. (1994) Tagliaferri, E., Spalding, R., Jacobs, C., Worden, S. P., & Erlich, A. 1994, Hazards due to Comets and Asteroids, 24, 199
  * Van Der Walt et al. (2011) Van Der Walt, S., Colbert, S. C., & Varoquaux, G. 2011, Computing in Science & Engineering, 13, 22
  * Virtanen et al. (2020) Virtanen, P., Gommers, R., Oliphant, T. E., et al. 2020, Nature Methods, 17, 261