Betweenness Relation

Betweenness Relation

Betweenness Relation

Summary

Betweenness Relation

Statement

%
\label{def:betweenness}
For points $x, y, z \in \tau^3$,
we say \textbf{$y$ is between $x$ and~$z$},
written $B(x,y,z)$, if and only if
\[
    \boxed{B(x,y,z)
    \;\;:\Longleftrightarrow\;\;
    d(x,z)
    \;=\;
    \max\bigl(\, d(x,y),\; d(y,z) \,\bigr).}
\]
Equivalently, in terms of the first disagreement depth
$\delta$ (II.D12):
\[
    B(x,y,z)
    \;\;\Longleftrightarrow\;\;
    \delta(x,z)
    \;=\;
    \min\bigl(\, \delta(x,y),\; \delta(y,z) \,\bigr).
\]
In words: $y$ is between $x$ and~$z$
when~$y$ agrees with each endpoint
to at least the depth at which
the endpoints diverge from each other.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 49
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part04/ch18-betweenness.tex lines 83-109

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Geometry.Betweenness
• Name: between

Dependencies

• Canonical: II.D13, II.T05

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.