Three-Level Equality

Three levels of sameness: (1) ontic identity (primitive), (2) address equivalence (decidable, NF-based), (3) shadow equality (external VM readout).

Three-Level Equality

Summary

Three levels of sameness: (1) ontic identity (primitive), (2) address equivalence (decidable, NF-based), (3) shadow equality (external VM readout).

Statement

%
\label{def:three-equality}
The three levels of equality in $\tau$ are:

\medskip
\textbf{Level 1 --- Ontic identity ($=_{\mathrm{ont}}$).}
Two objects $x, y \in \Obj(\tau)$ are \textbf{ontically identical}
if they are the same element of $\Obj(\tau)$:
same seed generator and same depth.
\[
    x =_{\mathrm{ont}} y
    \quad:\Longleftrightarrow\quad
    \mathrm{seed}(x) = \mathrm{seed}(y)
    \;\text{and}\;
    \mathrm{depth}(x) = \mathrm{depth}(y).
\]
This is the primitive notion of equality.
It is decidable: given any two objects,
one can compare their seeds and depths in finite time.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 29
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part03/ch14-three-equality.tex lines 54-74

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Denotation.Equality
• Name: Tau.Denotation.Equality

Dependencies

• Canonical: I.T01, I.D07

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.