Congruence Relation

Segment congruence on tau^3 defined by AB ~ CD iff d(A,B) = d(C,D), where d is the canonical ultrametric distance.

Congruence Relation

Summary

Segment congruence on tau^3 defined by AB ~ CD iff d(A,B) = d(C,D), where d is the canonical ultrametric distance.

Statement

%
\label{def:congruence}
For points $A, B, C, D \in \tau^3$,
the segment~$AB$ is \textbf{congruent} to the segment~$CD$,
written
\[
    \boxed{AB \cong CD
    \quad:\!\iff\quad
    d(A, B) \;=\; d(C, D),}
\]
where $d$ is the canonical ultrametric distance
(Definition~\ref{def:ultrametric-distance}).
Equivalently, in terms of first disagreement depth:
\[
    AB \cong CD
    \quad\iff\quad
    \delta(A, B) \;=\; \delta(C, D).
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 51
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part04/ch19-congruence.tex lines 74-93

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Geometry.Congruence
• Name: congruent

Dependencies

• Canonical: II.D13

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.