Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The reverse triangle inequality d(x,z)d(y,z)d(x,y)|d(x,z) - d(y,z)| \le d(x,y) in any metric space

Statement

Let (X,d)(X,d) be a metric space (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric) and let x,y,zXx, y, z \in X. Then

d(x,z)d(y,z)d(x,y),|d(x,z) - d(y,z)| \le d(x,y),

where |\cdot| is the absolute value of R\mathbb{R} (Absolute value in an ordered field).

Facts & Assumptions

Given: A metric space (X,d)(X,d) and points x,y,zXx, y, z \in X; write t:=d(x,z)d(y,z)t := d(x,z) - d(y,z).

[A1]

The triangle inequality (M3): d(a,c)d(a,b)+d(b,c)d(a,c) \le d(a,b) + d(b,c) for all a,b,cXa,b,c \in X (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[A2]

Symmetry (M2): d(a,b)=d(b,a)d(a,b) = d(b,a) for all a,bXa,b \in X (Metric space: d(x,y)=0d(x,y) = 0 iff x=yx = y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L1]

For every real uu, the value u|u| equals uu or u-u (Basic properties of the absolute value, Absolute value in an ordered field).

[L2]

Adding a constant to an inequality: if aba \le b then a+cb+ca + c \le b + c. Order is preserved by adding a constant and by adding inequalities states the strict form a<ba+c<b+ca < b \Rightarrow a + c < b + c; the nonstrict form used here is that strict form together with the case a=ba = b, in which the two sides are equal, the order being total (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

By [A1] at (a,b,c)=(x,y,z)(a,b,c) = (x,y,z): d(x,z)d(x,y)+d(y,z)d(x,z) \le d(x,y) + d(y,z).

A1
1.2

By [A1] at (a,b,c)=(y,x,z)(a,b,c) = (y,x,z): d(y,z)d(y,x)+d(x,z)d(y,z) \le d(y,x) + d(x,z), and by [A2] d(y,x)=d(x,y)d(y,x) = d(x,y), so d(y,z)d(x,y)+d(x,z)d(y,z) \le d(x,y) + d(x,z).

A1A2
2.1

Adding d(y,z)-d(y,z) to both sides of step 1.1 gives t=d(x,z)d(y,z)d(x,y)t = d(x,z) - d(y,z) \le d(x,y).

step 1.1L2
2.2

Adding d(x,z)-d(x,z) to both sides of step 1.2 gives d(y,z)d(x,z)d(x,y)d(y,z) - d(x,z) \le d(x,y), that is td(x,y)-t \le d(x,y).

step 1.2L2
3.1

By [L1] the real number t|t| is either tt or t-t, and both of these are at most d(x,y)d(x,y) by steps 2.1 and 2.2, so d(x,z)d(y,z)=td(x,y)|d(x,z) - d(y,z)| = |t| \le d(x,y).

step 2.1step 2.2L1

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 19 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources