Nonnegativity of a metric is a consequence of the other axioms, not an axiom

Let $X$ be a set and let $p : X \times X \to \mathbb{R}$ satisfy the reflexivity axiom (M1') $p(x,x) = 0$ and the symmetry axiom (M2) $p(x,y) = p(y,x)$ of Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric. Then:

1. If $p$ satisfies the triangle inequality (M3), then $p(x,y) \ge 0$ for all $x, y \in X$.
2. If $p$ satisfies the strong triangle inequality (M3'), then $p(x,y) \ge 0$ for all $x, y \in X$.

In particular every metric, every pseudometric and every ultrametric (Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric) takes only nonnegative values. Nonnegativity is therefore a theorem about the axiom list this library uses, not a fourth axiom, and no statement on this page needs to assume it separately.

• What each claim uses. Claim 1 is the familiar two-line argument $0 = p(x,x) \le p(x,y) + p(y,x) = 2p(x,y)$ followed by the observation that a negative real added to itself stays negative. Claim 2 does not need that second half at all: the strong triangle inequality delivers $0 \le p(x,y)$ in one step, because the maximum of a real number with itself is that number.
• Symmetry is used in both claims and cannot be dropped. Without (M2) the instantiation of step 1.1 only gives $0 \le p(x,y) + p(y,x)$, which leaves the possibility that one of the two values is negative and the other larger and positive. Dropping (M2) instead of weakening (M1) gives the notion usually called a quasimetric, which this library does not treat; for it the argument above is unavailable, so nonnegativity is not redundant there and is imposed as part of the definition (Which metric axiom list this library uses, the live naming fork between semimetric and pseudometric, and why extended metrics are not treated here).